[Agda] defining coinductive types
aaron-stump at uiowa.edu
Wed Dec 18 18:22:34 CET 2013
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
On Wed, Dec 18, 2013 at 11:14 AM, Wojciech Jedynak <wjedynak at gmail.com>wrote:
> > 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:
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda