Stream: general

Topic: lean's type theory

Mario Carneiro (Mar 17 2018 at 03:39):

Okay, I'm a bit embarrassed to release this in this very early form, but there's enough meat in it that it can be useful to others even before it's done. This will probably become a major part of my master's thesis. What you will find:

• A definition of the axioms of lean
• The basic DTT stuff
• let binders and definitions
• inductive types (in full gory detail)
• the computation rules (beta, eta, zeta, delta, iota)
• Quotient types
• propext and choice
• Algorithmic equality (aka lean's defeq)
• proof that algorithmic equality is not transitive and defeq is not decidable
• Unique typing
• A long and complicated proof, involving a hierarchy of church-rosser theorems. I'm really glad it worked out, but the complexity shows, and I need to trim it down and make it more accessible
• Soundness (unfinished)
• It is exactly as simple as it sounds like, but the language is huge and there are a lot of cases.

Kevin Buzzard (Mar 17 2018 at 09:17):

Oh many thanks for this -- as you saw, I made some sort of effort to engage with this kind of material without reading the source code (i.e. restricting to the docs) and it was tough. I am relieved to see that iota reduction applies to things defined by recursion rather than just cases!

Kevin Buzzard (Mar 17 2018 at 09:40):

I spent some time yesterday trying to get to the bottom of this accrec example and it would have been a darn sight easier if I'd had access to this paper then.

Gabriel Ebner (Mar 17 2018 at 10:26):

I think it's great that we finally have a written description of the type theory implemented in Lean. Ideally it should also be included in the reference manual, and/or published somewhere.

Gabriel Ebner (Mar 17 2018 at 10:30):

section 2.3: I don't think it is a good idea to require full whnf in the algorithmic equivalence since we don't do it any of the implementations. We do lazy delta-reduction, that is, do full beta/iota/quotient/zeta and only unfold the constant with the larger definitional height, once. I think you should just replace ↓ by ⇝* here.

Gabriel Ebner (Mar 17 2018 at 10:33):

section 2.4: "Lean takes a simpler approach and simply zeta expands these binders when necessary for checking.": I don't think you've defined "Lean" anywhere. Not all of the implementations follow this approach. The C++ type_checker, the Haskell tc, and trepplein all eagerly unfold lets. However, the type_context doesn't. I believe the term ζ-reduction typically refers to x ⇝ e'.

Mario Carneiro (Mar 17 2018 at 10:40):

There are a few white lies in algorithmic equivalence, and I'd be happy to give a more honest account but I'm not quite sure how. (One thing I have noticed is that sometimes pure congruence proofs don't check, because one side is eagerly iota reduced to something that is not recognizably equivalent anymore.)

Gabriel Ebner (Mar 17 2018 at 10:40):

section 2.6.2: "Here we have K-like elimination": do you mean large elimination? K-like reduction for acc would not be strongly normalizing, right?

Mario Carneiro (Mar 17 2018 at 10:41):

I don't use the term "subsingleton elimination" anywhere in the paper, I may have mixed up my terms. I use K-like elimination to refer to large eliminating props

Mario Carneiro (Mar 17 2018 at 10:43):

When I talk about "lean does X", I am usually referring to lean.exe's kernel. I didn't want to get into checking expressions with lets in the context, like type_context does, which is why I omitted that approach.

Gabriel Ebner (Mar 17 2018 at 10:43):

but there is a second reduction rule used for K-like eliminators. It can be thought of as a combination of proof irrelevance to change the major
premise into a constructor followed by the iota rule.

Yes, you might want to clean up the definitions (and actually define them). ^^

which part?

Mario Carneiro (Mar 17 2018 at 10:44):

Also: I just finished the proof of soundness. Celebrate! Lean can't prove false

Gabriel Ebner (Mar 17 2018 at 10:44):

K-like elimination refers to K-like reduction here, and subsingleton elimination on the page before, afaict.

Gabriel Ebner (Mar 17 2018 at 10:44):

That's not using algorithmic defeq, right?

Mario Carneiro (Mar 17 2018 at 10:45):

Soundness for both algorithmic and ideal typechecking

Mario Carneiro (Mar 17 2018 at 10:46):

I proved it for the ideal version, and the algorithmic check implies ideal check

Gabriel Ebner (Mar 17 2018 at 10:48):

algorithmic check implies ideal check

That's not proven yet, right?

Mario Carneiro (Mar 17 2018 at 10:48):

It's pretty trivial

Mario Carneiro (Mar 17 2018 at 10:48):

the algorithmic rules are a subset of the ideal ones

Mario Carneiro (Mar 17 2018 at 10:49):

the ideal check is basically what lean would do if it was nondeterministic and tried all the tricks at once

Gabriel Ebner (Mar 17 2018 at 10:50):

Except that the ideal ones have extra side conditions that require the well-typedness of all terms that occur. The implication requires at the very least subject reduction for ⇝, which is not completely obvious to me.

Gabriel Ebner (Mar 17 2018 at 10:52):

Ok, I see subjection reduction is Lemma 3.10.

Mario Carneiro (Mar 17 2018 at 10:53):

Note that ->_kappa is a bit different from ->, it has slightly different rules for iota stuff

Mario Carneiro (Mar 17 2018 at 10:53):

I never explicitly stated subject reduction for -> (using the ideal check), but maybe I should be more precise about it

Gabriel Ebner (Mar 17 2018 at 10:59):

I think the general approach for the algorithmic defeq is good. It's better to have an over-approximation than to precisely model the actual (current implementation of the) type-checker. If you can show this defeq proof system to be sound, then all "reasonable" type-checkers should be correct.

Gabriel Ebner (Mar 17 2018 at 11:00):

section 2.3: you're also missing η-expansion, see https://github.com/leanprover/lean/blob/07bb7d809b6be49f38ce4e427c54a82708ae281f/src/kernel/type_checker.cpp#L517-L529

Mario Carneiro (Mar 17 2018 at 11:12):

Would it suffice to replace the eta rule with extensionality "e x <-> e' x => e <-> e'"?

Mario Carneiro (Mar 17 2018 at 11:13):

or is this only used when solving lam x:a. e <-> e'

Gabriel Ebner (Mar 17 2018 at 11:13):

Yes, you can then recover η via the conversion rule.

Gabriel Ebner (Mar 17 2018 at 11:13):

Yes, in practice it is only used when one side is a lambda.

Mario Carneiro (Mar 17 2018 at 11:14):

I know some typecheckers prefer extensionality over eta, since it's pretty easy to figure out when to use it

Mario Carneiro (Mar 17 2018 at 11:29):

but there is a second reduction rule used for K-like eliminators. It can be thought of as a combination of proof irrelevance to change the major
premise into a constructor followed by the iota rule.

Yes, you might want to clean up the definitions (and actually define them). ^^

I don't follow. That passage looks alright, is something missing?

Gabriel Ebner (Mar 17 2018 at 11:33):

K-like elimination refers to multiple concepts in the paper: 1) subsingleton elimination, and 2) K-like reduction. For example, and has 1) but not 2).

Mario Carneiro (Mar 17 2018 at 11:34):

I use it essentially only for (1), (2) is more of a remark that comes up once as a sort of historical note "why K?"

Gabriel Ebner (Mar 17 2018 at 11:35):

You use it for 2) in section 2.6.4. Although it is not clear how you obtain the b there.

Mario Carneiro (Mar 17 2018 at 11:36):

I need a name for inductive types that eliminate to Type but live in Prop. "Large elimination" seems to also suggest when the type itself is large, so it's not a great name. Will subsingleton elimination cover exactly this usage?

Mario Carneiro (Mar 17 2018 at 11:36):

the b is obtained from the LHS as described in the paragraph after

Mario Carneiro (Mar 17 2018 at 11:36):

and it only applies if you can obtain all of b that way

Gabriel Ebner (Mar 17 2018 at 11:36):

I've only seen "subsingleton elimination" in this usage.

Mario Carneiro (Mar 17 2018 at 11:37):

cool, I'll stop saying K-like then

Gabriel Ebner (Mar 17 2018 at 11:37):

Ah, next page, ok.

Mario Carneiro (Mar 17 2018 at 12:38):

Huh, I've been telling myself that defeq is only undecidable in inconsistent contexts, but this is not true, almost trivially: if x : 0 |- A = B is some undecidable defeq problem, then |- \lam x : 0. A = \lam x : 0. B is also an undecidable defeq problem

Patrick Massot (Mar 17 2018 at 14:28):

I swear one day I'll have time to actually read this paper (or maybe a version with a bit higher word/symbol ratio). In the mean time I'm surprised by the source code. It' funny to see Lean consistently use unicode to be more readable than Coq but you still write \Gamma\vdash \alpha:\U_\ell\quad \Gamma\vdash e:\beta in your LaTeX source like it's still 1990.

Gabriel Ebner (Mar 17 2018 at 14:40):

section 3.4: why do you consider η-reduction? I don't think any Lean typechecker has that.

Patrick Massot (Mar 17 2018 at 14:41):

 has spacing issues (beyond being harder to parsers)

Mario Carneiro (Mar 17 2018 at 14:43):

How else are you going to get eta reduction unless you put it in? Also: the constraints on the kappa reduction relation are very tight. I went through no less than 10 variations on it before I was able to get the church rosser theorem to go through

Simon Hudon (Mar 17 2018 at 14:44):

That's the reason why you see more and more papers on arxiv where only the pdf is available and not the TeX source

Do you mean that it is not used as a preprocessor and therefore people only submit pdfs?

Gabriel Ebner (Mar 17 2018 at 14:44):

Not at all? None of the typecheckers uses it, AFAIK. Trepplein definitely doesn't. We only do η for defeq.

Gabriel Ebner (Mar 17 2018 at 14:44):

I just got the feeling that η is a serious complication here, and the main reason you need a new and different reduction relation and defeq relation.

Mario Carneiro (Mar 17 2018 at 14:45):

the whole point of the kappa reduction is so that the statement of Theorem 3.15 holds

Mario Carneiro (Mar 17 2018 at 14:47):

The alternative would be to try to put eta or extensionality in the =p relation

Gabriel Ebner (Mar 17 2018 at 14:47):

I thought it is included in the ... in the definition of =p.

Mario Carneiro (Mar 17 2018 at 14:47):

the ... only includes compatibility rules

Gabriel Ebner (Mar 17 2018 at 14:48):

I don't think it says that anywhere. (at least not above and below the definition)

Mario Carneiro (Mar 17 2018 at 14:49):

It's a very spartan relation, it's just replacing proofs and nothing else (except for that lambda thing)

Mario Carneiro (Mar 17 2018 at 14:54):

I will investigate whether it suffices to have one-sided extensionality e =p e' x => lam x:a. e =p e' and remove eta from the kappa reduction. If so that would allow me to remove the context from ->k, which would be nice

Mario Carneiro (Mar 17 2018 at 15:04):

I think the biggest departure from the usual reduction relation is the K reduction (which I have renamed K+), because it is super aggressive unfolding of a proof, which guarantees nontermination when it sees an acc.rec

Kevin Buzzard (Mar 17 2018 at 15:29):

so is this paper about what Lean does, or what it should do in your opinion :-)

Kevin Buzzard (Mar 17 2018 at 15:30):

And do the devs have any comments about whether Lean 4 will do the same thing when it comes to definitional equality?

Gabriel Ebner (Mar 17 2018 at 15:30):

Not sure if I count as a dev anymore, but I seriously doubt there will be any foundational changes in Lean 4.

Kevin Buzzard (Mar 17 2018 at 15:31):

That's good to know -- I guess there were foundational changes from Lean 2 to Lean 3 so I suppose it wasn't something one could definitely assume...

Gabriel Ebner (Mar 17 2018 at 15:34):

There were exactly two foundational changes from Lean 2 to Lean 3: 1) let-expressions in the kernel (completely harmless), 2) mutually inductive types are no longer supported by the kernel (these are now simulated). Also the axioms for choice and quotients got some mostly cosmetic changes.

Kevin Buzzard (Mar 17 2018 at 15:35):

Oh I thought there was some change to the underlying type theory -- HoTT in Lean 2?

Gabriel Ebner (Mar 17 2018 at 15:38):

Oh yes, HoTT got removed from the kernel (you had to pass an extra command-line flag to use it, and there was a separate library). Completely forgot about that. But we now have a reasonably way to do it without kernel changes: https://github.com/gebner/hott3

Mario Carneiro (Mar 17 2018 at 15:53):

so is this paper about what Lean does, or what it should do in your opinion :-)

The motivation is of course what lean does, but this is badly behaved in a number of ways which make it completely unsuitable for theoretical treatment, so I replace it with a better version, show soundness of the original version with respect to that, and then forget about the original thing

Mario Carneiro (Mar 17 2018 at 15:56):

As Gabriel mentions, there are multiple "leans", and they don't all agree on the foundational stuff. This is in part what I wanted to address with this paper, to get down a single system that we can talk about as the ideal lean, and look at how close we can get to that. One thing which should be true, however, is that all existing lean kernels are underestimates of the typing judgment in this paper. That means that anything you can't prove with the ideal judgment can't be verified in these kernels either, which is the soundness result I want

Gabriel Ebner (Mar 17 2018 at 16:00):

AFAICT all existing kernels even fit within the algorithmic definitional equality check.

Gabriel Ebner (Mar 17 2018 at 16:02):

NB: I think the algorithmic definitional equality is not just an ugly approximation of the ideal one, but also important as a practical optimization: using the algorithmic definitional equality, we can elide almost all type-inference calls during type-checking.

Gabriel Ebner (Mar 17 2018 at 16:05):

Compare also the various variants of the typing rules proved equivalent in [1].
[1] A.Bauer, P. Haselwarter, T. Wintertaler, A modular formalization of type theory in Coq, TYPES (2017). http://math.andrej.com/2017/05/29/a-modular-formalization-of-type-theory-in-coq/

Mario Carneiro (Mar 17 2018 at 16:15):

I'm also having difficulty with stating strong normalization because of my struggles here, I think. What is the reduction relation of interest here? Is it just head reduction? I think it is supposed to include reduction under binders, but then once we decide "arbitrarily" not to reduce some things that should be reducible, in what sense are we talking about the "right" relation? I.e. what does strong normalization have to do with consistency?

Gabriel Ebner (Mar 17 2018 at 16:27):

Weak head reduction is enough for consistency. But strong normalization for the full reduction relation is definitely interesting as well.

Gabriel Ebner (Mar 17 2018 at 16:30):

Since we've talked about η today, I think I've found a novel way to break transitivity with just K-like reduction for eq:

def foo : 0 = 0 → ℕ :=
@eq.rec ℕ 0 (λ _, ℕ) 42 0
def bar : 0 = 0 → ℕ :=
@eq.rec ℕ 0 (λ n, if n = 0 then ℕ else empty) (42 : ℕ) 0

example : foo = (λ _, 42) := rfl
example : bar = (λ _, 42) := rfl
example : foo = bar := rfl -- fails


Mario Carneiro (Mar 17 2018 at 16:42):

I found an interesting potential computational rule for quot.sound:

variables (α : Sort*) (r : α → α → Prop) (a : α)
(f : α → Sort*) (H : ∀ (a b : α), r a b → f a = f b)
(e : f a) (b : α) (h : r a b)

example : @eq.rec (quot r) (quot.mk r a) (quot.lift f H) e
(quot.mk r b) (quot.sound h) = cast (H a b h) e :=
by change H a b h with (congr_arg (quot.lift f H) (quot.sound h):_);
induction quot.sound h; refl


Mario Carneiro (Mar 17 2018 at 16:45):

@Gabriel Ebner That was a big pain during the proof of church rosser. It's actually not a theoretical problem, but rather a side effect of K reductions without accounting for eta reduction

Mario Carneiro (Mar 17 2018 at 16:45):

I fixed it by making sure that all recursors have the right number of arguments at all times

Mario Carneiro (Mar 17 2018 at 16:46):

Alternatively, any K-like inductive should be eta expanded before normalization

Mario Carneiro (Mar 17 2018 at 16:58):

The problem is that unapplied K recursors are stuck terms when they shouldn't be

variables (α : Sort*) (a : α) (C : α → Sort*) (e : C a)
#reduce λ h, @eq.rec α a C e a h -- λ (h : a = a), e   <- good
#reduce @eq.rec α a C e a -- eq.rec e                  <- bad


Mario Carneiro (Mar 17 2018 at 17:03):

I originally had the recursors evaluating to lambdas like this, but it was a notational nightmare since the number of unapplications depends on how many variables there are (the only one you have "control" over is the major premise, once that one is allowed to be a variable you have to deal with the parameters and such, and any of those could be variables or things equivalent to variables...), so I opted instead for an up-front eta expansion, since during reduction a recursor never loses its major premise

Last updated: May 10 2021 at 00:31 UTC