[Haskell-cafe] Re: Type-Marking finite/infinte lists?

Roberto Zunino zunino at di.unipi.it
Mon Sep 17 13:14:58 EDT 2007

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.


More information about the Haskell-Cafe mailing list