<div dir="ltr"><div class="gmail_extra">On Fri, Apr 10, 2015 at 7:35 PM, effectfully <span dir="ltr">&lt;<a 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">Dan Doel, then it&#39;s simpler to use Scott-encoded lists as an example:<br></blockquote><div><br><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;display:inline">​I thought Scott encoding was actually:<br><br>​</div> <div class="gmail_default" style="font-family:arial,helvetica,sans-serif;display:inline">​  newtype List a = Roll { case_ :: forall r. (a -&gt; List a -&gt; r) -&gt; r -&gt; r }<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;display:inline">​I.E. the one-step eliminator. Yours looks like the primitive recursive eliminator (instead of the structurally recursive one).<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;display:inline">The problem with the one-step eliminator is that it performs exactly like wired-in data types. So it&#39;s natural that zip is fine for those, because it&#39;s fine for data types. The interesting part is that Church encoding is _better_ than those at certain things. For instance, it fuses maps, so that &#39;map g . map f&#39; can be reduced to &#39;map (g . f)&#39; in a finite number of steps, but on a Scott lists, this doesn&#39;t even make sense, because &#39;map&#39; is an irreducible recursive definition.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;display:inline">I haven&#39;t thought about it a long time, but I expect the primitive recursive version also does not work like the Church version. Certainly it requires a recursive definition for map. And it seems that if you did anything taking advantage of the Scott-like part of it, the maps would not be fused for that. So if I zipped lists that had functions mapped over them, they wouldn&#39;t be fused. Perhaps I&#39;m wrong, though.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;display:inline">The point of the Church example is that zipping is the type of thing that you might think is part of the trade-off. I get better map for worse zip. But with non-strict positive types you can eliminate the zip penalty.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;display:inline">-- Dan<br></div></div></div></div></div>