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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
