<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">&lt;<a moz-do-not-send="true"
              href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>&gt;</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="">
                &gt; 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 rebuild​ing 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>