[Haskell-cafe] Re: Total Functional Programming in Haskell
lrpalmer at gmail.com
Tue Sep 30 18:28:27 EDT 2008
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.
More information about the Haskell-Cafe