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

[Dan Piponi]

On 9/16/07, apfelmus <apfelmus at quantentunnel.de> wrote:
> 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