Total Type Classes
summary
Identifies a pattern where type classes over data kinds are provably total and implements a GHC plugin that (1) verifies totality by doing exhaustiveness, termination, precondition checks, (2) injects placeholder evidence during typechecking, and (3) rewrites the typechecked program to add real constraint parameters and propagate them across calls and module boundaries. Demonstrates the rewrite for sing/Vector-style examples and effect-list catalogs, reports sound but incomplete checking (undecidable in general) and limitations with higher-rank types and some mutually recursive instance patterns.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:49Why total type classes matter
- 3:36Type-level naturals and vector length
- 5:20Formalizing total constraints
- 8:07Syntax and GHC plugin
- 9:13Checking totality
- 13:29Exhaustiveness and termination
- 16:37Rewriting with constraints
- 19:23Real-world applications
- 21:54Summary
- 22:15Question and answer session
related talks
24mTypeclasses: the value of programming vocabulary
20mType Classes for the Rest of Us
59mHaskell Design Patterns for Genericity & Asynchronous Behavior
01h 15mTypes are like the Weather, Type Systems are like Weathermen
45mTDD, as in Type-Directed Development
52mType Theory and its Meaning Explanations
44mTelling the Truth with Types
16mVerifying Replicated Data Types with Typeclass Refinements in Liquid Haskell