Hacker News Reader

Comment by skybrian | Hacker News Reader

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.

View on HN

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