The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Thanks Jason, Matthieu, Gabriel and Bas.

Gabriel: We ran into the same issue. Universe polymorphism helped us remove most of our code duplication when we were just defining first 3 universes. Even with IR, I would suspect that one cannot define the universes indexed by naturals if those universes themselves have types defined by an IR construct. I mainly like IR because it simplifies my definitions.

Jason and Matthieu:

In our case, the function part calls itself recursively only on structural subterms in the type being simultaneously constructed. I think this suffices for other constructions like universes in Martin Löf's intensional theory. I guess Coq already has enough machinery for doing this kind of termination analysis. However, some more checks are required on the function. As Jason mentioned, the following should be illegal:

Inductive Bad := Build_bad : bad_fix -> Bad 

with Fixpoint bad_fix : Type := Bad -> unit.

I think it might be good enough for most applications if we disallow the type being simultaneously defined to appear in the body of the function. (Although Agda is smart enough to allow:)

mutual

  data Bad : Set where

    c : (bad_fix 0) → Bad

  

  bad_fix : ℕ → Set

  bad Data.Nat.zero fix = ℕ

  bad Data.Nat.suc n fix = Bad 

The trickier part is checking (half) positivity of the inductive part. http://en.wikipedia.org/wiki/Induction-recursion_(type_theory) does a great job of explaining how the rules for checking the inductive part need to change when implementing IR.

I think that the only addition in IR is that function calls are now legal at all positions. (In mutually inductive definitions, they were illegal at negative positions). 

I'm sorry that this is a hand-wavy proposal based on my intuitive understanding of IR. If these rules can be implemented "quickly" and encompass many practical applications, I will try to justify their soundness using the formal axiomatizations in Dybjer's papers.

Matthieu : Using Prop or making Set impredicative will work, but we prefer to remain in the predicative world as much as possible. It would be nice if there was a --no-prop switch so that we could confidently claim that all our definitions are predicative.

Jason: http://adam.chlipala.net/cpdt/html/InductiveTypes.html shows an example of an Inductive Type which violates the strict positivity condition and enables us to write a non-terminating function on it (search for uhoh). Strict positivity is sufficient but not necessary for Inductive types to be well defined. Nuprl has a more relaxed criteria. An Inductive types can be thought of as least fixpoint of a function from a universe to itself. Nuprl requires that this function be monotonous w.r.t the subtyping relation (http://nuprl.org/KB/show.php?ShowPub=Men88).

Strict positivity implies monotonocity, but the converse is not true. For example, Nuprl accepts an analog of the following Inductive type ot Coq:

Inductive Mono : Type :=

|u: Mono

|m : ((Mono -> nat) -> Mono) -> Mono.

However, I don't know of any practical use of Inductive types which are monotonous, but not strictly positive. Does anyone know about one?

Thanks,

Abhishek and Vincent

On Tue, Nov 12, 2013 at 6:12 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

Dear all,

  I've been thinking of adding IR to Coq for a while, but mainly thought about
the implementation issues (representation of mutual inductive/fixpoints and
positivity). I suspect it would not be too long to add it, as the change would
mainly impact the kernel entry point for declarations of inductives and not
change the representation of terms. Basically adding I and f would simultaneously
introduce an inductive and a constant in the environment, they would just
have to be grouped to allow simultaneous checking. The big engineering issue will
be positivity/termination checking indeed. I don't have time to implement
this now, but if you're willing to try it I'd be happy to help you Abhishek.
My (always optimistic) gut feeling is at least 6 weeks of full-time work for
one person not knowing the code previously, with safety checking taking most
of the time (and intelligence). I'm not very familiar with the theoretical
justifications, surely Dybjer's and Barras's work is reusable. One thing that
I'm not sure about is what form the fixpoints can take, i.e. do you need to
recognize a specific fix-match pattern or can allow free-form terms.

  On the related problem of encoding IR with inductives only, I guess with
polymorphic universes you will be able to apply the translation always but
of course you'll still be bumping the universe level, and indeed the translation
is heavy. Looking at it closely, it doesn't change the universe level if
your inductive is in Set and you have impredicative set though, right?
  I don't know about Prop and IR, but Capretta uses Prop in his encoding and
I don't see why it would cause any problem (but you never know until it's
been proved :).

  The universe polymorphism branch supports the use of a polymorphic
identity type instead of eq : A -> A -> Prop (in principle, in the Coq code).
E.g., I adapted discriminate etc to work with a different eq type (perhaps not
completely, it's untested). B. Barras also has some prototypical work on making
the base logic parametric in Coq, i.e. declaring type classes for different
logics, intuitionistic, classical, in Prop, in Set/Type. The tactics using
e.g. True would now take the truth value of the current Logic instance in the
context, which might happen to be unit.

  Given the interest on this and other features, a Coq Implementors Meeting seems
to really be in order!

Cheers,
-- Matthieu

On 12 nov. 2013, at 11:02, Gabriel Scherer <gabriel.scherer AT gmail.com> wrote:

> It's precisely when you have universes indexed by naturals that
> induction-recursion becomes useful. I think that for the purpose of
> convincing oneself that something is solid, one could decide to work
> only a bounded number of universe levels (say 3 universes; 2 universes
> is not quite enough to seriously study cumulativity for example), but
> I'm not sure how to do that without duplicating the inductive
> definition (which is a no-no).
>
>>> On Tue, Nov 12, 2013 at 10:11 AM, Jason Gross <jasongross9 AT gmail.com>
>>> wrote:
>>>> [previous messages inserted into bottom]
>>>> I would not be surprised if it took much longer than a few days, but
>>>> I've
>>>> never seriously worked on Coq.  I'd start by looking at where and how
>>>> "Inductive" is defined.  You could also look at the changes made in
>>>> https://github.com/barras/coq/tree/hit, where Bruno Barras implements a
>>>> "with paths := ..." and "fixmatch" primitives as a start of higher
>>>> inductive
>>>> types.  I suspect that the code you need to touch is similar to/near the
>>>> code that "with paths :=" modifies.
>>>>
>>>> Some issues to watch out for with trying to add induction-recursion to
>>>> Coq:
>>>> - Coq doesn't have "mutual" blocks, and "fix" is a special keyword that
>>>> lets
>>>> you mention the name of the function in it's body.  So you'll probably
>>>> need
>>>> to pull some hackery to get the types of the constructors to be allowed
>>>> to
>>>> mention the fixpoint, which can't be defined until the inductive
>>>> definition
>>>> is meaningful.
>>>> - Unlike Agda, Coq's termination checker is syntactic and simple; it
>>>> only
>>>> permits structural recursion (or well-founded recursion, if you write
>>>> your
>>>> own proofs), and requires that inductives be strictly positive.  For
>>>> example, you can't typecheck [Inductive Bad := Build_bad : (Bad -> unit)
>>>> ->
>>>> Bad.]; it errors with "Error: Non strictly positive occurrence of "Bad"
>>>> in
>>>> "(Bad -> unit) -> Bad"."  How do you plan to extend this rule to
>>>> induction-recursion?  I probably shouldn't be allowed to do "Inductive
>>>> Bad
>>>> := Build_bad : bad_fix -> Bad with Fixpoint bad_fix : Type := Bad ->
>>>> unit.]
>>>> or something silly like that.  So either you'll need to write a
>>>> termination
>>>> checker for Coq, which I think goes against it's philosophy, or you'll
>>>> need
>>>> a simple syntactic check that you can use to ensure termination and
>>>> positivity.   (I'm not sure what exactly goes wrong if you allow
>>>> non-positivity... perhaps it gives you some kind of impredicativity?)
>>>> - The upcoming version of Coq will mostly likely have full universe
>>>> polymorphism/typical ambiguity.  Are there any subtleties to inferring
>>>> and
>>>> assigning universes in the presence of induction-recursion?
>>>>
>>>> However, I'd be very, very interested to have induction recursion in
>>>> Coq,
>>>> especially if it meshes well with Bruno's higher inductive types; I've
>>>> been
>>>> itching to try out my understanding of computation rules for higher
>>>> inductive types with defining univalent universes by higher induction
>>>> recursion, and seeing if I could formalize a computational
>>>> interpretation of
>>>> univalence that way.  (I also think it'd be a nice feature to have in
>>>> general.)  But I'd be surprised if you could do it in a few days.
>>>>
>>>> With regard to Prop and IR, I'd be surprised if there was an
>>>> inconsistency
>>>> there, as long as the IR didn't allow you to do large elimination out of
>>>> prop, or anything like that.  At worst, you could just forbid Prop from
>>>> showing up in your inductive-recursive definitions (just do an
>>>> after-the-fact check to make sure the identifier doesn't show up in the
>>>> delta normal form), and then I'd be very surprised if you could get a
>>>> contradiction from this.
>>>> There is no way to disable prop, currently; for one, [eq] is in [Prop]
>>>> and
>>>> many of the tactics will raise errors or anomalies if you don't have [eq
>>>> :
>>>> forall A, A -> A -> Prop], [True : Prop], [False : Prop], etc.  (I tried
>>>> putting them in Set/Type, for HoTT, and ran into errors.)
>>>>
>>>> I hope this helps,
>>>> Jason