## 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.

\n ## Formal System Definitions: Type Theory Rules ### Overview The image presents a collection of formal definitions and inference rules, likely related to a type theory system. It appears to be a visual representation of the syntax and semantics of a programming language or a logical framework. The image is densely packed with symbols and notations, suggesting a high level of technical detail. The layout is organized into sections defining various components (A, B, V, M, S, T, Δ, Ψ) and rules (UpCast, DnCast, VAR, HOLE, ERR, OE, +IL, +IR, 1E, XI, UI, UE, FI, FE, +E, +EE). ### Components/Axes The image does not contain traditional axes or charts. Instead, it consists of symbolic definitions and rules. The key components are: * **A, B:** Represent types. * **V:** Represents values. * **M:** Represents environments (mappings from names to values). * **S:** Represents substitution. * **T:** Represents contexts. * **Δ:** Represents type environments. * **Ψ:** Represents value environments. * **Γ:** Represents a context (a set of assumptions). * **Rules:** UpCast, DnCast, VAR, HOLE, ERR, OE, +IL, +IR, 1E, XI, UI, UE, FI, FE, +E, +EE. Each rule has a specific format: `Γ ⊢ expression : type`. ### Detailed Analysis or Content Details Here's a transcription of the definitions and rules, grouped by component: **Definitions:** * **A ::= ? | UB | O | A₁ + A₂ | A₁ × A₂ | A₂** * **B ::= | A | T | B & B | B₂ | A → B** * **V ::= (A ∧ V) | x | abort V** * **M, S ::= split V to (M | split V to (x,y,M)** * **T ::= .Γ, x:A** * **Φ ::= | Φ x ∈ C A'** * **Δ ::= :: B** * **Ψ ::= :: B ⊆ B'** **Rules:** * **UpCast:** `Γ ⊢ V : A A ⊆ A' => Γ ⊢ V : A'` * **DnCast:** `Γ ⊢ A ⊆ M' B ⊆ B' => Γ ⊢ B : M'` * **VAR:** `Γ ⊢ x : A, x:A' Γ ⊢ x : A` * **HOLE:** `Γ ⊢ :: B => Γ ⊢ : B` * **ERR:** `Γ ⊢ : UB => B` * **OE:** `Γ ⊢ V : O => Γ ⊢ Δ + abort V : T` * **+IL:** `Γ ⊢ V : A₁ Γ ⊢ V : A₂ => Γ ⊢ V : A₁ + A₂` * **+IR:** `Γ ⊢ V : A₁ + A₂ => Γ ⊢ case V(x₁,x₂) : A₁ → E₁ T A₂ → E₂ T` * **1E:** `Γ ⊢ V : 1 => Γ ⊢ V : E : T` * **XI:** `Γ ⊢ V₁ : V₂ A₁ × A₂ => Γ ⊢ Δ + split V to (x,y) : E : T` * **UI:** `Γ ⊢ V : UB => Γ ⊢ M : M : B` * **UE:** `Γ ⊢ V : UB Γ ⊢ force V : B => Γ ⊢ ret V : FA` * **FI:** `Γ ⊢ M : M : FA => Γ ⊢ Δ + bind x = M : N : B` * **FE:** `Γ ⊢ Δ + M : A → B => Γ ⊢ Δ + M V : B` * **+E:** `Γ ⊢ Δ + M V : B => Γ ⊢ Δ + M : B : B` * **+EE:** `Γ ⊢ Δ + M₁ : B₁ Γ ⊢ Δ + M₂ : B₂ => Γ ⊢ Δ + M : B₁ & B₂` **Additional Notation:** * `A ∧ V` * `x abort V` * `split V to (x,y,M)` * `case V(x₁,x₂) : A₁ → E₁ T A₂ → E₂ T` * `force V` * `ret V` * `bind x = M` ### Key Observations The rules are presented in a standard logical notation, with the turnstile symbol (`⊢`) indicating a derivation or judgment. The rules define how to manipulate types, values, and environments within the system. The presence of rules like `UpCast` and `DnCast` suggests a type system with subtyping. The rules involving `split` and `bind` indicate mechanisms for handling data structures and variable bindings. The notation is very compact and relies heavily on symbolic representation. ### Interpretation This image represents a formal specification of a type system, likely for a functional programming language. The rules define the valid operations and derivations within the system, ensuring type safety and correctness. The system appears to support subtyping, product types (A × A₂), sum types (A₁ + A₂), and potentially dependent types (indicated by the use of contexts and environments). The rules are designed to ensure that type checking and evaluation are sound and consistent. The presence of `abort V` suggests a mechanism for handling errors or exceptional conditions. The overall structure suggests a sophisticated type system capable of expressing complex data structures and computations. The notation is highly abstract and requires a strong background in type theory and formal methods to fully understand. The image is a concise and precise representation of a complex system, intended for experts in the field.

\n ## Formal Grammar and Inference Rules: A Type System Specification ### Overview The image presents a formal specification of a type system or calculus, likely for a functional programming language with effects, subtyping, and computational features. It is structured into two main columns defining syntactic categories and a lower section presenting inference rules (typing judgments). The content is purely mathematical/logical notation with no natural language prose beyond rule labels. ### Components/Axes (Syntactic Categories) The image is divided into two primary vertical sections defining the language's syntax. **Left Column (Values and Simple Types):** * **A (Types):** Defined as `? | UB | 0 | A₁ + A₂ | 1 | A₁ × A₂`. This includes a unknown type (`?`), a type `UB`, the empty type `0`, sum types (`+`), the unit type `1`, and product types (`×`). * **V (Values):** Includes variables `x`, abort, injections (`inl V`, `inr V`), case analysis, unit `()`, splits for unit and pairs, and `thunk M`. * **Γ (Value Context):** A mapping from variables `x` to types `A`. * **Φ (Subtyping Context):** A mapping from type variables `x` to subtyping relations `A ⊑ A'`. **Right Column (Computations and Effectful Types):** * **B (Effectful/Computation Types):** Defined as `¿ | FA | τ | B₁ & B₂ | A → B`. This includes a dual unknown type `¿`, a type `FA`, a type `τ`, an intersection/with type `&`, and a function type `→`. * **M, S (Computations/Structures):** Includes abort, case analysis, splits for computations and pairs, force, return, lambda abstraction, application, empty set `{}`, maps `π ↦ M`, and projections `πM`, `π'M`. * **Δ (Computation Context):** A mapping from a special marker `•` to computation types `B`. * **Ψ (Subtyping Context for Computation Types):** A mapping from a marker `•` to subtyping relations `B ⊑ B'`. **Central Definitions:** * **T (All Types):** `A | B` (The union of value types and computation types). * **E (All Expressions):** `V | M` (The union of values and computations). ### Detailed Analysis (Inference Rules) The lower portion of the image lists inference rules in a standard natural deduction style. Each rule has a label (e.g., `VAR`, `→I`), premises above a horizontal line, and a conclusion below it. **Key Judgments:** 1. `Γ ⊢ V : A` (Value `V` has type `A` in context `Γ`). 2. `Γ | Δ ⊢ M : B` (Computation `M` has type `B` in contexts `Γ` and `Δ`). 3. A highlighted box contains the combined judgment: `Γ ⊢ V : A and Γ | Δ ⊢ M : B`. **Subtyping Rules:** * **UpCAST:** From `Γ ⊢ V : A` and `A ⊑ A'`, infer `Γ ⊢ ⟨A' ↩ A⟩V : A'`. * **DnCAST:** From `Γ | Δ ⊢ M : B'` and `B ⊑ B'`, infer `Γ | Δ ⊢ ⟨B ↩ B'⟩M : B`. **Typing Rules (Grouped by connective/construct):** * **VAR, HOLE, ERR:** Rules for variables, the hole `•`, and the error term `U_B`. * **0E, +IL, +IR, +E:** Rules for the empty type (`abort`), left/right injections of sum types, and case analysis on sums. * **1I, 1E, ×I, ×E:** Rules for the unit type (introduction `()` and elimination `split`), and product types (introduction `(V₁, V₂)` and elimination `split`). * **UI, UE, FI, FE:** Rules for `UB` (introduction `thunk`, elimination `force`), and `FA` (introduction `ret`, elimination `bind`). * **→I, →E:** Rules for function introduction (lambda abstraction `λx:A.M`) and elimination (application `MV`). * **τI, &I, &E, &E':** Rules for the type `τ` (introduction `{}`), intersection type introduction (creating a map `π ↦ M₁, π' ↦ M₂`), and two elimination forms (projections `πM` and `π'M`). ### Key Observations 1. **Dual Structure:** There is a clear duality between the left column (value-oriented, `A`, `V`, `Γ`) and the right column (computation-oriented, `B`, `M`, `Δ`). This suggests a distinction between pure values and effectful computations. 2. **Subtyping Contexts:** The separate contexts `Φ` and `Ψ` for subtyping of `A` and `B` types indicate a system with explicit subtyping tracking. 3. **Special Markers:** The use of `•` in contexts `Δ` and `Ψ` is notable, possibly representing a special location or effect label. 4. **Highlighted Judgment:** The box around `Γ ⊢ V : A and Γ | Δ ⊢ M : B` emphasizes that the system's core concern is the simultaneous well-formedness of a value and a computation. 5. **Rule Density:** The rules for sums (`+E`) and intersections (`&I`, `&E`, `&E'`) are particularly detailed, suggesting these are complex or central features of the calculus. ### Interpretation This image specifies the formal syntax and typing rules for a sophisticated type system. The system appears designed to model a language that: * **Separates Values and Computations:** This is a common pattern in languages with effects (like monads) or in logical frameworks (propositions-as-types). * **Features Subtyping:** The explicit subtyping rules (`UpCAST`, `DnCAST`) and contexts (`Φ`, `Ψ`) indicate a system where types can be related by a hierarchy, allowing for safe coercion of values and computations. * **Incorporates Effects:** The presence of `UB`/`FA` types with `thunk`/`force` and `ret`/`bind` operations strongly suggests a monadic or similar structure for handling computational effects in a controlled manner. * **Supports Intersection Types:** The `&` type and its rules allow a computation to have multiple, simultaneous types, which is useful for modeling overloaded functions or more precise specifications. * **Is Likely Research-Grade:** The notation and structure are characteristic of academic work in programming language theory, possibly from a paper on effect systems, modal types, or a core calculus for a advanced functional language. The system aims for precision in defining how values and computations are constructed, typed, and related through subtyping.

## Logical Type Theory System: Core Inference Rules and Type Definitions ### Overview The image presents a formal type theory system with definitions for types (`A`, `B`), variables (`V`), contexts (`Γ`), and inference rules. It includes type judgments (`⊢`), term constructors (`case`, `split`), and operational semantics (`think`, `force`, `bind`). The system emphasizes type safety through strict type checking and pattern matching. ### Components/Axes #### Type Definitions - **`A`**: A type defined as `? | U_B | 0 | A₁ + A₂ | 1 | A₁ × A₂` - **`B`**: A type defined as `? | F_A | ⊤ | B₁ & B₂ | A → B` - **`V`**: A variable type with case analysis: `case V {x₁.V₁ | x₂.V₂} | () | split V to ().V' | (V₁, V₂) split V to (x, y).V'` - **`Γ`**: Type context: `· | Γ, x : A` - **`Φ`**: Type context with subtyping: `· | Φ, x ⊆ x' : A ⊆ A'` #### Inference Rules 1. **Var** (Variable Introduction): `Γ ⊢ V : A` and `Γ ⊢ Δ ⊢ M : B` `Γ ⊢ V : A` 2. **Hole** (Type Hole): `Γ ⊢ ? : B` 3. **Err** (Error Type): `Γ ⊢ U_B : B` 4. **UpCast/DownCast**: - **UpCast**: `Γ ⊢ V : A` and `A ⊆ A'` `Γ ⊢ ⟨A' ⇸ A⟩V : A'` - **DownCast**: `Γ ⊢ Δ ⊢ M : B'` and `B ⊆ B'` `Γ ⊢ Δ ⊢ ⟨B ⇸ B'⟩M : B` 5. **Operational Semantics**: - **`think`**: `Γ ⊢ ? ⊢ M : U_B` - **`force`**: `Γ ⊢ V : U_B` - **`bind`**: `Γ ⊢ x : A` and `Γ ⊢ N : B` `Γ ⊢ bind x ← M; N : B` 6. **Type Constructors**: - **Sum Type (`+`)**: `Γ ⊢ V : A₁ + A₂` `Γ, x₁ : A₁ ⊢ E₁ : T` and `Γ, x₂ : A₂ ⊢ E₂ : T` `Γ ⊢ case V {x₁.E₁ | x₂.E₂} : T` - **Product Type (`×`)**: `Γ ⊢ V : A₁ × A₂` `Γ, x : A₁, y : A₂ ⊢ E : T` `Γ ⊢ split V to (x, y).E : T` #### Type Judgments - **`⊢`**: Type derivation (e.g., `Γ ⊢ V : A`) - **`⊨`**: Semantic entailment (e.g., `A ⊆ A'`) ### Detailed Analysis - **Type Hierarchy**: - `A` includes base types (`0`, `1`), sums (`A₁ + A₂`), and products (`A₁ × A₂`). - `B` includes base types (`⊤`), products (`B₁ & B₂`), and function types (`A → B`). - **Pattern Matching**: - `case V` deconstructs sum types, while `split V` deconstructs product types. - **Context Extensions**: - `Γ, x : A` adds a variable `x` of type `A` to the context `Γ`. - **Subtyping**: - `A ⊆ A'` allows upcasting (widening) and downcasting (narrowing) with checks. ### Key Observations 1. **Strict Type Safety**: - All operations (e.g., `case`, `split`) are type-checked to ensure no runtime errors. 2. **Recursive Definitions**: - `V` and `M` are recursively defined with case analysis and splitting. 3. **Operational Semantics**: - `think` and `force` handle undefined and error types, respectively. 4. **Subtyping Rules**: - Upcasting (`A ⊆ A'`) and downcasting (`B ⊆ B'`) enforce type compatibility. ### Interpretation This system formalizes a dependently typed lambda calculus with: - **Algebraic Data Types**: Sums (`+`) and products (`×`) for data structures. - **Pattern Matching**: Ensures exhaustive and correct deconstruction of types. - **Type Safety**: Inference rules prevent ill-typed programs from compiling. - **Operational Semantics**: Defines evaluation rules for terms (e.g., `bind` for monadic operations). The system resembles a core calculus for functional programming languages, emphasizing correctness through type theory. The absence of numerical data suggests it is a theoretical framework rather than empirical analysis.