2008/9/30 Jason Dagit
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