[Haskell-cafe] Total Functional Programming in Haskell
Jason Dagit
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
apfelmus
> 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?
Agda?
http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.HomePage
It seems to me that dependent types are best for ensuring totality.
> 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 IO layer can be interpreted as "co-total", i.e. as codata.
Basically, this means that it's guaranteed that the program prints or
reads something after a finite amount of time and does not loop forever
without doing anything.
Regards,
apfelmus
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Mitchell, Neil
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
________________________________
==============================================================================
Please access the attached hyperlink for an important electronic communications disclaimer:
http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==============================================================================
Luke Palmer
> 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?
Aye. I'd say you pretty much need dependent types if you want to do
interesting things and prove totality at the same time. Or that might
be better stated as: as long as you're proving totality, why not use
dependent types? :-)
But I *want* to do something like that with Coq (I prefer it to Agda
for little more than personal taste). In particular, I'd like to see
a reasoning framework for partial functions, so you could state and
prove a property like:
length [1..] = _|_
As well as generate Haskell code for the partial functions which you
are reasoning about.
I've been idly pondering how to do this. Does anyone know about
something like this for coq or agda?
Luke
Mitchell, Neil
> for little more than personal taste). In particular, I'd like to see
> a reasoning framework for partial functions, so you could
> state and prove a property like:
>
> length [1..] = _|_
In a compiler, with:
default(Int)
main = print $ length [1..]
Results in 2147483647
I don't think dependent types are the answer - or at least I don't think
people have asked the questions in standard Haskell enough. We still
don't even have an equational reasoning assistant publically available
and widely used.
Thanks
Neil
==============================================================================
Please access the attached hyperlink for an important electronic communications disclaimer:
http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==============================================================================
_______________________________________________
Robin Green
"Luke Palmer" <lrpa...@gmail.com> wrote:
> But I *want* to do something like that with Coq (I prefer it to Agda
> for little more than personal taste). In particular, I'd like to see
> a reasoning framework for partial functions, so you could state and
> prove a property like:
>
> length [1..] = _|_
Bear in mind, in Coq, the equivalent of [1..] is a stream, whereas the
equivalent of [1,2,3] is a list. You'd have to have list functions in
Coq which worked generically over both lists and streams to be able to
say what you want, and I don't know of any existing attempt to do that.
--
Robin
Luke Palmer
> On Tue, 30 Sep 2008 03:27:09 -0600
> "Luke Palmer" <lrpa...@gmail.com> wrote:
>
>> But I *want* to do something like that with Coq (I prefer it to Agda
>> for little more than personal taste). In particular, I'd like to see
>> a reasoning framework for partial functions, so you could state and
>> prove a property like:
>>
>> length [1..] = _|_
>
> Bear in mind, in Coq, the equivalent of [1..] is a stream, whereas the
> equivalent of [1,2,3] is a list.
You miss my point. Every value here is lifted to its domain before
being reasoned about. So eg. [1,1..] is not the coinductive x = 1:x.
Instead we model this example like so (this is my current direction,
nothing tested or fully reasoned out, so I may be full of beans):
[1..] is the limit [_|_, 1:_|_, 1:2:_|_, ...]
length [1..] is the limit [_|_, _|_, _|_, ...]
Every function we can write in Haskell is corecursive on this
representation, because every such function is Scott-continuous. To
prove the above property would amount to proving that every element of
the resulting limit is _|_, so the whole limit is _|_.
Luke
Jason Dagit
> 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_0768_turner.pdf
> >
> > It leaves me with several questions:
> > 1) Are there are existing Haskell-ish implementations of the total
> > functional paradigm?
>
> Agda?
>
> http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.HomePage
>
> It seems to me that dependent types are best for ensuring totality.
Bear with me, as I know virtual nothing about dependent types yet. In the
total functional paradigm the language lacks a value for bottom. This means
general recursion is out and in the paper I cited it was replaced with
structural recursion on the inputs. How do dependent types remove bottom
from the language?
>
> > 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 IO layer can be interpreted as "co-total", i.e. as codata.
> Basically, this means that it's guaranteed that the program prints or
> reads something after a finite amount of time and does not loop forever
> without doing anything.
I was asserting that Haskell is currently 2 layered. Purely functional vs.
IO. They integrate nicely and play well together, but I still think of them
as distinct layers. Perhaps this is not fair or confusing though. The
paper I cited did indeed use codata to define streams so that something,
such as an OS, that needs to process infinite streams of requests can still
do so.
Thanks,
Jason
Derek Elkins
> 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.
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
Luke Palmer
>> It seems to me that dependent types are best for ensuring totality.
>
> Bear with me, as I know virtual nothing about dependent types yet. In the
> total functional paradigm the language lacks a value for bottom. This means
> general recursion is out and in the paper I cited it was replaced with
> structural recursion on the inputs. How do dependent types remove bottom
> from the language?
Most DT languages are total. You have to be able to evaluate terms to
typecheck, so in order to have a terminating compiler, your language
needs to be bottomless.
The other side of that is that dependent types are strong enough to
express termination proofs of some very tricky functions, which I
suspect would not be possible to prove otherwise.
Luke
Conor McBride
I've been reticent to join this thread as it has the potential
to eat my life, but I thought I'd say some technical things.
On 30 Sep 2008, at 22:54, Derek Elkins wrote:
> On Mon, 2008-09-29 at 20:02 -0700, Jason Dagit wrote:
>> 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
I'm not sure that's the best type for fix, to be honest (though it
would do in a pinch). It doesn't nest very neatly.
Some argue for
sfix :: (a -> Partial a) -> Partial a
which allows you to make partial computations from recursive values.
Being a happy Haskeller, I'd prefer
lfix :: (Partial a -> Partial a) -> Partial a
which is probably just join . fix as you present it, but says that
its body gets a computation which it can choose to run, or not, as
appropriate.
In the dependently typed world, remember there are two separate
notions of operational semantics
(1) the open evaluation used by the typechecker, reducing
under lambda, etc
(2) the closed evaluation used at run-time, with no computation
under binders
It should be straightforward to make lfix a constant in (1),
whilst (2) would actually run it. So that is indeed very like IO,
handing off computations to an unscrupulous run-time system. Of
course, we'd provide laws to reason about Partial computations
(monad laws, unrolling, fixpoint induction) with sufficient means
to allow escape from Partial on presentation of a (non-Partial)
termination proof (erased for (2)). That's all to say that we can
set things up so you can pay as you go. Of course, that's just to
say we can model the phenomena, not that we can present them
ergonomically...
But what of Haskell?
> 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.
Not the most copper-bottomed of arguments, as well you know,
but if programming in Partial entails clunky monadification of
lovely terse applicative code, most people are probably right.
However, what if we were to find a way to break that entailment?
The idiom bracket notation is a step in that direction, but it's
still not enough.
Suppose we were to find a way to program with our usual notation,
but with the extra freedom to vary the 'ambient' monad? We could
choose Id for total programs, Partial for workaday slackness, and
a whole bunch of other stuff at our convenience. We'd need some
way to change the ambient monad locally, of course.
To be frank, I don't know if such a setup could be made to fit
with Haskell's existing design choices. But I think it's an
attractive possibility, worth looking into.
Locally, however, my point is to ask whether there's a specific
hassle with the Partial monad beyond the usual notational
annoyances that come with any monad. If so, that would be
interesting to hear about, and new to my ears.
All the best
Conor
apfelmus
> apfelmus wrote:
>>
>> It seems to me that dependent types are best for ensuring totality.
>
> Bear with me, as I know virtual nothing about dependent types yet.
Ah, my bad. Time to change that ;) Personally, I found
Th. Altenkirch, C. McBride, J. McKinna.
Why dependent types matter.
http://www.cs.st-andrews.ac.uk/~james/RESEARCH/ydtm-submitted.pdf
to be a very gentle introduction.
> In the
> total functional paradigm the language lacks a value for bottom. This means
> general recursion is out and in the paper I cited it was replaced with
> structural recursion on the inputs. How do dependent types remove bottom
> from the language?
Originally, all typed lambda calculi - like the simply typed lambda
calculus or System F on which Haskell is based - are strongly
normalizing by default, i.e. every computation terminates. Thus, bottom
is actually *added* to Haskell, in particular by providing the new primitive
fix :: (a -> a) -> a
When viewed through the Curry-Howard Isomorphism, it's clear that fix
is a bad idea. I mean, it corresponds to the "theorem"
forall A. (A -> A) -> A
which is clearly wrong, for it can prove the existence of Santa Claus:
fix (\Santa Claus exists -> Santa Claus exists) = Santa Claus exists
Since dependently typed languages perform computations on the type
level, most do not add general recursion or at least pay special
attention to it. Furthermore, as Luke said, they give you the necessary
tools to easily express programs that are not structurally recursive,
but nonetheless terminate. One example would be a function to represent
a natural in binary:
data Nat = Succ Nat | Zero
data Digit = D0 | D1
digits :: Nat -> [Digit]
digits = reverse digits'
where
digits' 0 = []
digits' n
| even n = D0:digits' (n `div` 2)
| odd n = D1:digits' (n `div` 2)
This is not structurally recursive (at least not directly), but clearly
terminates. You can use dependent types to prove that it does. For a
more complicated example, see also
http://www.iis.sinica.edu.tw/~scm/2008/well-founded-recursion-and-accessibility/
>> The IO layer can be interpreted as "co-total", i.e. as codata.
>
> I was asserting that Haskell is currently 2 layered. Purely functional vs.
> IO. They integrate nicely and play well together, but I still think of them
> as distinct layers. Perhaps this is not fair or confusing though. The
> paper I cited did indeed use codata to define streams so that something,
> such as an OS, that needs to process infinite streams of requests can still
> do so.
Well, you can interpret IO as a data type
data IO a where
Bind :: IO a -> (a -> IO b) -> IO b
Return :: a -> IO a
PutChar :: Char -> IO ()
GetChar :: IO Char
just like any other data type. In fact, that's what
W. Swierstra, Th. Altenkirch. Beauty in the Beast.
http://www.cs.nott.ac.uk/~txa/publ/beast.pdf
do in order to QuickCheck programs with IO.
wren ng thornton
> I was asserting that Haskell is currently 2 layered. Purely functional vs.
> IO. They integrate nicely and play well together, but I still think of them
> as distinct layers. Perhaps this is not fair or confusing though. The
> paper I cited did indeed use codata to define streams so that something,
> such as an OS, that needs to process infinite streams of requests can still
> do so.
For a first take on monads, that's not a bad way of thinking about it.
But, once you move beyond first thoughts, monads aren't a special
separate layer and thinking of them as such is liable to land you in
trouble. Monads really are pure, it's just that they get there by
existentializing over impurities.[1]
Perhaps you really do mean only the IO monad and not any others, but
then the question becomes: whose IO? The IO monad is well-known to be a
sin bin for things people don't know or care enough about. Over time
things get added to IO and over time things get broken off into their
own monads. So then where is the layer boundary over time? I assert that
there's no meaningful place to draw the boundary because there's nothing
particularly special about IO that isn't shared by other monads like ST
or ACIO.
It'd be nice to have a total core language, but it's not clear how to
helpfully represent such things in the type system. One variety of
non-totality is the |error| function. We could design our types to say
that people can't call it, but the whole purpose of |error| is to raise
exceptions (a monadic action) from pure code; so as far as the types are
concerned, we already can't do any such things. We can eliminate many
instances of those non-totalities by adding in refinement types (a
modest proposal), in order to prevent people from passing [] to |head|
or |tail|, or passing 0 as the denominator of (/), etc.
But there are other non-totalities, such as _|_ which cannot be captured
by such means. In order to capture many instances of _|_ we'd need to
have our type represent their depth so that we can do co/induction in
order to ensure that the function terminates. While we can capture a
surprising level of such detail in Haskell's type system, this is
marching off in the direction of dependent types which would be making
things more complex rather than simpler. I'm not saying that we
shouldn't head there, but it doesn't seem to be addressing the goals you
had in mind.
[1] Just like existential types, you can put something in but you can
never get it back out again. For inescapable monads like IO and ST, this
is why they have the behavior of sucking your whole program into the
existential black-hole.
--
Live well,
~wren
David Menendez
>
> [1] Just like existential types, you can put something in but you can never
> get it back out again. For inescapable monads like IO and ST, this is why
> they have the behavior of sucking your whole program into the existential
> black-hole.
That's true for IO, but the whole point of ST is that it *is*
escapable. What makes ST (and IO and STM) unusual is that it can't be
implemented in pure Haskell without special support from the run-time
system.
--
Dave Menendez <da...@zednenem.com>
<http://www.eyrie.org/~zednenem/>
wren ng thornton
> On Wed, Oct 1, 2008 at 7:53 PM, wren ng thornton <wr...@freegeek.org> wrote:
>> [1] Just like existential types, you can put something in but you can never
>> get it back out again. For inescapable monads like IO and ST, this is why
>> they have the behavior of sucking your whole program into the existential
>> black-hole.
>
> That's true for IO, but the whole point of ST is that it *is*
> escapable. What makes ST (and IO and STM) unusual is that it can't be
> implemented in pure Haskell without special support from the run-time
> system.
I suppose it depends on definitions. Certainly you can runST it to get
an end result out, but doing so looses the internal structure (STRefs)
which cannot be reclaimed. To me this makes ST a world apart from State,
[], Maybe, and other monads which you can freely escape and reenter.
Perhaps it would've been better to say that ST is not, er, reentrant.
--
Live well,
~wren