Formal HoTT contexts

[Ali Caglayan]

In A.2.2 of the HoTT book, the structural rules for contexts are presented. I am not sure these inference rules are written well however.

Take the rule Subst₁

Γ  a : A     Γ, x : A, Δ   b : B 

{\displaystyle \vdash }

―――――――――――――― Subst₁

  Γ, Δ[a / x]  b[a / x] ; B[a / x]

Given that contexts are a list, I don't see how we can "pattern match" against non-constructors such as context concatenation Γ, Δ. I don't know any functional languages which allow you to pattern match in the middle of a list.

Now there are two solutions to this problem:

 1. Rewrite all rules with this kind of term to avoid them magically. (I have not been able to work this out).

 2. Contexts are not really lists

I am inclined to believe 2. is more correct however this doesn't actually help define what they are.

Could somebody clear this up for me?

[Ali Caglayan]

Sorry the inference rule has been messed up. Here is the corrected version:

 Γ ⊢ a:A  Γ,x:A,Δ ⊢ b:B 

―――――――――――――――――――――――――― Subst₁

 Γ,Δ[a/x] ⊢ b[a/x]:B[a/x]

[Michael Shulman]

One doesn't have to "pattern match" against a list in order to say "x:A appears somewhere in the list".  Type theory is not written in a functional programming language, it is written in mathematics.  (That said, even in a functional programming language you can define a predicate "occurs" that checks whether an element appears in a list.)

--
You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Guillaume Brunerie]

Moreover here you already know Γ from the first premise, so it’s not like you have to split the second context into two arbitrary pieces. You just have to check that the context in the first premise is a prefix of the context in the second premise, and then pattern match the rest of the second context with "x:A, Δ", which doesn’t pose any problem (it’s maybe not a constructor either, but at least there is unicity of the decomposition, so there is no ambiguity).

[Matt Oliveri]

Last but not least, you don't actually have to implement that rule in a type checker. It's admissible; it's a metatheorem about derivability.

(But actually, the style of rules in A.2 is not what you'd usually implement directly anyway.)

[Ali Caglayan]

(But actually, the style of rules in A.2 is not what you'd usually implement directly anyway.)

Would you mind elobrating on this? 

[Matt Oliveri]

1) The context is propagated from the root (of the derivation) to the leaves without checking it as it's built up. Instead, it's checked at each leaf, which is highly redundant.
2) The rules for judgmental equality aren't algorithmic.
3) It's not clear from the rules when a checker should use the conversion rule.

These all have traditional solutions:

1) Change the leaf rules, and the rules for binders, to check types as they're added to the context, on the way towards the leaves.
2) The usual approach interleaves weak head normalization, then comparing the outermost term formers, then recursing to subexpressions.
3) Conversion is removed as a separate rule. Instead, judgmental equality is used explicitly in rules that need it (e.g. Pi elimination).

The details of this kind of solution are in a chapter of "Advanced Topics in Types and Programming Languages", edited by Benjamin Pierce. It's probably in other places too though, so I wouldn't buy the book just for that.

It's like Mike said: type theory is usually just written as mathematics. If you want to read a type checking algorithm, you need to look for that specially. You might try searching for papers on dependent type checking. Or reading about one of the type theory implementation projects going on around here, like cubicaltt, redtt, or Andromeda. Full blown, user-friendly dependent type checkers do much more than just fix issues 1-3 above.