converting data-level natural numbers to type-level
lemming at henning-thielemann.de
Sat Mar 15 20:48:58 UTC 2014
Am 15.03.2014 19:17, schrieb Erik Hesselink:
> I think most of the singletons stuff has been moved to the
> 'singletons' package .
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:
(forall n. (KnownNat n) => Vector n a -> 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
More information about the Glasgow-haskell-users