Thread (2 posts)

Glossary of Type Theory Concepts

Absolutely Useless

Curry-Howard correspondence - The deep connection between logic and computation where propositions correspond to types and proofs to programs. Likely classified as useless because while philosophically interesting, it doesn't directly help you build a practical compiler or write better programs.

Decidability of type inference - Whether an algorithm can always determine types without annotations. Useless because practical languages often have undecidable type inference anyway (like Haskell) and work fine with heuristics.

Decidability of type checking - Whether checking if a program is well-typed always terminates. The author's note [1] suggests they find proving termination pointless when real type checkers just use timeouts.

Principality of typing - Whether there's always a most general type for an expression. Practical languages often lack principal types but still work well with good error messages.

Completeness - Whether all "true" statements can be proven within the system. A theoretical property with no bearing on whether programmers can write useful code.

Consistency - Whether the system can't prove false statements. While important theoretically, practical languages often have escape hatches anyway.

W-types / TT containers - Inductive types for representing well-founded trees. Too abstract and general-purpose to be useful compared to specific data types.

Church-Rosser theorem - That different evaluation orders yield the same result. Most practical languages don't satisfy this anyway due to side effects.

Universe hierarchies - Stratified levels of types to avoid paradoxes. Adds complexity without helping programmers; practical languages use simpler approaches.

Univalence - Homotopy type theory principle that equivalent types are equal. Extremely abstract with no clear practical benefit.

Basically Useless

Totality (termination + productivity) - Guaranteeing programs always terminate or produce output. Too restrictive for general-purpose programming; Turing-completeness is useful.

Denotational semantics, especially categorical - Mathematical models of program meaning. Operational semantics (how programs execute) is more useful for implementation.

Gradual typing - Mixing static and dynamic typing. Often leads to complex systems that satisfy neither static nor dynamic typing advocates.

More Pain Than Gain

Let-generalization - Inferring polymorphic types for let-bound values. Can lead to confusing type errors and complexity in the type system.

Recursion schemes - Patterns for structuring recursive functions. Often over-engineered compared to simple recursive functions.

Subtyping - Allowing types to be used where supertypes are expected. Note [3] suggests the author finds most forms problematic except specific variants.

Dependent typing - Types that depend on values. Note [5] indicates even restricted forms might be acceptable, but full dependence is too complex.

Refinement typing - Types with predicates constraining values. Note [6] suggests potential if done well, but often cumbersome.

Algebraic effects - Structured way to handle effects like exceptions. Often more complex than traditional effect systems.

Can Be Nice to Have

Union and intersection types - Types that can be one of several types or satisfy multiple types. Useful for expressiveness but not essential.

Proof search - Automatically finding proofs/implementations. Good for tooling like autocomplete but not core functionality.

Row polymorphism - Polymorphism over record fields. Enables flexible record manipulation but adds complexity.

Useful

Parametricity - Properties that hold for all type instantiations. Note [4] mentions needing the right flavor; helps reasoning about generic code.

Polarization - Distinguishing data (positive) from computation (negative) types. Helps optimize compilation and clarify semantics.

Linear typing - Tracking resource usage in types. Enables safe resource management and optimization.

Type-level programming - Computation at the type level. Enables powerful abstractions and compile-time guarantees.

Data type encodings - Representing data types in terms of simpler constructs. Essential for implementing generics efficiently.

Continuations - Reified control flow. Enable powerful control abstractions.

Very Useful

Operational semantics - Formal rules for program execution. Essential for implementing interpreters and compilers correctly.

Type-erasure semantics - How programs behave after removing type information. Critical for efficient compilation.

Normalization by evaluation - Technique for evaluating terms to normal form. Efficient implementation technique for type checkers.

Ad-hoc polymorphism - Overloading functions for different types. Essential for practical programming (typeclasses, traits, etc.).

Coherence - Ensuring consistent behavior across instances. Note [2] mentions importance for instance resolution.

Progress - Well-typed programs can take a step or are values. Core safety property that prevents getting stuck.

Subject reduction (preservation) - Types are preserved during evaluation. Core safety property ensuring type soundness.

Bidirectional typing - Alternating between inferring and checking types. Practical approach to type checking, though not the syntax apparently.

Pattern matching - Destructuring data by shape. Fundamental feature programmers expect.

Exceptions - Error handling mechanism. Practical necessity despite theoretical impurity.

Existentials - Types that hide implementation details. Essential for abstraction and modularity.

Higher-kinded types - Types parameterized by type constructors. Enable powerful abstractions like Functor and Monad.

Metaprogramming - Programs that manipulate programs. Essential for reducing boilerplate and enabling DSLs.

The author clearly values practical implementation concerns, developer ergonomics, and features that enable real programming over theoretical purity or completeness properties.