[Agda] How safe is Type:Type?

[Michael Shulman]

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