[Agda] Positive but not strictly positive types

[Dan Doel]

On Fri, Apr 10, 2015 at 7:35 PM, effectfully <effectfully at gmail.com> wrote:

> Dan Doel, then it's simpler to use Scott-encoded lists as an example:
>

​I thought Scott encoding was actually:

​

​  newtype List a = Roll { case_ :: forall r. (a -> List a -> r) -> r -> r }

​I.E. the one-step eliminator. Yours looks like the primitive recursive
eliminator (instead of the structurally recursive one).

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.

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.

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.

-- Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150410/57b3e236/attachment-0001.html