
Hi 1) Total Functional Programming is great. But a combination of Approve and Catch gives you termination and pattern-match safety checks for Haskell, giving you all the advantages of TFP without forcing you to write total patterns etc. Plus you can use all the Haskell tools. In reality, neither of those tools is probably ready for prime time - but neither is that far off. In the meantime something like Agda might give you some of what you want. 2) We already have a IO outer layer (monad), and the checkers above collapse the first 2 layers. Perhaps a "monadic" or annotated middle layer would be handy for bits that the checkers can't validate. The idea of |-> vs -> seems like encoding lots in the type system, which seems to be going overboard. It might be a tool of last resort, but you'd much rather eliminate the partial bits entirely. As for optimisation, remember that closed terms are strongly normalising, but that the compiler will almost certainly have to work on open terms, which aren't. Things like partial evaluation might be easier to do, but there is still technology from the 1970's (supercompilation) that we've only just begun to apply to Haskell - so I don't think termination of closed terms is pressing optimisation bottleneck. Thanks Neil ________________________________ From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of Jason Dagit Sent: 30 September 2008 4:03 am To: haskell mailing list Subject: [Haskell-cafe] Total Functional Programming in Haskell 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_07 51_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 ============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================