[Agda] Agda's coinduction incompatible with initial algebras

[Nicolas Pouillard]

On Thu, Oct 6, 2011 at 9:15 PM, Dan Doel <dan.doel at gmail.com> wrote:
> On Thu, Oct 6, 2011 at 3:07 AM, Thorsten Altenkirch <txa at cs.nott.ac.uk> wrote:
>>> I don't think this is true if you want a (typical) set theoretic
>>> semantics. Fixed points of functors like:
>>>
>>>    K R A = (A -> R) -> R
>>>
>>> only exist in categories of domains and the like as I recall (and my
>>> skimming of Matthes' paper didn't suggest any different). Assuming
>>> anyone cares about that.
>>
>> We should stick to things we understand intuitively.
>
> I frequently don't find the set theoretic models of type theoretic
> features particularly intuitive. Should we get rid of
> induction-recursion? I don't have any intuition for Mahlo cardinals.
>
>> Anyway, who needs non-strict positive definitions?

This september at ICFP 2011, the paper «A Hierarchy of Mendler style
Recursion Combinators: Taming Inductive Datatypes with Negative
Occurrences» has been presented.

I did not studied the paper but this definitely relevant to the discussion.

URL: http://kyagrd.dyndns.org/wiki/MendlerStyleRecursionCombinators

-- 
Nicolas Pouillard
http://nicolaspouillard.fr