帰納型とは何か, Lean の型システムの概略について

[Seasawher]

Zulip での以下の投稿がわかりやすい

---

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Type.20and.20Type*/near/444063991

• A type is a set of objects that's been called a type.
• A term is an expression for an object, where from the expression you can compute what type the object is an element of (for example, from Nat.succ Nat.zero you can see that it must be in the Nat type).
  An inductive type is a type that comes with a complete description of all its elements via constructors and a recursion/induction principle.
• Every type is itself in a type called a universe. The universes are Sort 0, Sort 1, Sort 2 and so on (though apparently the set of universe levels need not be just the natural numbers — I've never needed to think about this) with Prop := Sort 0 and Type u := Sort (u + 1) for convenience. By convention, the type of the universe Sort u is Sort (u + 1). My understanding is that this is not a deep fact, but a convenience so that you don't need both x is-term-in Nat and Nat is-type-in Type, and instead we can just write x : Nat and Nat : Type for both concepts).
• The "underlying sets" for types need not be disjoint. That's not something you can logically talk about from within Lean, but you can use this to convince yourself that certain things are unprovable in Lean (for example, Nat = Int can neither be proved nor disproved since it's possible for them to be the same, but it's also possible for them not to be). This may seem to conflict with "every term has a unique type", but it's terms that have types, not the objects that the terms refer to.
• There are rules for how "big" certain constructions are. For example, if X : Type u and Y : Type v, then X -> Y : Type (max u v). It makes some sense since (1) Unit -> Type u is in bijective correspondence to Type u and indeed they are both in Type (u + 1) and (2) Type u -> Prop is Set (Type u) and it makes sense that both would be in Type (u + 1) (these are "large" sets). There's an exception, where if X : Sort u and p : Prop then X -> p is in Prop. This is called impredicativity and it's important to make it so that universal quantification is a proposition while still being, conveniently, a function type.