Re: [Haskell-cafe] Re: Total Functional Programming in Haskell

[wren ng thornton]

David Menendez wrote:

On Wed, Oct 1, 2008 at 7:53 PM, wren ng thornton <[EMAIL PROTECTED]> 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: Total Functional Programming in Haskell

[David Menendez]

On Wed, Oct 1, 2008 at 7:53 PM, wren ng thornton <[EMAIL PROTECTED]> 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.
-- 
Dave Menendez <[EMAIL PROTECTED]>

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: Total Functional Programming in Haskell

[wren ng thornton]

Jason Dagit wrote:

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: Total Functional Programming in Haskell

[Luke Palmer]

2008/9/30 Jason Dagit <[EMAIL PROTECTED]>:
>> 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: Total Functional Programming in Haskell

[Jason Dagit]

On Tue, Sep 30, 2008 at 12:51 AM, apfelmus <[EMAIL PROTECTED]>wrote:

> 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe