## Type Theory Rules: Judgement Derivations ### Overview The image presents a collection of type theory inference rules, likely related to a formal system for programming languages or logic. Each rule defines how to derive a judgement (a statement about types and terms) from other judgements. The rules cover various constructs, including variables, functions, products, sums, recursive types, and control flow. ### Components/Axes The image consists of multiple inference rules. Each rule has the following structure: * **Premises:** Judgements above the horizontal line. These are the conditions that must be satisfied to apply the rule. * **Conclusion:** The judgement below the horizontal line. This is the judgement that can be derived if the premises are satisfied. * **Context (Γ):** A set of assumptions about the types of variables. * **Terms (M, N, V):** Expressions in the language. * **Types (A, B):** Classifications of terms. * **Judgements:** Statements of the form "Γ ⊢ M : A", meaning "in context Γ, term M has type A". * **Other Symbols:** Various symbols representing type constructors, term constructors, and operations (e.g., × for product types, + for sum types, μ for recursive types). ### Detailed Analysis or ### Content Details Here's a breakdown of each rule, transcribing the text and explaining its meaning: 1. **Variable Rule:** * `Γ, x: A, Γ' ⊢ x : A` * Meaning: If variable `x` has type `A` in the context, then `x` has type `A`. 2. **Unit Type Introduction:** * `Γ ⊢ • : B` * `Γ ⊢ • ⊏ • : B` * Meaning: The unit value `•` has type `B`. 3. **Union Type Introduction:** * `Γ ⊢ ∪ ⊏ ∪ : B` * Meaning: The union value `∪` has type `B`. 4. **Let Binding:** * `Γ ⊢ V ⊏ V' : A Γ, x: A ⊢ M ⊏ M' : B` * `Γ ⊢ let x = V; M ⊏ let x = V'; M': B` * Meaning: If `V` has type `A` and `M` has type `B` assuming `x` has type `A`, then `let x = V; M` has type `B`. 5. **Abort Rule:** * `Γ ⊢ V ⊏ V' : 0` * `Γ ⊢ abort V ⊏ abort V': B` * Meaning: If `V` has type `0` (empty type), then `abort V` has type `B`. 6. **Inl (Left Injection):** * `Γ ⊢ V ⊏ V' : A1` * `Γ ⊢ inl V ⊏ inl V': A1 + A2` * Meaning: If `V` has type `A1`, then `inl V` has type `A1 + A2` (sum type). 7. **Inr (Right Injection):** * `Γ ⊢ V ⊏ V' : A2` * `Γ ⊢ inr V ⊏ inr V': A1 + A2` * Meaning: If `V` has type `A2`, then `inr V` has type `A1 + A2` (sum type). 8. **Unit Value:** * `Γ ⊢ () ⊏ () : 1` * Meaning: The unit value `()` has type `1`. 9. **Case Analysis:** * `Γ ⊢ V ⊏ V' : A1 + A2 Γ, x1: A1 ⊢ M1 ⊏ M1' : B Γ, x2: A2 ⊢ M2 ⊏ M2' : B` * `Γ ⊢ case V {x1.M1 | x2.M2} ⊏ case V' {x1.M1' | x2.M2'}: B` * Meaning: If `V` has type `A1 + A2`, `M1` has type `B` assuming `x1` has type `A1`, and `M2` has type `B` assuming `x2` has type `A2`, then the case expression has type `B`. 10. **Pair Formation:** * `Γ ⊢ V1 ⊏ V1' : A1 Γ ⊢ V2 ⊏ V2' : A2` * `Γ ⊢ (V1, V2) ⊏ (V1', V2'): A1 × A2` * Meaning: If `V1` has type `A1` and `V2` has type `A2`, then the pair `(V1, V2)` has type `A1 × A2` (product type). 11. **Split (Pair Decomposition):** * `Γ ⊢ V ⊏ V' : A1 × A2 Γ, x: A1, y: A2 ⊢ M ⊏ M' : B` * `Γ ⊢ split V to (x, y).M ⊏ split V' to (x, y).M': B` * Meaning: If `V` has type `A1 × A2` and `M` has type `B` assuming `x` has type `A1` and `y` has type `A2`, then the split expression has type `B`. 12. **Roll (Recursive Type Introduction):** * `Γ ⊢ V ⊏ V' : A[μX.A/X]` * `Γ ⊢ rollμX.A V ⊏ rollμX.A V': μX.A` * Meaning: If `V` has type `A[μX.A/X]` (A with `μX.A` substituted for `X`), then `rollμX.A V` has type `μX.A` (recursive type). 13. **Unroll (Recursive Type Elimination):** * `Γ ⊢ V ⊏ V' : μX.A Γ, x: A[μX.A/X] ⊢ M ⊏ M' : B` * `Γ ⊢ unroll V to roll x.M ⊏ unroll V' to roll x.M': B` * Meaning: If `V` has type `μX.A` and `M` has type `B` assuming `x` has type `A[μX.A/X]`, then the unroll expression has type `B`. 14. **Thunk (Suspension):** * `Γ ⊢ M ⊏ M' : B` * `Γ ⊢ thunk M ⊏ thunk M': UB` * Meaning: If `M` has type `B`, then `thunk M` has type `UB` (suspended computation). 15. **Force (Evaluation of Suspension):** * `Γ ⊢ V ⊏ V' : UB` * `Γ ⊢ force V ⊏ force V': B` * Meaning: If `V` has type `UB`, then `force V` has type `B`. 16. **Return (Value):** * `Γ ⊢ M ⊏ M' : FA` * `Γ ⊢ ret V ⊏ ret V': A` * Meaning: If `M` has type `FA`, then `ret V` has type `A`. 17. **Bind (Monadic Binding):** * `Γ ⊢ M ⊏ M' : FA Γ, x: A ⊢ N ⊏ N' : B` * `Γ ⊢ bind x ← M; N ⊏ bind x ← M'; N': B` * Meaning: If `M` has type `FA` and `N` has type `B` assuming `x` has type `A`, then the bind expression has type `B`. 18. **Lambda Abstraction:** * `Γ, x: A ⊢ M ⊏ M' : B` * `Γ ⊢ λx: A.M ⊏ λx: A.M': A → B` * Meaning: If `M` has type `B` assuming `x` has type `A`, then `λx: A.M` has type `A → B` (function type). 19. **Application:** * `Γ ⊢ M ⊏ M' : A → B Γ ⊢ V ⊏ V' : A` * `Γ ⊢ MV ⊏ M'V': B` * Meaning: If `M` has type `A → B` and `V` has type `A`, then `MV` has type `B`. 20. **Record Update:** * `Γ ⊢ M1 ⊏ M1' : B1 Γ ⊢ M2 ⊏ M2' : B2` * `Γ ⊢ {π ← M1 | π' → M2} ⊏ {π ← M1' | π' → M2'}: B1 & B2` * Meaning: If `M1` has type `B1` and `M2` has type `B2`, then the record update expression has type `B1 & B2`. 21. **And Type Introduction (Left Projection):** * `Γ ⊢ M ⊏ M' : B1 & B2` * `Γ ⊢ πM ⊏ πM': B1` * Meaning: If `M` has type `B1 & B2` (product type), then `πM` (left projection) has type `B1`. 22. **And Type Introduction (Right Projection):** * `Γ ⊢ M ⊏ M' : B1 & B2` * `Γ ⊢ π'M ⊏ π'M': B2` * Meaning: If `M` has type `B1 & B2` (product type), then `π'M` (right projection) has type `B2`. 23. **Roll with Variable:** * `Γ ⊢ M ⊏ M' : B[vY.B/Y]` * `Γ ⊢ rollvY.B M ⊏ rollvY.B M': vY.B` * Meaning: If `M` has type `B[vY.B/Y]`, then `rollvY.B M` has type `vY.B`. 24. **Unroll with Variable:** * `Γ ⊢ M ⊏ M' : vY.B` * `Γ ⊢ unroll M ⊏ unroll M': B[vY.B/Y]` * Meaning: If `M` has type `vY.B`, then `unroll M` has type `B[vY.B/Y]`. ### Key Observations * The rules define a type system with features like sum types, product types, recursive types, and monadic effects. * The rules use a judgement form `Γ ⊢ M ⊏ M' : A`, which suggests a relation between two terms `M` and `M'` of type `A` in context `Γ`. This could represent a form of subtyping, refinement typing, or program equivalence. * The presence of `UB` and `FA` types, along with `thunk`, `force`, `ret`, and `bind` rules, indicates the presence of monadic effects, likely for handling side effects or control flow. * The rules for `roll` and `unroll` define recursive types, allowing for the definition of self-referential data structures. ### Interpretation The image presents a formal type system that likely underpins a programming language or logical framework. The rules define how to assign types to terms and how to derive new judgements from existing ones. The system includes features for handling data structures (products, sums, recursive types), control flow (monads), and potentially program equivalence or refinement. The specific meaning of the `⊏` relation would need further context to fully understand, but it likely plays a crucial role in the system's semantics. The rules are essential for ensuring type safety and reasoning about the behavior of programs within this system.