25 Oct
2014
25 Oct
'14
2:22 p.m.
you want the following (which doesnt require undediable instances)
data Nat = Z | S Nat
type family U (x :: Nat) where U 0 = Z U n = S (U (n-1))
this lets you convert type lits into your own peanos or whatever
Yes, you can do that, but why should you have to? Nat is already the natural numbers, so already has this structure. Why do we have to define it again, making our code that much less clear and readable?