[Haskell-cafe] Re: Type-Marking finite/infinte lists?
zunino at di.unipi.it
Mon Sep 17 13:14:58 EDT 2007
> 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 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.
More information about the Haskell-Cafe