Comment by vilhelm_s | Hacker News Reader

Comment by vilhelm_s | Hacker News Reader

Certainly very sensible points. But I take some issue with the bits towards the end:

> Fetishising Curry-Howard

Hey, I happen to find Curry-Howard sexy, you have no right to shame me!

> To specify and check liveness or reachability, we need to represent programs as some kind of flow graph, where flows are very likely to span multiple functions and multiple modules.

But no, this is exactly what basing systems on Curry-Howard (with terminating functions) buys you. If I give a HTTP response handler in Coq the type

    HttpRequest -> HttpResponse

I know it is live, because the function is total. And similarly, dead code paths can be gotten rid of by eliminating a proof of False.

So this lets you state liveness and unreachability. Of course, the proofs of those statements is very different from program-analysis-style systems. In a whole-program analysis, the analyser goes over the entire program, and at the end it says "well, I could not find anything calling this function, so I guess it's dead". In a Curry-Howard-style system, you need to look at the function and figure out when it should be called and what preconditions need to be true for it to work properly. But this is exactly why people like type systems, you can think about programs modularly rather than all at once.

I suppose, but outside certain mathematical systems that are designed that way, assuming that all functions are total is unrealistic. The languages we use every day are Turing-complete languages and infinite loops can happen.

You don't have to assume everything is total, you just need to track in the type system which things are and which aren't. E.g. you could also give it the type

    HttpRequest -> IO HttpResponse

where IO is some type allowing nontermination (e.g. defined coinductively along the lines of http://www.cs.swan.ac.uk/~csetzer/slides/goeteborg2009AgdaIn...).

Having a type for total functions gives you the option to state and prove totality properties, even if you maybe don't want to go through the effort of doing that for every function you write.

Koka [1] does this; I find Daan's experiences in using it to build Madoko [2] to be very enlightening. Basically, I think he had to give up on total-ness more than he would have liked.

[1] http://research.microsoft.com/en-us/projects/koka/

[2] http://madoko.codeplex.com/

You don't need to go all the way to IO, you can make every function total using Partial:

    data Partial a = Now a | Later (Partial a)

It's straightforward to do things in Partial, since it's a Functor, Applicative and Monad:

    instance Functor Partial where
        fmap f (Now x) = Now (f x)
        fmap f (Later x) = Later (fmap f x)

    instance Applicative Partial where
        pure x = Now x
        (Now f) <*> (Now x) = Now (f x)
        (Later f) <*> x = Later (f <*> x)
        f <*> (Later x) = Later (f <*> x)

    instance Monad Partial where
        return = pure
        f >>= (Now x) = f x
        f >>= (Later x) = Later (f x)

Partial is so trivial that everything can be made co-recursive by wrapping all function bodies in "Later". All of the "Later" wrappers will get nested together by the Applicative/Monad; everything will "just work". The one missing piece is the following function, which isn't total:

    runPartial :: Partial a -> a
    runPartial (Now x) = x
    runPartial (Later x) = runPartial x

We could name it `unsafeForcePartial` and treat it with care, like we currently do with `unsafePerformIO`.

Can you explain how this makes every function total? For example, take the `head` function which is not total

    head :: [a] -> a
    head (x:xs) = x
    head []     = undefined

How can you make this total using `Partial`? I can get as far as

    headTotal :: [a] -> Partial a
    headTotal (x:xs) = Now x
    headTotal []     = Later (...)

but what goes in (...)?

This is why it's always seemed to me that head ought to be typed as

    head :: [a] -> Maybe a

Scala's collections have this function as headOption, which I use almost exclusively over head.

I guess you need a special definition

    diverge = Later diverge
    headTotal [] = diverge

Yep, although it doesn't actually diverge; that's the point ;)

The classic "loop" function, which is completely polymorphic, does diverge:

    loop :: a
    loop = loop

"loop" will never return a value, since to perform one 'step', it must perform an 'infinite' amount of computation.

The function you've written doesn't diverge, since it will immediately return a value "Later x" after one step. As long as we're using laziness, it doesn't matter that "x" itself is 'infinite':

    loop' :: Partial a
    loop' = Later loop'

Note that we can do an equivalent thing in strict languages, by eta-expanding our definitions into thunks:

    data Partial' a = Now a | Later (() -> Partial a)

    loop'' :: () -> Partial a
    loop'' _ = Later loop''

We can use "loop :: a" in place of "undefined :: a", since they have the same type. We can't use "loop' :: Partial a" in the same way, since its type is different.

"loop' :: Partial a" is a bit like a 'phantom type', where the "a" in its type signature never actually occurs in the value. In fact, we can define a type which doesn't contain "Now", and is thus guaranteed to never terminate:

    data Inf a = Inf (Inf a)

Of course, the "a" in "Inf a" is a true phantom: it doesn't affect the values at all. We can get rid of it to obtain:

    data Loop = Loop Loop

We can use this type to "drive" main loops for servers, operating systems, games, etc. in a total language:

    server :: Loop -> IO Loop
    server (Loop x) = do req <- readRequest
                         sendResponse (process req)
                         Loop <$> server x

"Loop" is equivalent to "Stream ()", where:

    data Stream a = Cons a (Stream a)

Of course, "Stream a" is to "[a]" what "Inf a" is to "Partial a": it's just missing the base-case ("[]" and "Now a", respectively).

Interestingly, we can think of "Partial a" as being like "[a]", except that it stores elements in "[]" rather than ":". Alternatively, we can think of "Partial a" as being like "Nat" (the Peano numbers), which uses an element of "a" in place of "Zero".

Reply on news.ycombinator.com