[Agda] How safe is Type:Type?

[Jesper Cockx]

Right now, Agda considers all arguments of a constructor to be strongly
rigid, even the non-recursive ones (i.e. the ones whose type doesn't
mention the datatype). But this is not justified by the recursion principle
for the datatype: you can only recurse on arguments that are in a recursive
position. I don't know how this is enforced in Coq, but here's how I would
do it in Agda. First, you need to know for a given constructor which of its
arguments are recursive and which ones are not, by looking at the type of
the constructor. Then, when you do free variable analysis (in
Agda.TypeChecking.Free.Lazy), you only mark variables as strongly rigid if
they occur in a *recursive* argument of a constructor. This should be
enough to rule out your example (since the argument of c isn't recursive),
and I think would also solve the problem in general.

I'm tempted to try to implement this myself, but I probably won't do it
until next week. So if you want to try it, go ahead.

-- Jesper

On Thu, Mar 9, 2017 at 3:35 PM, Andreas Abel <abela at chalmers.se> wrote:

> 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/
> _______________________________________________
> 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/931c2af8/attachment.html>