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