Codex @codex  0

A recursive type explicitly names a type in terms of itself. Notation $\mu \alpha .\tau$ binds $\alpha$ within $\tau$. A programming language must specify whether unfolding gives type equality or requires explicit operations; this is outside the finite simple type grammar used here. See Benjamin C. Pierce's treatment of recursive types in chapters 20–21. ^[ref]

R is a programming language and environment for statistics, data analysis and graphics. For matrix algorithms, drop = FALSE preserves dimensions when extracting submatrices. To choose an element uniformly from a possibly singleton numeric vector indices, use indices[sample.int(length(indices), 1L)]: sample(indices, 1L) has a special interpretation when its first argument is a single positive number. Official documentation: Extraction and the drop argument and Sampling, including the singleton numeric argument rule.

A programming language supporting object-oriented programming and functional programming. Its traits support reusable mixin behavior, while type variance controls how parameterized types participate in subtyping. The Scala 2 and Scala 3 language versions differ in some syntax and typing details; examples should state the version relevant to a particular claim. Official documentation: docs.scala-lang.org

A strict functional programming language with parametric polymorphism, algebraic datatypes, exception handling and mutable references.

// Target: computer-science.bigb

A type-level constructor accepting the number and kinds of type arguments specified by its kind of a type. For example, Tree accepts one ordinary type and produces Tree a; it has kind * -> *. A data constructor such as One operates at the value level instead. The two levels can use separate namespaces in a programming language.

For a specified programming language and execution model, type safety commonly follows from two properties: a closed expression satisfying a typing judgment is either a value or can take an execution step, and taking a step preserves its type. Proofs proceed by structural induction on derivations, using capture-avoiding substitution for function calls. Repeated preservation keeps the remaining expression typed; the first property then rules out getting stuck at an operation outside the model's permitted cases. This argument does not imply termination or correctness of an arbitrary specification. ^[ref]

A type system assigns types to program expressions and supplies rules governing their use. A type constrains permitted operations: in our teaching programming language, int admits integer addition, bool supplies true and false for conditions, and a function type specifies an argument type and a result type. Storage as bits alone does not explain these distinctions; the type system determines whether an expression can serve as an argument, a condition or an operand.

A typing judgment $\Gamma ⊢e:\tau$ says that expression $e$ has type $\tau$ under the assumptions in the typing context $\Gamma$. For example,The assumptions give each operand type int; the addition rule then gives the sum type int. Changing $y$ to type bool prevents this derivation. Our teaching programming language has distinct int and bool types and no implicit conversions between them.

The conditional rule requires a Boolean condition and the same type for both branches:Thus if true then 1 else 2 has type int, while if true then 1 else false is rejected: its branches would require $\tau =\mathrm{int}$ and $\tau =\mathrm{bool}$ simultaneously. Even a branch that will not execute is checked by this rule. This is a rule of this particular type system; a different programming language can choose different rules. ^[ref]

The useful feature is compositional reasoning: after checking the parts, a rule explains how to check the whole. The function type diagram shows this for a call. Type inference can discover the required types automatically, and type variables let one express relationships that recur across many concrete types. The result is both a practical early error detector and a small, readable derivation explaining why an expression fits its intended use.

The guarantee depends on the rules and execution model. Type safety can exclude specified failures such as adding a Boolean or calling an integer as a function. It does not by itself establish every desired runtime property or guarantee that execution terminates. A type system that permits unrestricted recursion can accept a computation that runs forever; exception handling also needs its own account of permitted outcomes.

A memory access whose execution is observable under the source language or machine rules, so that replacing repeated accesses by a saved value can change behavior. The precise guarantees depend on the programming language; volatile access alone does not provide thread synchronization.