[Haskell-cafe] Total Functional Programming in Haskell

Mitchell, Neil neil.mitchell.2 at credit-suisse.com
Tue Sep 30 03:51:29 EDT 2008


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.




	From: haskell-cafe-bounces at haskell.org
[mailto:haskell-cafe-bounces at 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
	I recently had someone point me to this thread on LtU:
	The main paper in the article is this one:
	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
	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.

Please access the attached hyperlink for an important electronic communications disclaimer: 


More information about the Haskell-Cafe mailing list