[Haskell-cafe] Re: Total Functional Programming in Haskell

[Luke Palmer]

2008/9/30 Jason Dagit <dagit at codersbase.com>:
>> It seems to me that dependent types are best for ensuring totality.
>
> Bear with me, as I know virtual nothing about dependent types yet.  In the
> total functional paradigm the language lacks a value for bottom.  This means
> general recursion is out and in the paper I cited it was replaced with
> structural recursion on the inputs.  How do dependent types remove bottom
> from the language?

Most DT languages are total.  You have to be able to evaluate terms to
typecheck, so in order to have a terminating compiler, your language
needs to be bottomless.

The other side of that is that dependent types are strong enough to
express termination proofs of some very tricky functions, which I
suspect would not be possible to prove otherwise.

Luke