<div dir="ltr"><br><br><div class="gmail_quote">On Tue, Sep 30, 2008 at 12:51 AM, apfelmus <span dir="ltr"><<a href="mailto:apfelmus@quantentunnel.de">apfelmus@quantentunnel.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div class="Ih2E3d">Jason Dagit wrote:<br>
> Hello,<br>
><br>
> I recently had someone point me to this thread on LtU:<br>
> <a href="http://lambda-the-ultimate.org/node/2003" target="_blank">http://lambda-the-ultimate.org/node/2003</a><br>
><br>
> The main paper in the article is this one:<br>
> <a href="http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf" target="_blank">http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf</a><br>
><br>
> It leaves me with several questions:<br>
> 1) Are there are existing Haskell-ish implementations of the total<br>
> functional paradigm?<br>
<br>
</div>Agda?<br>
<br>
<a href="http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.HomePage" target="_blank">http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.HomePage</a><br>
<br>
It seems to me that dependent types are best for ensuring totality.</blockquote><div><br>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?<br>
</div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><br><div class="Ih2E3d">
> 2) Could we restructure Haskell so that it comes in 3 layers, total<br>
> functional core, lazy pure partial functional middle, and IO outer layer?<br>
<br>
</div>The IO layer can be interpreted as "co-total", i.e. as codata.<br>
Basically, this means that it's guaranteed that the program prints or<br>
reads something after a finite amount of time and does not loop forever<br>
without doing anything.</blockquote><div><br>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.<br>
<br>Thanks,<br>Jason<br></div></div></div>