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. I'm also interested in hearing about the optimizations that would be possible when all your expressions are strongly normalizing. Jason