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

[apfelmus]

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)
> 
> Then, bad (adapted from above) does not typecheck.

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