16 Sep
2007
16 Sep
'07
6:01 p.m.
On 9/16/07, apfelmus
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.
Exactly. Haskell allows free unrestrained recursion, and this is the source of the problem. Instead we could limit ourselves to "structural recursion" and then we can guarantee that even if we write recursive code, the results will always be finite. For details there's Turner's paper on "Total Functional Programming": http://www.cs.mdx.ac.uk/staffpages/dat/sblp1.pdf -- Dan