[Agda] How safe is Type:Type?

[Andreas Abel]

Yes, that's the point.  Coq has to be more careful about the structural 
ordering since it supports impredicativity.  (The example is taken from 
Coquand 1992, Pattern matching with dependent types, where Thierry 
already points out the problem.)

Agda is build on the assumption of predicativity, thus

   c f > f args

is ok with any constructor c, be it recursive or not.

When you leave the safe ground of predicativity via --type-in-type, 
things might go wrong in an unexpected way.

My long term-plan is to replace the structural termination check by 
type-based termination, which does not exhibit the pathological behavior 
exploited here.  Thus, I am not so pressed to get rid of it.

However, if someone can point me to the analysis Coq does on its data 
types for the sake of structural recursion, it may be worthwile to think 
how to integrate this into Agda.

Best,
Andreas

On 09.03.2017 05:52, Matthieu Sozeau wrote:
> 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
> <mailto: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 <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
>
>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto: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
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/