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

[apfelmus]

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-accessibility/


>> 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