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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
