Type-Level Programming with Match Types
summary
Formalizes a type‑level pattern matching mechanism in a System F sub calculus and proves soundness with a Coq mechanization of about 6,000 lines, implements match types in the Scala 3 reference compiler, and shows they integrate with subtyping by requiring disjointness checks and ordered patterns so type reduction matches term reduction. Includes a practical DSL example that tracks tensor dimensions at compile time and notes type checking may diverge so compiler timeouts are used in practice.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 4:00Second Example
- 6:30Syntax
- 8:25Evaluation
- 9:10Match Type Reduction
- 9:55Jointness
- 12:15Receptive Proof
- 14:10Case Study
- 16:05Questions
related talks
41mThe Dialectics of Type-Level Programming
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
48mA gentle introduction to type level programming in Scala
50mA Type-Theoretic Framework for Certified Meta-programming
44mType level Computations in Scala
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
29mTheoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning
01h 57mTypes as Program Specifications: A Intro to Type-Level Programming in Haskell