# Type Theory

Here is a nice thread on what a type is. Mélitte is nice toy implementation of Martin-Löf Type Theory.

Daniel writes interesting type theory code.

## Notes

- A value is some concrete thing, and a type is a collection of concrete things (but is itself not a concrete thing. For example any individual integer is a value, but the collection of all integers is a type. Much like elements and sets in set theory.
- A type is a collection of values which inhabit that type. A type is a value which is a member of the type of types.
- Type theory goes much much further than just tagging data.
- The type determines which data structure you use.
- Dependent types is basically about being able to express arbitrary things in your type system, meaning that you can construct arbitrary proofs. That's how Coq, Agda and Idris work.
- Types are types and propositions are propositions; types come from programming languages, and propositions from logic, and they seem to have no relation to each other.
- Types are specifications of behavior.
- Roughly speaking, a type is a specification of its possible values.
- Generics should not force you to mention irrelevant information.

## Links

- Learn TT - A collection of resources for learning type theory and type theory adjacent fields.
- Homotopy Type Theory lecture materials
- A textbook on informal homotopy type theory
- Homotopy type theory book
- GHOTL Project scope and outline plan - Good read.
- What I wish I knew when learning HoTT
- Collected works of Per Martin-Löf - Web version.
- Type Theory: Does understanding of the Curry-Howard correspondence make you a better programmer?
- Hazel - Live functional programming environment with typed holes. (Web)
- LaTTe - Laboratory for Type Theory experiments (in clojure).
- TT Lite - SuperCompiler for Martin-Löf's Type Theory.
- Implementation of spartan type theory
- Why Types Matter
- Introduction to type theory based on meaning explanations
- SymmetryBook - Undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
- nbe-for-mltt - Normalization by Evaluation for Martin-Löf Type Theory.
- Martin Escardo's research
- Lambdas are Codatatypes (2019)
- On the Relationship Between Static Analysis and Type Theory (2019) (Lobsters)
- [Timeline for Logic, λ-Calculus, and Programming Language Theory (2012)(http://fm.csl.sri.com/SSFT15/Timeline.pages.pdf) (HN)
- Types and Programming Languages Book (2002) (Code) (Book Page) (HN)
- Type Theory and Formal Proof book
- qtt - Quantitative Type Theory implementation.
- Normalization by evaluation for Martin-Löf Type Theory with dependent records
- Introduction to Type Theory (2019)
- No, dynamic type systems are not inherently more open (2020) (HN) (Lobsters)
- Hindley-Milner type system/Algorithm W study (2018)
- HN: So you want to write a type checker
- What are the common ways of performing typechecking? (2019)
- mlsub - Prototype type inference engine.
- Papers and talks around type inference
- Low-Level Liquid Types
- PRL Project - Implementing computational mathematics and providing logic-based tools that help automate programming.
- Code is Engineering; Types are Science (2020) (HN)
- Implementation of "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism" in Rust (Paper)
- Milner Award Lecture: The Type Soundness Theorem That You Really Want to Prove (and now you can)
- Experimenting with Dependent Type Theory in Rust
- Making Illegal States Unrepresentable (2020) (Lobsters)
- Beautiful, interactive visualizations of logical inference
- Type Inference by Example
- First-Class Dynamic Types (2019)
- Gradual Typing for Extensibility by Rows (2019)
- Graduality and Parametricity: Together Again for the First Time (2020)
- Abstracting gradual typing: metatheory and applications (2019)
- Gradual Typing as if Types Mattered (2020)
- Disjoint Intersection Types: Theory and Practice (2018)
- The Fire Triangle (2020)
- Foreign Function Typing: Semantic Type Soundness for FFIs (2020)
- Bidirectional Typing (2019)
- Refinement Kinds (2019) - Type-safe Programming with Practical Type-level Computation.
- Refinement type contracts for verification of scientific investigative software (2019)
- Design and Evaluation of Contracts for Gradual Typing (2019)
- Manifest Contracts with Intersection Types (2019)
- Kinds are calling conventions (2019)
- Space-Efficient Monotonic References (2020)
- Label-Dependent Session Types (2019)
- Tabled Typeclass Resolution (2020)
- A type and effect system for uniqueness and immutability (2018)
- Inferring Types and Effects via Static Single AssignmentLeonardo
- smalltt - Demo for high-performance type theory elaboration.
- Hoare Type Theory - Contains the main libraries of Hoare Type Theory (HTT) for reasoning about sequential heap-manipulating programs.
- Type inference under the hood (2019)
- Type inference for beginners (2019)
- Algorithm W Step by Step (2006) - Implementation of the classic algorithm W for Hindley- Milner polymorphic type inference in Haskell.
- Elaboration with First-Class Implicit Function Types (2020) (Code)
- Experimental type-checker for internally parametric type theory
- Type Systems as Macros (2017)
- Compositional Explanation of Types and Algorithmic Debugging of Type Errors (2001)
- Christian Williams: Structural types for algebraic theories (2020)
- Peter LeFanu Lumsdaine, What are we thinking when we present a type theory? (2020)
- Mathematics in type theory (2020) (HN)
- Division by zero in type theory: a FAQ (2020) (HN)
- Programming in Martin-L ̈of’s Type Theory: An Introduction (1990)
- Type Theory and Functional Programming book (1991)
- Intro To Type Theory (Lobsters)
- Towards Observational Type Theory
- Typing is Hard (Lobsters)
- Types as axioms, or: playing god with static types (2020) (Lobsters)
- The Cartesian Product Algorithm (Type Inference) (1995)
- Martin Hofmann’s contributions to Type Theory: Groupoids and Univalence (2020)
- Demystifying Type Systems (2020)
- Incremental Type Migration Using Type Algebra (2020)
- Things I Was Wrong About: Types (HN)
- Luca Cardelli: Typeful Programming
- Alg - Program that generates all finite models of a first-order theory. It is optimized for equational theories.
- Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification (2020) (Tweet)
- Propositions as types: some missing links (2019)
- SPRITE - Tutorial-style implementation of liquid/refinement types for a subset of Ocaml/Reason.
- Refinement Types: A Tutorial (2020)
- Names are not type safety (2020) (HN)
- A Conversation on FRP, Databases, and Types (2020)
- An extended type system with lambda-typed lambda-expressions (2020)
- lambda-dti - Interpreter of the ITGL with dynamic type inference.
- Session Types without Sophistry
- Finiteness in Cubical Type Theory (2020) (Code)
- Homemade Bidirectional Typing
- BiRelCost - Bidirectional Type Checking for Relational Properties.
- An accessible introduction to type theory and implementing a type-checker (2020)
- Linear ML - Small implementation of a linear type theory in the style of the Benton-Wadler adjoint calculus.
- Implementing Inverse Bidirectional Typechecking
- The intrinsic topology of a Martin-Lo ̈f universe (2012)
- Typing is Hard
- Catt - Infinity categorical coherence typechecker.
- Strongly-typed System F in Haskell
- Native Type Theory (2021) (Lobsters) (HN)
- Simple-sub Algorithm for Algebraic Subtyping (Demo)
- "The Trouble With Types" by Martin Odersky (2013)
- Grothendieck's EGA English Translation (Code)
- Untyped Types (2021)
- Algebra and Data Types (2021) (Lobsters)
- What part of Hindley-Milner do you not understand?
- The Hindley-Milner Type System (2021)
- Formalization of simple type theory
- Modal Type Theory implementation - Toy functional language based on modal type theory. (Code)
- Giml's type inference engine (2021)
- Understanding typing judgments (2016)
- Prototype implementations of systems based on setoid type theory
- Higher-Dimensional Type Theory Course (2020) - Graduate seminar course on the recent development of higher-dimensional type theory. (Code)
- Synthetic mathematics with an excursion into computability theory (2021)
- Counterexamples in Type Systems (Code) (HN) (HN)
- Introduction to Type Systems
- System F Playground
- Building Blocks of the Sasquach Type System (2021)
- Anders - Homotopy Type System with Strict Equality.
- Homotopy Type System - Type theory with two equalities.
- Types versus sets in math and programming languages (2021)
- Let's build a type system in Haskell!
- Bidirectional Typing Rules: A Tutorial (2013) (Code)
- The Hardest Problem in Type Theory [Uniqueness of Identity Proofs] (2021)
- Notes on type theory
- You Could Have Invented De Bruijn Indices (2021)
- type-inference - Unification and type inference algorithms in Haskell.
- Type system innovation propagation (2021)
- Shape Irrelevant Reflection in Type Theory
- Human Aspects of Types and Reasoning Assistants (2021) (Article)
- Where Do Type Systems Come From? (HN)
- Pure type system implemented in OCaml
- Type Systems Toy Implementations
- First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory (2021)
- Topoi — inside and out (2020)
- How to define a PER model (2020)
- Grothendieck's Pursuing Stacks (1983) (Code)
- Should Type Theory replace Set Theory as the Foundation of Mathematics (2021)
- Implementation of a Zeilberger-style linear type theory
- TypicalMath - General-purpose type theory and proof checker generator.
- Proofs and Types (1990)
- EUTYPES-TYPES 2020 - Abstracts (Tweet)
- The critical dimension as an invariant of Type III odometers (2013)
- Introduction to Domain Theory
- Brown Benchmark for Table Types
- Cubical Type Theory (2021)
- Hindley-Milner Type Inference: A Practical Example (2014)
- Learning resources for type inference (2021)
- Basic Polymorphic Typechecking
- An accessible introduction to type theory and implementing a type-checker (2020) (Reddit)
- Swapping arguments of variables in higher-order pattern unification
- Linearity and Uniqueness: An Entente Cordiale (2022)
- Structurally-Typed Condition Handling (2022) (HN)
- Type Checking as Calculation (2022) (HN)
- Agnostic Extensional Type Theory - Parameterized extensional type theory parameterized by a choice operator, and interpreted by a forcing interpretation parameterized by a modality.
- System-F type-checker written in Haskell
- Path Semantics - Research project in path semantics, a re-interpretation of functions for expressing mathematics.
- Type Theory for Memory Allocation and Data Layout
- Hurricane - Minimal Implementation of HoTT-I Type System (of JetBrains Arend) with definitional Path-β.
- Castle Bravo - Experimental Implementation of HoTT-∂ Type System with definitional Path-β.
- Understanding higher-kinded types (2022) (Lobsters)
- Types versus sets (and what about categories?) (2022) (HN)
- Bidirectional type checking algorithms for higher-ranked polymorphism
- Example implementation of Algorithm W for Hindley-Milner type inference
- Type-Theoretic Signatures for Algebraic Theories and Inductive Types
- Usable type system for call by push-value
- Type Theory Forall - #16 Agda, K Axiom, HoTT, Rewrite Theory (2022)
- Why Don't More Languages Offer Flow Typing? (2022) (HN)
- Henk: Pure Type System
- Cofibrations in Cartecian Cubical Type Theory
- Core Gallifrey Interpreter
- LaTeX code for a paper on lean's type theory
- Anders: Cubical Type Checker
- Type checker in Haskell
- Implementing XTT, from the papers "A cubical language for Bishop sets" and "Cubical syntax for reflection-free extensional equality"
- Alonzo - STLC type system.
- Classic Algorithm W for type inference in Haskell
- Introductory resources to type theory for language implementers (2022) (Reddit)
- What is a type?
- Interactive Type Inference: Play with algorithm W in your browser (Code)
- Stagedtt - Staged Type Theory.
- System Fω with Row-Polymorphism
- Fωμ type checker and compiler
- Hindley–Milner Type inferencing in C
- Mélitte - Toy implementation of Martin-Löf Type Theory.
- Type inference from scratch (2019) (Video)
- Gradual Typing Across the Spectrum (Web Code)
- Uniqueness Typing Simplified
- Type-Signature - Who Wants to Be a Millionaire - but with types. (Code)
- Implementation of type inference for System F in Scala 3
- Why Duck Typing Is Safe (2020)
- Setoid type theory implementation
- Trebor - Implementation of Observational Type Theory (OTT) and more.
- MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types (2022)
- Erasable coercions: a unified approach to type systems (2014)
- Curry–Howard by example (2021)
- Various attempts to model version control systems in Homotopy Type Theory
- Hindley-Milner type inference (in Rust) (Lobsters)
- Andrej Bauer: "The countable reals" (2022)
- Test the limits of a Linear System F
- Linear F in OCaml
- Hindley-Milner Type Inference implemented in Python
- Types are moving to the right (2023) (Lobsters)
- All you need is higher kinded types (2023)
- Type inference that sticks (2023) (HN)
- cooked-pi - Type checker for λΠ in several different styles.
- How to implement type theory in an hour (2018)
- Type Systems - Luca Cardelli (2004)
- OpenTau: Using OpenAI Codex for Gradual Type Inference - Using Code Language Models for Gradual Type Inference.
- Every type is defined by its intro and elim forms (2023) (Lobsters)
- Minimal TypeScript implementation of Hindley-Milner type inference