Am 16.03.2014 09:40, schrieb Christiaan Baaij:
To answer the second question (under the assumption that you want
phantom-type style Vectors and not GADT-style):
That works, someNatVal was the missing piece.
Now the natural next question is how to perform type-level induction on
Nat. This page mentions the Nat1 type, a unary representation of natural
numbers:
https://ghc.haskell.org/trac/ghc/wiki/TypeNats/MatchingOnNats
Since the unary natural number kind so ubiquituous in examples, is there
a recommended module to import it from, which also contains the
injectivity magic of FromNat1? I cannot see it in:
http://hackage.haskell.org/package/base-4.7.0.0/candidate/docs/GHC-TypeLits.html
although it seems to have been there:
http://co-dan.github.io/base-docs/src/GHC-TypeLits.html
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
