apfelmus apfelmus at quantentunnel.de
Wed Oct 1 06:09:35 EDT 2008

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

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