[Agda] How safe is Type:Type?
Matthieu Sozeau
mattam at mattam.org
Fri Mar 10 10:25:03 CET 2017
Hi,
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.
-- Matthieu
On Thu, Mar 9, 2017 at 5:24 PM Jesper Cockx <Jesper at sikanda.be> wrote:
> Huh, you're right. I didn't know Agda accepts the definition
>
> data D : Set where
> c : (f : (A : Set) → A → A × D) → D
>
> but apparently it does. It also accepts
>
> data D' : Set where
> c : List D' → D'
>
> 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.
>
> -- Jesper
>
>
>
> On Thu, Mar 9, 2017 at 4:46 PM, Gabriel Scherer <gabriel.scherer at gmail.com
> > wrote:
>
> 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
> >
>
>
> _______________________________________________
> 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/20170310/3da784c0/attachment.html>
More information about the Agda
mailing list