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

[Roberto Zunino]

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.