Am 15.03.2014 19:17, schrieb Erik Hesselink:
I think most of the singletons stuff has been moved to the
'singletons' package [0].
Yes, that's it. It means that all Nat related functionality in
'singletons' can be implemented using GHC.TypeLits - interesting.
Using the library I succeeded to convert type-level Nats to data-level
Integer. Now I need the other way round. I want to implement:
withVector ::
[a] ->
(forall n. (KnownNat n) => Vector n a -> b) ->
b
I want to have the (KnownNat n) constraint, since I want to call 'sing'
within the continuation and this requires (KnownNat n). I guess, in
order to implement withVector I need toSing, but this one does not give
me a (KnownNat n). :-(
Thus I have two questions: What is the meaning of KnownNat and how can I
implement "withVector"?
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
