Type Systems & Functional Constructs

← Back to Domain-Specific Families

Abstractions about how programs and expressions are typed, composed, and dispatched, covering type systems and theories (type inference, simply typed lambda calculus, intuitionistic type theory, kinds, bottom types), functional constructs (anonymous functions, Mogensen-Scott encoding, monad transformers), and classes, predicate dispatch, and Liskov substitution.

18 abstractions in this family — domain-specific abstractions that sit near one another in structural-signature space (k-means over structural-signature embeddings). Each is shown with its short description.

• Anonymous Function — Construct a callable value at an expression site without declaring a persistent function name as part of that construction, so behavior can be invoked, passed, returned, stored, or composed inline.
• Bottom Type — The least type in a declared subtyping order, below every type and useful for typing paths that return no ordinary value.
• Function-Level Programming — Build programs from whole programs through a closed vocabulary of program-forming operations, so program construction becomes an algebra over functions rather than a value-level expression with variables.
• Intuitionistic Type Theory — A constructive dependent type-theory family that treats propositions as types and proofs as terms governed by explicit formation, use, and computation rules.
• Kind (Type Theory) — A type-level classifier that governs which types and type constructors can be formed or applied.
• Liskov Substitution Principle — Certify that a subtype can safely replace its supertype only when it honours the supertype's full contract toward clients — weakening preconditions, strengthening postconditions, preserving invariants — regardless of taxonomy or compilability.
• Mogensen–Scott encoding — Mogensen–Scott encoding represents constructor data as functions that select a matching handler and expose immediate fields.
• Monad Transformer — A constructor that turns an eligible base monad into a new monad and lawfully lifts base computations into it.
• Ordinal Data Type — An ordinal data type gives its language-defined values ordered integer positions that support stepping and contiguous subranges.
• Predicate Dispatch — A guarded method-selection mechanism that tests arguments for applicability and, in its formal form, orders applicable implementations by predicate implication.
• Programming Class — A programming-language construct that defines a kind of object and governs how its instances are created and obtain attributes or behavior.
• Signedness — A programming-language type property that determines whether an integer representation and its operations include negative values or instead use a nonnegative modular range, affecting conversions, comparison, overflow, and interfaces.
• Simply typed lambda calculus — The term simple type is also used to refer to extensions of the simply typed lambda calculus with constructs such as products, coproducts or natural numbers (System T) or even full recursion (like PCF).
• String-to-String Correction Problem — Find the minimum total cost of transforming one symbol string into another by permitted single-symbol edits.
• Thompson's Construction — A compositional conversion of a classical regular expression into a language-equivalent ε-NFA.
• Type Inference — Algorithmically reconstruct the types of expressions from their usage context rather than from annotations, by generating an equality constraint at each syntactic form and solving them by unification to return either each expression's principal (most general) type or a genuine type error.
• Type System — A discipline that assigns every value and expression a type and uses that classification to constrain which operations may legally apply, verifying via compositional typing rules that well-typed programs cannot reach a wrong-kinded state (soundness).
• Well-Formed Formula — In mathematical logic, propositional logic, and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet, constructed following the defined grammar of a formal language.