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.

TypeScript implementation of Hindley-Milner type inference is good read.

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
• Less-technical introductions to type checking (2023)
• Interaction Type Theory
• Sliding In a Type Checker (2023)
• Type Checking with Eqlog: Typing (2023)
• How do I read type systems notation (Lobsters) (HN)
• Type Inference Library written in TypeScript