<div dir="ltr"><div>Huh, you're right. I didn't know Agda accepts the definition<br><br><div style="margin-left:40px">data D : Set where<br> c : (f : (A : Set) → A → A × D) → D<br><br></div>but apparently it does. It also accepts<br><br><div style="margin-left:40px">data D' : Set where<br> c : List D' → D'<br><br></div>in which case you're allowed to make recursive calls on any element in the list, even though the first argument of list cons is not recursive. This definitely is a harder problem than it seems at first. Now I'm also wondering how Coq computes the set of valid recursive calls.<br><br></div>-- Jesper<br><div><div><div><br><div><div><br></div></div></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Mar 9, 2017 at 4:46 PM, Gabriel Scherer <span dir="ltr"><<a href="mailto:gabriel.scherer@gmail.com" target="_blank">gabriel.scherer@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Thu, Mar 9, 2017 at 9:55 AM, Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>> wrote:<br>
> First, you need to know for a given constructor which of its<br>
> arguments are recursive and which ones are not, by looking at the type of<br>
> the constructor.<br>
<br>
</span>Is that not too coarse-grained? It is the type occurrences within each<br>
consturctor<br>
type that are recursive or not, so I would expect different neutral<br>
terms on the same<br>
constructor variable head to be safe or not.<br>
<br>
If I had for example (pardon the non-standard syntax)<br>
<br>
c : (f : (A : Set) → A → { fst: A; snd: D })) → D<br>
<br>
Matching on (c f), I would expect (fst (f T v)) to be a valid<br>
structurally recursive position,<br>
but (snd (f D (c f))) to be rejected.<br>
<div class="HOEnZb"><div class="h5"><br>
On Thu, Mar 9, 2017 at 9:55 AM, Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>> wrote:<br>
> Right now, Agda considers all arguments of a constructor to be strongly<br>
> rigid, even the non-recursive ones (i.e. the ones whose type doesn't mention<br>
> the datatype). But this is not justified by the recursion principle for the<br>
> datatype: you can only recurse on arguments that are in a recursive<br>
> position. I don't know how this is enforced in Coq, but here's how I would<br>
> do it in Agda. First, you need to know for a given constructor which of its<br>
> arguments are recursive and which ones are not, by looking at the type of<br>
> the constructor. Then, when you do free variable analysis (in<br>
> Agda.TypeChecking.Free.Lazy), you only mark variables as strongly rigid if<br>
> they occur in a *recursive* argument of a constructor. This should be enough<br>
> to rule out your example (since the argument of c isn't recursive), and I<br>
> think would also solve the problem in general.<br>
><br>
> I'm tempted to try to implement this myself, but I probably won't do it<br>
> until next week. So if you want to try it, go ahead.<br>
><br>
> -- Jesper<br>
><br>
> On Thu, Mar 9, 2017 at 3:35 PM, Andreas Abel <<a href="mailto:abela@chalmers.se">abela@chalmers.se</a>> wrote:<br>
>><br>
>> Yes, that's the point. Coq has to be more careful about the structural<br>
>> ordering since it supports impredicativity. (The example is taken from<br>
>> Coquand 1992, Pattern matching with dependent types, where Thierry already<br>
>> points out the problem.)<br>
>><br>
>> Agda is build on the assumption of predicativity, thus<br>
>><br>
>> c f > f args<br>
>><br>
>> is ok with any constructor c, be it recursive or not.<br>
>><br>
>> When you leave the safe ground of predicativity via --type-in-type, things<br>
>> might go wrong in an unexpected way.<br>
>><br>
>> My long term-plan is to replace the structural termination check by<br>
>> type-based termination, which does not exhibit the pathological behavior<br>
>> exploited here. Thus, I am not so pressed to get rid of it.<br>
>><br>
>> However, if someone can point me to the analysis Coq does on its data<br>
>> types for the sake of structural recursion, it may be worthwile to think how<br>
>> to integrate this into Agda.<br>
>><br>
>> Best,<br>
>> Andreas<br>
>><br>
>> On 09.03.2017 05:52, Matthieu Sozeau wrote:<br>
>>><br>
>>> Indeed in Coq we statically compute the possible recursive calls at the<br>
>>> definition of the inductive type, independently of its use. In this case<br>
>>> Agda is "fooled" because it thinks that [f] is a valid subterm (of type<br>
>>> [D]) of [x : D], while Coq simply doesn't categorize [f] as a subterm<br>
>>> when checking the guardedness/structural recursion criterion.<br>
>>><br>
>>> On Thu, Mar 9, 2017 at 11:37 AM Michael Shulman <<a href="mailto:shulman@sandiego.edu">shulman@sandiego.edu</a><br>
>>> <mailto:<a href="mailto:shulman@sandiego.edu">shulman@sandiego.edu</a>>> wrote:<br>
>>><br>
>>> Pardon my ignorance, but I don't understand why anyone would accept<br>
>>> the definition of "empty". The datatype D is not recursive; it's<br>
>>> basically of the form<br>
>>><br>
>>> data D : Set where<br>
>>> c : X -> D<br>
>>><br>
>>> for some fixed type X, which just happens to be large in this case.<br>
>>> So its induction principle says that we get a map D -> Y whenever we<br>
>>> have a map X -> Y. What justifies any sort of recursive call?<br>
>>><br>
>>><br>
>>> On Wed, Mar 8, 2017 at 2:59 PM, Stefan Monnier<br>
>>> <<a href="mailto:monnier@iro.umontreal.ca">monnier@iro.umontreal.ca</a> <mailto:<a href="mailto:monnier@iro.umontreal.ca">monnier@iro.umontreal.<wbr>ca</a>>> wrote:<br>
>>><br>
>>> > data D : Set where<br>
>>> > c : (f : (A : Set) → A → A) → D<br>
>>> > -- Structural recursion with f args < c f is no longer<br>
>>> valid.<br>
>>> > -- We should not be able to demonstrated that D is empty.<br>
>>><br>
>>> Coq lets us define this datatype (in Prop).<br>
>>><br>
>>> > empty : D → ⊥<br>
>>> > empty (c f) = empty (f D (c f))<br>
>>><br>
>>> But rejects this definition:<br>
>>><br>
>>> Error:<br>
>>> Recursive definition of empty is ill-formed.<br>
>>> In environment<br>
>>> empty : D -> False<br>
>>> x : D<br>
>>> f : forall A : Prop, A -> A<br>
>>> Recursive call to empty has principal argument equal to<br>
>>> "f D (c f)" instead of a subterm of "x".<br>
>>> Recursive definition is:<br>
>>> "fun x : D => match x with<br>
>>> | c f => empty (f D (c f))<br>
>>> end".<br>
>>><br>
>>> Not sure exactly what is the rule they use to decide whether a<br>
>>> recursive<br>
>>> call is considered as valid structural recursion. I suspect it<br>
>>> depends<br>
>>> on the notion of a "large inductive type" or something along<br>
>>> these lines.<br>
>>><br>
>>><br>
>>> Stefan<br>
>>><br>
>>> ______________________________<wbr>_________________<br>
>>> Agda mailing list<br>
>>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><wbr>><br>
>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
>>><br>
>>><br>
>>> ______________________________<wbr>_________________<br>
>>> Agda mailing list<br>
>>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><wbr>><br>
>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
>>><br>
>>><br>
>>><br>
>>> ______________________________<wbr>_________________<br>
>>> Agda mailing list<br>
>>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
>>><br>
>><br>
>><br>
>> --<br>
>> Andreas Abel <>< Du bist der geliebte Mensch.<br>
>><br>
>> Department of Computer Science and Engineering<br>
>> Chalmers and Gothenburg University, Sweden<br>
>><br>
>> <a href="mailto:andreas.abel@gu.se">andreas.abel@gu.se</a><br>
>> <a href="http://www.cse.chalmers.se/~abela/" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~<wbr>abela/</a><br>
>> ______________________________<wbr>_________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
><br>
><br>
><br>
> ______________________________<wbr>_________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
><br>
</div></div></blockquote></div><br></div>