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

apfelmus apfelmus at quantentunnel.de
Mon Sep 17 17:09:42 EDT 2007

```Roberto Zunino wrote:
> 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?):

Interesting, it probably is. See below.

> data Z
> data S n
> data List a len where
>   Nil :: List a Z
>   Cons:: a -> List a len -> List a (S len)
>

Note that you're doing more than forcing your lists to be finite, you
force them to be of a particular size. For instance, a list of type

List a (S (S (S Z)))

is guaranteed to have exactly 3 elements. That's why

bad x = let xs = cons x xs in xs

doesn't type check: the lhs has one more element than the rhs.

As soon as you try to hide the finiteness proof (= count of elements in
the list) away via existential quantification

data ListFinite a where
IsFinite :: List a len -> ListFinite a

the  bad  function reappears and type checks

cons :: a -> ListFinite a -> ListFinite a
cons x (IsFinite xs) = IsFinite (Cons x xs)

bad :: a -> ListFinite a
bad x = let xs = cons x xs in xs

But there is a major difference now: bad is not an infinite list, it's
_|_. That's because  cons  is now strict in the second argument, i.e. it
really does check whether the second argument matches the constructor
IsFinite which means that there's a proof that  xs  is finite.

That's good news, it seems to be that everything of type ListFinite is
finite modulo _|_s. I don't have a proof, though. Of course, we can have
a _|_ in every position, like

cons 1 (cons 2 (IsFinite undefined))

which corresponds to

1 : 2 : _|_

Regards,
apfelmus

```