[Agda] How safe is Type:Type?

[Martin Escardo]

On 09/03/17 10:37, Michael Shulman 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?

In fact your type D is isomorphic to X, of course. And so can be empty
only if X is empty.

And the type X = ((A : Set) -> A -> A) is of course inhabited by the
(polymorphic) identity function.

So something seems to be wrong in the example given by Andreas.

Martin



> 
> On Wed, Mar 8, 2017 at 2:59 PM, Stefan Monnier <monnier at iro.umontreal.ca
> <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe