The Dialectics of Type-Level Programming
summary
Claim: compilers can compute useful program logic at compile time. Uses Scala and Haskell, plus libraries/ideas from Shapeless and Servant, to force the compiler via typeclass resolution to interpret a type list and generate values and a dispatch function. Builds a type-level event-sink DSL encoded as nested tuples that emits a compile-time coproduct output type and runtime handlers; it works end-to-end but produces brittle, hard-to-read compiler errors. Practical, small kernel implementation without macros.
AI-written summary · about
chapters (17)
- 0:00Intro
- 2:31Embedded DSLs
- 4:03Not Extensible
- 4:51Type DSL
- 5:33Haskell Servant
- 6:09Haskell Package Manager
- 7:16Servant
- 8:20Building a DSL
- 8:46Heterogeneous Event Sync
- 11:22Event Sync Requirements
- 11:45Building the DSL
- 12:50Encoding
- 19:43Base Case
- 27:20Event Handling
- 35:21Recap
- 37:17Why do we have proxies
- 38:03Summary
related talks
49mCompile-time Logic Programming in Scala: what for?
15mLogic Programming with Extensible Types (Lightning talk)
51mHands-on Typelevel Scala
43mMastering Typeclass Induction
52mWhat logic can teach us, Scala programmers
01h 09mCompilers are Databases
19mIll-Typed Programs Don't Evaluate
15mStaged Compilation with Two-Level Type Theory