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_0...
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