[Agda] defining coinductive types

[Aaron Stump]

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>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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131218/d528e279/attachment-0001.html