type-level induction on Nat

Henning Thielemann lemming at henning-thielemann.de
Sun Mar 16 10:29:20 UTC 2014

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 

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:


although it seems to have been there:

More information about the Glasgow-haskell-users mailing list