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

[Jason Dagit]

On Tue, Sep 30, 2008 at 12:51 AM, apfelmus <apfelmus at quantentunnel.de>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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080930/2640f1d4/attachment.htm