[Haskell-cafe] Re: Total Functional Programming in Haskell
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.
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'
digits' 0 = 
| 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
>> 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.
do in order to QuickCheck programs with IO.
More information about the Haskell-Cafe