[Agda] How safe is Type:Type?
Andreas Abel
abela at chalmers.se
Thu Mar 9 16:05:29 CET 2017
On 09.03.2017 09:55, Jesper Cockx 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.
Sounds easy, but in Agda, "First" is hard to implement, since you can
have meta-variables everywhere. Thus, you cannot decide whether an
argument is recursive or not if there are metas left.
We can maybe approximate this by assuming the worst case. Maybe the
worst case is "non-recursive", thus the analysis could return either
"definitely recursive"
or
"don't know".
On 09.03.2017 09:55, Jesper Cockx 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
> <mailto: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>
> <mailto: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>
> <mailto: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>
> <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>>
> https://lists.chalmers.se/mailman/listinfo/agda
> <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>>
> https://lists.chalmers.se/mailman/listinfo/agda
> <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
> <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 <mailto:andreas.abel at gu.se>
> http://www.cse.chalmers.se/~abela/ <http://www.cse.chalmers.se/~abela/>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda
> <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/
More information about the Agda
mailing list