8 views

Skip to first unread message

Sep 16, 2013, 4:45:12 AM9/16/13

to homotopyt...@googlegroups.com

Last semester at IAS there was much discussion about extending type

theory with "questionable" judgmental equalities, such as

extensionality for natural numbers. What are some other examples that

would be desirable to have? I am asking so that it is easier to think

about proof assistants that would support such black magic.

With kind regards,

Andrej

theory with "questionable" judgmental equalities, such as

extensionality for natural numbers. What are some other examples that

would be desirable to have? I am asking so that it is easier to think

about proof assistants that would support such black magic.

With kind regards,

Andrej

Sep 16, 2013, 8:50:34 AM9/16/13

to Andrej Bauer, homotopyt...@googlegroups.com

definitional computation rules for the generating paths in HITs.

S

> --

> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.

> For more options, visit https://groups.google.com/groups/opt_out.

S

> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.

> For more options, visit https://groups.google.com/groups/opt_out.

Sep 16, 2013, 10:58:53 AM9/16/13

to Steve Awodey, Andrej Bauer, homotopyt...@googlegroups.com

I'd be interested in seeing the following as judgemental equalities:

A generalized generalized eta rule that [match] commutes with any function which is polymorphic over the indices of the inductive data type. So, for example, with [paths] which has two parameters ([A : Type] and [x : A]) and one index (of type A), the rule is

∀ A (x y : A) (P : ∀ a, x = a → Type) (f : ∀ a (p : x = a), P a p) (p : x = y),

f _ p

= match p as p0 in (_ = y0) return (P y0 p0) with

| idpath ⇒ f _ idpah

end.

and for [JMeq], the rule is

∀ A (x : A) (P : ∀ B (b : B), JMeq x b → Type) (f : ∀ B (y : B) (p : JMeq x y) → P B y p) B (y : B) (p : JMeq x y),

f _ _ p

= match p as p0 in (@JMeq _ _ B0 y0) return (P B0 y0 p0) with

| JMeq_refl ⇒ f _ _ JMeq_refl

end.

and for [sum], the rule is

∀ A B (P : A + B → Type) (f : ∀ x, P x) (x : A + B),

f x

= match x as x0 return P x0 with

| inl a ⇒ f (inl a)

| inr b ⇒ f (inr b)

end.

By combining the case that [f] is a constructor applied to projections with the case that [f] is the identity, I think this rule suffices to obtain eta for records.

(I shudder a bit to think how hard this would be make normalizing.) (I've submitted a feature request for this for Coq, at https://coq.inria.fr/bugs/show_bug.cgi?id=3119)

----------------------

[transport_compose : ∀ {A B x y} (P : B → Type) (f : A → B) (p : x = y) (z : P (f x)), transport (fun x0 => P (f x0)) p z = transport P (ap f p) z], or, in [match]es,

match p in (_ = x0) return (P (f x0)) with

| idpath => z

end

= match (match p in (_ = x0) return (f x = f x0) with idpath => idpath end) in (_ = fx0) return (P fx0) with

| idpath => z

end

----------------------

I'd also like to see a generalization of transport_compose, which I haven't figured out the details of yet, which makes [inverse (inverse p) = p] a judgemental equality for all paths p.

----------------------

The following (partial) computation rule for matching on higher inductive types:

Given a higher inductive type [T] and a path constructor [p : a = b], any match of the form

match p in (_ = y) return (P (match y with a => c | b => d | p => f end)) with

| idpath => g

end

should be convertible with

match f in (_ = y) return (P y) with

| idpath => g

end

In terms of [transport : ∀ {A} (P : A → Type) {x y} (p : x = y), P x → P y], this says that

transport (fun y : T => P (T_elim (a_case := c) (b_case := d) (p_case := f) y) p

should be convertible with

transport (fun y => P y) f

----------------------

I might like some sort of judgemental rule about what to do if the argument to the return clause of a match/the argument to the first non-implicit argument to transport is used multiple times, as in "transport (fun y => y x = y z) ...", and how to split this up into multiple nested matches over the same path. I wonder if something like this would make, e.g., "projT1_path_sigma : forall {A} {P : A -> Type} {u v : exists x, P x} (p : u .1 = v .1) (q : transport P p u .2 = v .2), (path_sigma P u v p q) ..1 = p" a judgemental equality. But I haven't thought about this one enough to say much.

-Jason

Sep 16, 2013, 11:18:58 AM9/16/13

to Jason Gross, Steve Awodey, Andrej Bauer, homotopyt...@googlegroups.com

A while ago, Vladimir sent an email to the Coq mailing list containing

several interesting examples of "crazy" definitional equalities, for

instance

(A × Unit) = A

(Unit -> A) = A

We can invent more like that, for instance (Empty -> A) = Unit, or

(Bool -> Bool) = (Bool × Bool).

Guillaume

2013/9/16 Jason Gross <jason...@gmail.com>:

several interesting examples of "crazy" definitional equalities, for

instance

(A × Unit) = A

(Unit -> A) = A

We can invent more like that, for instance (Empty -> A) = Unit, or

(Bool -> Bool) = (Bool × Bool).

Guillaume

2013/9/16 Jason Gross <jason...@gmail.com>:

Sep 16, 2013, 11:42:22 AM9/16/13

to Guillaume Brunerie, Jason Gross, Steve Awodey, Andrej Bauer, homotopyt...@googlegroups.com

On Mon, Sep 16, 2013 at 8:18 AM, Guillaume Brunerie

<guillaume...@gmail.com> wrote:

> (A × Unit) = A

> (Unit -> A) = A

Personally, my initial reaction is that equalities of this sort would
<guillaume...@gmail.com> wrote:

> (A × Unit) = A

> (Unit -> A) = A

*not* be "desirable". I feel like they would probably subvert some of

the value of type theory as an organizing structure for mathematics.

One which hasn't been mentioned yet, though, is judgmental univalence:

Id_Type(A,B) = Equiv(A,B)

and similarly, judgmental funext:

Id_{A\to B)(f,g) = Pi_{a:A} Id_B(fa,ga)

and so on for a lot of the other theorems in chapter 2 (including I

think some of Jason's proposals). These go along with the expectation

of a "computational" meaning of HoTT.

Sep 16, 2013, 11:51:40 AM9/16/13

to Michael Shulman, Guillaume Brunerie, Jason Gross, Andrej Bauer, homotopyt...@googlegroups.com

right - that's what makes them "crazy".

Sep 16, 2013, 11:57:19 AM9/16/13

to Michael Shulman, Guillaume Brunerie, Jason Gross, Steve Awodey, Andrej Bauer, homotopyt...@googlegroups.com

Regarding Michael's examples, I guess I would have expected that in a computationally adequate system, there would be coercions between the types on either side that would judgmentally be inverses, rather than that the types would be judgmentally equal.

Sep 16, 2013, 12:01:25 PM9/16/13

to Michael Shulman, Jason Gross, Steve Awodey, Andrej Bauer, homotopyt...@googlegroups.com

On 2013/9/16 Michael Shulman <shu...@sandiego.edu> wrote:

> On Mon, Sep 16, 2013 at 8:18 AM, Guillaume Brunerie

> <guillaume...@gmail.com> wrote:

>> (A × Unit) = A

>> (Unit -> A) = A

>

> Personally, my initial reaction is that equalities of this sort would

> *not* be "desirable". I feel like they would probably subvert some of

> the value of type theory as an organizing structure for mathematics.

I agree with you, but isn’t that precisely what Andrej is looking for
> On Mon, Sep 16, 2013 at 8:18 AM, Guillaume Brunerie

> <guillaume...@gmail.com> wrote:

>> (A × Unit) = A

>> (Unit -> A) = A

>

> Personally, my initial reaction is that equalities of this sort would

> *not* be "desirable". I feel like they would probably subvert some of

> the value of type theory as an organizing structure for mathematics.

(he said "crazy" judgemental equalities)? In my opinion, having a type

theory where type checking is not decidable is not desirable already

anyway and I think Andrej’s question is more about judgemental

equalities that do not preserve decidability of type checking in

general.

For computation rules of HITs or judgemental univalence, there is some

hope that we won’t need any black magic there because they should be

part of the computational interpretation of HoTT (which should have

decidable type checking).

For extensionality for natural numbers, as far as I understand we

cannot hope to have decidable type checking so we have to use the kind

of black magic Andrej is talking about.

Guillaume

Sep 16, 2013, 2:13:18 PM9/16/13

to Guillaume Brunerie, Jason Gross, Steve Awodey, Andrej Bauer, homotopyt...@googlegroups.com

His subject line said "crazy", but the text of his email asked "What

are some other examples that would be desirable to have?"

On Mon, Sep 16, 2013 at 9:01 AM, Guillaume Brunerie
Sep 16, 2013, 3:26:07 PM9/16/13

to Michael Shulman, Guillaume Brunerie, Steve Awodey, Andrej Bauer, homotopyt...@googlegroups.com

Generalizing the idea of equality reflection for nat, it might be interesting/useful to have a built-in type of "types with decidable equality", and then grant equality reflection for anything of that type. Perhaps it should be possible to construct such a type by giving a type together with a function that decides equality on that type.

More decidably, it might be nice to be able declare that some finite set of symbols (e.g., "+", "*", "-", "S", "O") are mutually decidable, provide a normalizer for terms which use only those symbols (and possibly have to proof the relevant features of your normalization procedure so that it plays well with the rest of the kernel), and then get equality reflection for any terms that normalize to the same thing. (I think I might have gotten this idea from Paolo Capriotti, whom I think mentioned to me at OPLSS the suggestion that the typechecker has a ring solver built into it, and any equations this solver can solve can be taken as judgemental.)

-Jason

Sep 16, 2013, 5:23:01 PM9/16/13

to HomotopyT...@googlegroups.com

On 16/09/13 20:26, Jason Gross wrote:

That one sounds dangerous. Given any a:A, the typeï¿½ Sigma (b : A). a = bï¿½ trivially has decidable equality, but you don't want to grant equality reflection to it: If you make (a,refl) and (b,p) judgmentally equal, you also make their first projection judgmentally equal. I learnt this argument from Peter L in a similar discussion.

The other ideas sound interesting though.

Nicolai

Generalizing the idea of equality reflection for nat, it might be interesting/useful to have a built-in type of "types with decidable equality", and then grant equality reflection for anything of that type. ï¿½Perhaps it should be possible to construct such a type by giving a type together with a function that decides equality on that type.

That one sounds dangerous. Given any a:A, the typeï¿½ Sigma (b : A). a = bï¿½ trivially has decidable equality, but you don't want to grant equality reflection to it: If you make (a,refl) and (b,p) judgmentally equal, you also make their first projection judgmentally equal. I learnt this argument from Peter L in a similar discussion.

The other ideas sound interesting though.

Nicolai

More decidably, it might be nice to be able declare that some finite set of symbols (e.g., "+", "*", "-", "S", "O") are mutually decidable, provide a normalizer for terms which use only those symbols (and possibly have to proof the relevant features of your normalization procedure so that it plays well with the rest of the kernel), and then get equality reflection for any terms that normalize to the same thing. ï¿½(I think I might have gotten this idea fromï¿½Paolo Capriotti, whom I think mentioned to me at OPLSS the suggestion that the typechecker has a ring solver built into it, and any equations this solver can solve can be taken as judgemental.)

-Jasonï¿½

On Monday, September 16, 2013, Michael Shulman wrote:

His subject line said "crazy", but the text of his email asked "What

are some other examples that would be desirable to have?"

On Mon, Sep 16, 2013 at 9:01 AM, Guillaume Brunerie

<guillaume...@gmail.com> wrote:

> On 2013/9/16 Michael Shulman <shu...@sandiego.edu> wrote:

>> On Mon, Sep 16, 2013 at 8:18 AM, Guillaume Brunerie

>> <guillaume...@gmail.com> wrote:

>>> (A ï¿½ Unit) = A

>>> (Unit -> A) = A

>>

>> Personally, my initial reaction is that equalities of this sort would

>> *not* be "desirable". ï¿½I feel like they would probably subvert some of

>> the value of type theory as an organizing structure for mathematics.

>

> I agree with you, but isnï¿½t that precisely what Andrej is looking for

> (he said "crazy" judgemental equalities)? In my opinion, having a type

> theory where type checking is not decidable is not desirable already

> anyway and I think Andrejï¿½s question is more about judgemental

> equalities that do not preserve decidability of type checking in

> general.

> For computation rules of HITs or judgemental univalence, there is some

> hope that we wonï¿½t need any black magic there because they should be

> part of the computational interpretation of HoTT (which should have

> decidable type checking).

> For extensionality for natural numbers, as far as I understand we

> cannot hope to have decidable type checking so we have to use the kind

> of black magic Andrej is talking about.

>

> Guillaume

>

> --

> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.

> For more options, visit https://groups.google.com/groups/opt_out.

Sep 17, 2013, 7:02:39 AM9/17/13

to Jason Gross, Michael Shulman, Guillaume Brunerie, Steve Awodey, Andrej Bauer, homotopyt...@googlegroups.com

This is the sort of thing Pierre Yves Strub is trying to do with Coq

modulo theory.

http://pierre-yves.strub.nu/coqmt/

http://hal.inria.fr/inria-00583136/en/

The project may be somewhat stalled since he is now doing interesting

things related to security.

modulo theory.

http://pierre-yves.strub.nu/coqmt/

http://hal.inria.fr/inria-00583136/en/

The project may be somewhat stalled since he is now doing interesting

things related to security.

Sep 27, 2013, 10:30:00 AM9/27/13

to Bas Spitters, Michael Shulman, Guillaume Brunerie, Steve Awodey, Andrej Bauer, homotopyt...@googlegroups.com

In case any are interested: I was talking with Bruno, and after a bit of pushing, came up with the following generalization of transport_compose, which expresses that you can de-nest matches:

Set Implicit Arguments.

Section ex4.

Variable T0 : Type.

Variable T1 : Type.

Variables t0 t1 : T0.

Let T := @eq T0 t0. (* must be an inductive type with all parameters filled in, but no indices filled in *)

Variables f g : forall x : T0, T x -> T1.

Let P0 x H := @eq T1 (@f x H). (* must end up with an inductive type with all parameters but no indices filled in; must quantify over a [T _], and the arguments to it *)

Let P x H := @P0 x H (@g x H). (* we get to fill in the indices for [P0] with whatever expression of [x] and [H] we like *)

Variable Q : forall x H y, @P0 x H y -> Type. (* must take as arguments all arguments to [P0], and all parameters to the relevant inductive type *)

Goal forall (x : T t1) (y : @P t0 eq_refl) (z : @Q t1 x (@f t1 x) eq_refl),

match (match x as x' in (_ = u) return @P u x' with

| eq_refl => y

end) as x' in (_ = Px') return (@Q t1 x Px' x') with

| eq_refl => z

end

= match x as x' in (_ = u) return @Q u x' (@f u x') eq_refl

-> @Q u x' (@g u x') (match x' as x'' in (_ = u') return (@P u' x'') with

| eq_refl => y

end) with

| eq_refl => fun z => match y as y' in (_ = u) return @Q t0 eq_refl u y' with

| eq_refl => z

end

end z.

Proof.

compute in *; clear.

destruct x.

intros.

destruct y.

reflexivity.

Qed.

End ex4.

It might not be confluent, or easy to turn into a reduction rule, though.

-Jason

Oct 8, 2013, 6:13:30 PM10/8/13

to homotopyt...@googlegroups.com

MLTT (every propositional equality is judgemental).

The craziest judgemental equality I can imagine in HoTT is declaring

that all elements of the hpropositional truncation || X || of a type X

are judgementally equal. How crazy is that? (We had a little

discussion about that in the Agda mailing list some months ago.)

It is not clear to me what the boundary between "questionable" and

"desirable" is. Do you have a criterion?

It is worth remarking that, without univalence, adding certain

judgemental equalities, for example those of the HoTT book for the

type || 2 ||, give function extensionality, and so they are "very

powerful" (going beyond mere convenience in a proof assistant).

Which judgemental equalities can one add (1) without contradicting

univalence, (2) without contradicting the potential computational

content of univalence, and (3) without destroying decidability of

type-checking?

Martin

Oct 8, 2013, 6:38:12 PM10/8/13

to homotopyt...@googlegroups.com

M.

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu