Building a Dependently Typed Language in Haskell Part 1
summary
Recreates a minimal dependently typed core in Haskell: concrete syntax, locally nameless binding, bidirectional type checking, evaluation that produces values as closures and neutral terms so partial evaluation decides type equality by quoting to normal forms. Implements infer/check functions, environment carrying typed values, fresh-name generation and a small eval/check monad; demos include a polymorphic identity and its instantiations. Code exists but full cleaned repository not yet released.
AI-written summary · about
chapters (12)
- 0:00Introduction And Motivation
- 6:05From Eliminators To Pattern Matching
- 11:25Syntax Of A Dependently Typed Language
- 17:56Bidirectional Type Checking Design
- 20:02Locally Nameless Representation
- 26:43Evaluation And Type Equality
- 35:55Values, Closures, And Neutral Terms
- 49:43Implementing Type Inference
- 58:40Type Checking Lambda Expressions
- 1:00:15Quoting And Normal Forms
- 1:05:32Polymorphic Identity Example
- 1:06:38Preparing For Data Types And Pattern Matching
related talks
59mKeynote: Dependently-Typed Haskell
49mMaking sense of the Haskell type system
02h 50mIntro to Type Systems and Operational Semantics
34mGraded Monads and Type-Level Programming for Dependence Analysis
25mBinding Syntax for Dependently-Typed Programs
18mDeveloping a Dependently Typed Language with Runtime Proof Search
19mDeriving Dependently-Typed OOP from First Principles
19mA Dependently Typed Language with Dynamic Equality