<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
This encoding is due to Michel Parigot, in "Programming with Proofs:
A second order type theory":<br>
<br>
<a class="moz-txt-link-freetext" href="http://link.springer.com/chapter/10.1007%2F3-540-19027-9_10">http://link.springer.com/chapter/10.1007%2F3-540-19027-9_10</a><br>
<br>
For a freely available and probably more accessible presentation,
see Herman Geuvers's "The Church-Scott representation of inductive
and coinductive data"<br>
<br>
<a class="moz-txt-link-freetext" href="http://www.cs.ru.nl/~herman/PUBS/ChurchScottDataTypes.pdf">http://www.cs.ru.nl/~herman/PUBS/ChurchScottDataTypes.pdf</a><br>
<br>
Geuvers extends the encoding, which he calls the Church-Scott
encoding (I prefer the term Parigot encoding, in honor of the
inventor in the case of natural numbers), to coinductive types,
which is quite interesting.<br>
<br>
Cheers,<br>
Aaron<br>
<br>
<div class="moz-cite-prefix">On 04/10/2015 09:48 PM, Dan Doel wrote:<br>
</div>
<blockquote
cite="mid:CAHEA9tN4tOMjqcq4VECQG64Uv9J_JsSjqYK3e_bUJwswrWXX8g@mail.gmail.com"
type="cite">
<div dir="ltr">
<div class="gmail_extra">On Fri, Apr 10, 2015 at 10:03 PM,
effectfully <span dir="ltr"><<a moz-do-not-send="true"
href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>></span>
wrote:<br>
<div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex"><span
class="">
> But with non-strict positive types you can
eliminate the zip penalty.<br>
</span>I've been thinking for quite a long time, that it's
not even possible.<br>
Is your technique described somewhere?<br>
<br>
[1] <a moz-do-not-send="true"
href="http://okmij.org/ftp/Haskell/LC_Pnum.lhs"
target="_blank">http://okmij.org/ftp/Haskell/LC_Pnum.lhs</a><br>
</blockquote>
</div>
<br>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif">It's not
described anywhere that I know of. It was shown to me by
someone else---a person who goes as ski in #haskell (and
other channels) on freenode, whose real name I don't know
off hand, and who I assume came up with the idea in the
first place.</div>
<br>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif">I haven't
done much investigation of what else you can do with this
sort of thing. I doubt it gets you O(1) tail, for instance.
The key seems to be that zip has to tear down and build
everything anyway, this just ensures you build only the
output, instead of rebuilding one of the inputs many times.
Mostly I keep it in the back of my mind for when someone
asks why you might want non-strict positive types. :)<br>
<br>
</div>
<div class="gmail_default"
style="font-family:arial,helvetica,sans-serif">-- Dan<br>
</div>
<br>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>