2008/9/30 Jason Dagit <[EMAIL PROTECTED]>: >> 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe