[Haskell-cafe] Total Functional Programming in Haskell

[Derek Elkins]

On Mon, 2008-09-29 at 20:02 -0700, Jason Dagit wrote:
> Hello,
> 
> I recently had someone point me to this thread on LtU:
> http://lambda-the-ultimate.org/node/2003
> 
> The main paper in the article is this one:
> http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf
> 
> It leaves me with several questions:
> 1) Are there are existing Haskell-ish implementations of the total
> functional paradigm?
> 2) Could we restructure Haskell so that it comes in 3 layers, total
> functional core, lazy pure partial functional middle, and IO outer
> layer?
> 
> The idea with #2 is that similar to how we use the type system to
> separate the purely functional from monadic, and in particular IO
> actions, can we make the inner most part of Haskell total?
> Furthermore, could we do this in a way that makes it easy to
> intermingle the three layers the way we can mingle pure Haskell with
> IO actions?
> 
> 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

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.

* and other stuff, but that's the significant one, it's easy enough to
add a primitive error :: String -> Partial a