## Type Theory Rules
### Overview
The image presents a collection of type theory rules, defining the syntax and semantics of a formal system. It includes definitions for types, values, expressions, and typing judgments, along with inference rules for various language constructs.
### Components/Axes
* **Top-Left**: Definitions for types `A`, values `V`.
* **Top-Right**: Definitions for types `B`, expressions `M, S`.
* **Middle-Left**: Definitions for contexts `Γ`, `Φ`.
* **Middle-Right**: Definitions for contexts `Δ`, `Ψ`.
* **Bottom**: Inference rules for type checking.
### Detailed Analysis or ### Content Details
**Definitions:**
* **Types (A)**:
* `A ::= ? | UB | 0 | A1 + A2 | 1 | A1 X A2`
* `?`: Unknown type.
* `UB`: Unit type.
* `0`: Empty type.
* `A1 + A2`: Sum type.
* `1`: Unit type.
* `A1 X A2`: Product type.
* **Values (V)**:
* `V ::= <A' <- A> V | x | abort V | inl V | inr V | case V{x1.V1 | x2.V2} | () | split V to ().V' | (V1, V2) | split V to (x, y).V' | thunk M`
* `<A' <- A> V`: Type cast.
* `x`: Variable.
* `abort V`: Abort.
* `inl V`: Left injection.
* `inr V`: Right injection.
* `case V{x1.V1 | x2.V2}`: Case expression.
* `()`: Unit value.
* `split V to ().V'`: Split operation.
* `(V1, V2)`: Pair.
* `split V to (x, y).V'`: Split operation.
* `thunk M`: Thunk.
* **Types (B)**:
* `B ::= ¿ | FA | T | B1 & B2 | A -> B`
* `¿`: Unknown type.
* `FA`: Type constructor.
* `T`: Type variable.
* `B1 & B2`: Product type.
* `A -> B`: Function type.
* **Expressions (M, S)**:
* `M, S ::= <B <- B'> M | • | UB | abort V | case V{x1.M1 | x2.M2} | split V to ().M | split V to (x, y).M | force V | ret V | bind x <- M; N | λx: A.M | MV | {} | {π -> M1 | π' -> M2} | πM | π'M`
* `<B <- B'> M`: Type cast.
* `•`: Hole.
* `UB`: Unit expression.
* `abort V`: Abort.
* `case V{x1.M1 | x2.M2}`: Case expression.
* `split V to ().M`: Split operation.
* `split V to (x, y).M`: Split operation.
* `force V`: Force.
* `ret V`: Return.
* `bind x <- M; N`: Bind.
* `λx: A.M`: Lambda abstraction.
* `MV`: Application.
* `{}`: Empty record.
* `{π -> M1 | π' -> M2}`: Record.
* `πM`: Projection.
* `π'M`: Projection.
* **Contexts (Γ)**:
* `Γ ::= · | Γ, x: A`
* `.`: Empty context.
* `Γ, x: A`: Context extension.
* **Contexts (Φ)**:
* `Φ ::= · | Φ, x <- x': A ⊆ A'`
* `.`: Empty context.
* `Φ, x <- x': A ⊆ A'`: Context extension with subtyping.
* **Contexts (Δ)**:
* `Δ ::= · | • ⊆ B`
* `.`: Empty context.
* `• ⊆ B`: Context extension with subtyping.
* **Contexts (Ψ)**:
* `Ψ ::= · | • ⊆ B ⊆ B'`
* `.`: Empty context.
* `• ⊆ B ⊆ B'`: Context extension with subtyping.
* **Other Definitions**:
* `T ::= A | B`
* `E ::= V | M`
**Typing Rules:**
* **Upcast**:
* Premises: `Γ |- V: A`, `A ⊆ A'`
* Conclusion: `Γ |- <A' <- A> V: A'`
* **Downcast**:
* Premises: `Γ |- Δ |- M: B'`, `B ⊆ B'`
* Conclusion: `Γ |- Δ |- <B <- B'> M: B`
* **Var**:
* Conclusion: `Γ, x: A, Γ' |- x: A`
* **Hole**:
* Conclusion: `Γ |- •: B`
* **Err**:
* Conclusion: `Γ |- UB: B`
* **0E**:
* Premise: `Γ |- V: 0`
* Conclusion: `Γ |- Δ |- abort V: T`
* **+IL**:
* Premise: `Γ |- V: A1`
* Conclusion: `Γ |- inl V: A1 + A2`
* **+IR**:
* Premise: `Γ |- V: A2`
* Conclusion: `Γ |- inr V: A1 + A2`
* **+E**:
* Premises: `Γ |- V: A1 + A2`, `Γ, x1: A1 |- Δ |- E1: T`, `Γ, x2: A2 |- Δ |- E2: T`
* Conclusion: `Γ |- Δ |- case V{x1.E1 | x2.E2}: T`
* **1I**:
* Conclusion: `Γ |- (): 1`
* **1E**:
* Premise: `Γ |- V: 1`
* Conclusion: `Γ |- Δ |- split V to ().E: T`
* **xI**:
* Premises: `Γ |- V1: A1`, `Γ |- V2: A2`
* Conclusion: `Γ |- (V1, V2): A1 X A2`
* **xE**:
* Premises: `Γ |- V: A1 X A2`, `Γ, x: A1, y: A2 |- Δ |- E: T`
* Conclusion: `Γ |- Δ |- split V to (x, y).E: T`
* **UI**:
* Premise: `Γ |- M: B`
* Conclusion: `Γ |- thunk M: UB`
* **UE**:
* Premise: `Γ |- V: UB`
* Conclusion: `Γ |- force V: B`
* **FI**:
* Premise: `Γ |- V: A`
* Conclusion: `Γ |- ret V: FA`
* **FE**:
* Premises: `Γ |- Δ |- M: FA`, `Γ, x: A |- Δ |- N: B`
* Conclusion: `Γ |- Δ |- bind x <- M; N: B`
* **->I**:
* Premise: `Γ, x: A |- Δ |- M: B`
* Conclusion: `Γ |- Δ |- λx: A.M: A -> B`
* **->E**:
* Premises: `Γ |- Δ |- M: A -> B`, `Γ |- V: A`
* Conclusion: `Γ |- Δ |- MV: B`
* **TI**:
* Conclusion: `Γ |- {}: T`
* **&I**:
* Premises: `Γ |- Δ |- M1: B1`, `Γ |- Δ |- M2: B2`
* Conclusion: `Γ |- Δ |- {π -> M1 | π' -> M2}: B1 & B2`
* **&E**:
* Premise: `Γ |- Δ |- M: B1 & B2`
* Conclusion: `Γ |- Δ |- πM: B1`
* **&E'**:
* Premise: `Γ |- Δ |- M: B1 & B2`
* Conclusion: `Γ |- Δ |- π'M: B2`
### Key Observations
* The system includes basic types like unit, empty, sum, and product.
* It supports type casting, function abstraction and application, and record manipulation.
* The typing rules define how to derive the type of an expression based on the types of its sub-expressions and the context.
### Interpretation
The image presents a formal type system, likely for a functional programming language. The definitions and typing rules provide a rigorous framework for ensuring type safety and preventing runtime errors. The system includes features like subtyping, type casting, and record types, which enhance its expressiveness and flexibility. The rules are designed to be compositional, allowing the type of a complex expression to be derived from the types of its constituent parts.
