[Agda] How safe is Type:Type?

[Matthieu Sozeau]

Indeed in Coq we statically compute the possible recursive calls at the
definition of the inductive type, independently of its use. In this case
Agda is "fooled" because it thinks that [f] is a valid subterm (of type
[D]) of [x : D], while Coq simply doesn't categorize [f] as a subterm when
checking the guardedness/structural recursion criterion.

On Thu, Mar 9, 2017 at 11:37 AM Michael Shulman <shulman at sandiego.edu>
wrote:

> Pardon my ignorance, but I don't understand why anyone would accept the
> definition of "empty".  The datatype D is not recursive; it's basically of
> the form
>
> data D : Set where
>   c : X -> D
>
> for some fixed type X, which just happens to be large in this case.  So
> its induction principle says that we get a map D -> Y whenever we have a
> map X -> Y.  What justifies any sort of recursive call?
>
>
> On Wed, Mar 8, 2017 at 2:59 PM, Stefan Monnier <monnier at iro.umontreal.ca>
> wrote:
>
> >   data D : Set where
> >     c : (f : (A : Set) → A → A) → D
> >   -- Structural recursion with  f args < c f  is no longer valid.
> >   -- We should not be able to demonstrated that D is empty.
>
> Coq lets us define this datatype (in Prop).
>
> >   empty : D → ⊥
> >   empty (c f) = empty (f D (c f))
>
> But rejects this definition:
>
>     Error:
>     Recursive definition of empty is ill-formed.
>     In environment
>     empty : D -> False
>     x : D
>     f : forall A : Prop, A -> A
>     Recursive call to empty has principal argument equal to
>     "f D (c f)" instead of a subterm of "x".
>     Recursive definition is:
>     "fun x : D => match x with
>                   | c f => empty (f D (c f))
>                   end".
>
> Not sure exactly what is the rule they use to decide whether a recursive
> call is considered as valid structural recursion.  I suspect it depends
> on the notion of a "large inductive type" or something along these lines.
>
>
>         Stefan
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
> _______________________________________________
> 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/20170309/b39d7437/attachment.html>