[Haskell-cafe] Total Functional Programming in Haskell

[Jason Dagit]

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.

I'm also interested in hearing about the optimizations that would be
possible when all your expressions are strongly normalizing.

Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080929/a5fa13f9/attachment.htm