
17 Sep
2007
17 Sep
'07
5:14 p.m.
apfelmus wrote:
cons :: a -> List e f a -> List Nonempty f a
But unfortunately, finiteness is a special property that the type system cannot guarantee. The above type signature for cons doesn't work since the following would type check
bad :: a -> List Nonempty Finite a bad x = let xs = cons x xs in xs
In other words, Haskell's type system doesn't detect infinite recursion.
I thought this was possible with GADTs (is it?): data Z data S n data List a len where Nil :: List a Z Cons:: a -> List a len -> List a (S len) Then, bad (adapted from above) does not typecheck. Probably, type classes can be exploited to the same aim. Regards, Zun.