[Haskell-cafe] Total Functional Programming in Haskell

[Conor McBride]

Hi

I've been reticent to join this thread as it has the potential
to eat my life, but I thought I'd say some technical things.

On 30 Sep 2008, at 22:54, Derek Elkins wrote:

> On Mon, 2008-09-29 at 20:02 -0700, Jason Dagit wrote:
>> Maybe instead of using (->) as the function constructor for total
>> functions we use a different symbol, say (|->), and the compiler  
>> knows
>> to use the more specialized semantics on those definitions.  I'm not
>> sure how make this work for values that are total functional versus
>> values that are just pure (partial) functional.
>
> This can be done exactly the same way it is done with IO.  Remove
> general recursion* from Haskell and have a partiality monad with
> fix :: (a -> a) -> Partial a

I'm not sure that's the best type for fix, to be honest (though it
would do in a pinch). It doesn't nest very neatly.

Some argue for

   sfix :: (a -> Partial a) -> Partial a

which allows you to make partial computations from recursive values.
Being a happy Haskeller, I'd prefer

   lfix :: (Partial a -> Partial a) -> Partial a

which is probably just join . fix as you present it, but says that
its body gets a computation which it can choose to run, or not, as
appropriate.

In the dependently typed world, remember there are two separate
notions of operational semantics
   (1) the open evaluation used by the typechecker, reducing
         under lambda, etc
   (2) the closed evaluation used at run-time, with no computation
         under binders

It should be straightforward to make lfix a constant in (1),
whilst (2) would actually run it. So that is indeed very like IO,
handing off computations to an unscrupulous run-time system. Of
course, we'd provide laws to reason about Partial computations
(monad laws, unrolling, fixpoint induction) with sufficient means
to allow escape from Partial on presentation of a (non-Partial)
termination proof (erased for (2)). That's all to say that we can
set things up so you can pay as you go. Of course, that's just to
say we can model the phenomena, not that we can present them
ergonomically...

But what of Haskell?

> This particular idea has been discussed several times in a couple of
> places.  Most people seem to think it would be too much of a hassle to
> use.

Not the most copper-bottomed of arguments, as well you know,
but if programming in Partial entails clunky monadification of
lovely terse applicative code, most people are probably right.
However, what if we were to find a way to break that entailment?
The idiom bracket notation is a step in that direction, but it's
still not enough.

Suppose we were to find a way to program with our usual notation,
but with the extra freedom to vary the 'ambient' monad? We could
choose Id for total programs, Partial for workaday slackness, and
a whole bunch of other stuff at our convenience. We'd need some
way to change the ambient monad locally, of course.

To be frank, I don't know if such a setup could be made to fit
with Haskell's existing design choices. But I think it's an
attractive possibility, worth looking into.

Locally, however, my point is to ask whether there's a specific
hassle with the Partial monad beyond the usual notational
annoyances that come with any monad. If so, that would be
interesting to hear about, and new to my ears.

All the best

Conor