<div dir="ltr"><div class="gmail_extra">On Fri, Apr 10, 2015 at 7:35 PM, effectfully <span dir="ltr"><<a 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">Dan Doel, then it'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 -> List a -> r) -> r -> 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's natural that zip is fine for those, because it'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 'map g . map f' can be reduced to 'map (g . f)' in a finite number of steps, but on a Scott lists, this doesn't even make sense, because 'map' is an irreducible recursive definition.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;display:inline">I haven'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't be fused. Perhaps I'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>