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