[Agda] How safe is Type:Type?
Gabriel Scherer
gabriel.scherer at gmail.com
Thu Mar 9 16:46:56 CET 2017
On Thu, Mar 9, 2017 at 9:55 AM, Jesper Cockx <Jesper at sikanda.be> wrote:
> 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.
Is that not too coarse-grained? It is the type occurrences within each
consturctor
type that are recursive or not, so I would expect different neutral
terms on the same
constructor variable head to be safe or not.
If I had for example (pardon the non-standard syntax)
c : (f : (A : Set) → A → { fst: A; snd: D })) → D
Matching on (c f), I would expect (fst (f T v)) to be a valid
structurally recursive position,
but (snd (f D (c f))) to be rejected.
On Thu, Mar 9, 2017 at 9:55 AM, Jesper Cockx <Jesper at sikanda.be> wrote:
> 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
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
More information about the Agda
mailing list