[Agda] defining coinductive types

[Thierry Coquand]

 At least in an impredicative metatheory, the usual normalization argument should extend
to the addition of such positive recursive types in Agda (using Tarski's fixed point theorem
to define the computability at these types).

 Best regards,
 Thierry

PS: This would be however incompatible with the addition of an impredicative universe U,
since one can then form

 R = mu X. (X-> U) -> U

and derive a contradiction from this following Reynolds' proof that there is no set theoretical
model of system F.

On Dec 18, 2013, at 6:22 PM, Aaron Stump wrote:

Dear Wojtek,

Yes, I know about this example for recursive types which contain negative occurrences of the recursively defined type.  But I am asking about positive but not strictly positive recursive types.  An example is a type like the one Nils mentioned:

μA.∀R. (μX. (A → R) + X) → R

Here, the type variable A occurs to the left of an even number of arrows.  This makes it positive (the even number of negations cancel out), but not strictly positive.

Cheers,
Aaron




On Wed, Dec 18, 2013 at 11:14 AM, Wojciech Jedynak <wjedynak at gmail.com<mailto:wjedynak at gmail.com>> wrote:
Hello,

> Ok, I see.  Is it known that supporting non-strictly positive types would
> have bad consequences in Agda?  Not that I am suggesting it -- I am just
> curious about what might be possible.

Yes, it's possible to write a non-terminating expression using such a
type. For instance, take a look here:
<http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.BadInHaskell>

Best,
Wojtek

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto: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/20131218/163ea577/attachment-0001.html