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