Jason Dagit wrote:
apfelmus wrote:
It seems to me that dependent types are best for ensuring totality.
Bear with me, as I know virtual nothing about dependent types yet.
Ah, my bad. Time to change that ;) Personally, I found Th. Altenkirch, C. McBride, J. McKinna. Why dependent types matter. http://www.cs.st-andrews.ac.uk/~james/RESEARCH/ydtm-submitted.pdf to be a very gentle introduction.
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?
Originally, all typed lambda calculi - like the simply typed lambda calculus or System F on which Haskell is based - are strongly normalizing by default, i.e. every computation terminates. Thus, bottom is actually *added* to Haskell, in particular by providing the new primitive fix :: (a -> a) -> a When viewed through the Curry-Howard Isomorphism, it's clear that fix is a bad idea. I mean, it corresponds to the "theorem" forall A. (A -> A) -> A which is clearly wrong, for it can prove the existence of Santa Claus: fix (\Santa Claus exists -> Santa Claus exists) = Santa Claus exists Since dependently typed languages perform computations on the type level, most do not add general recursion or at least pay special attention to it. Furthermore, as Luke said, they give you the necessary tools to easily express programs that are not structurally recursive, but nonetheless terminate. One example would be a function to represent a natural in binary: data Nat = Succ Nat | Zero data Digit = D0 | D1 digits :: Nat -> [Digit] digits = reverse digits' where digits' 0 = [] digits' n | even n = D0:digits' (n `div` 2) | odd n = D1:digits' (n `div` 2) This is not structurally recursive (at least not directly), but clearly terminates. You can use dependent types to prove that it does. For a more complicated example, see also http://www.iis.sinica.edu.tw/~scm/2008/well-founded-recursion-and-accessibil...
The IO layer can be interpreted as "co-total", i.e. as codata.
I was asserting that Haskell is currently 2 layered. Purely functional vs. IO. They integrate nicely and play well together, but I still think of them as distinct layers. Perhaps this is not fair or confusing though. The paper I cited did indeed use codata to define streams so that something, such as an OS, that needs to process infinite streams of requests can still do so.
Well, you can interpret IO as a data type data IO a where Bind :: IO a -> (a -> IO b) -> IO b Return :: a -> IO a PutChar :: Char -> IO () GetChar :: IO Char just like any other data type. In fact, that's what W. Swierstra, Th. Altenkirch. Beauty in the Beast. http://www.cs.nott.ac.uk/~txa/publ/beast.pdf do in order to QuickCheck programs with IO. Regards, apfelmus