[Agda] Positive but not strictly positive types

[Aaron Stump]

This encoding is due to Michel Parigot, in "Programming with Proofs: A 
second order type theory":

http://link.springer.com/chapter/10.1007%2F3-540-19027-9_10

For a freely available and probably more accessible presentation, see 
Herman Geuvers's "The Church-Scott representation of inductive and 
coinductive data"

http://www.cs.ru.nl/~herman/PUBS/ChurchScottDataTypes.pdf

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.

Cheers,
Aaron

On 04/10/2015 09:48 PM, Dan Doel wrote:
> On Fri, Apr 10, 2015 at 10:03 PM, effectfully <effectfully at gmail.com 
> <mailto: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
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150411/9c227ef6/attachment.html