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