[Agda] Positive but not strictly positive types

[Dan Doel]

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

> > But with non-strict positive types you can eliminate the zip penalty.
> I've been thinking for quite a long time, that it's not even possible.
> Is your technique described somewhere?
>
> [1] http://okmij.org/ftp/Haskell/LC_Pnum.lhs
>

​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.

​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. :)

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