Scale By The Bay 2018 Unconference: Sergei Winitzki
summary
A Scala macro library generates concrete implementations from polymorphic type signatures by translating types into logic, running an LJT proof search to build lambda-term proofs, and emitting Scala code; it ranks alternatives with an information-loss scoring heuristic so it prefers implementations that use more inputs. It supports products, coproducts and function types, attaches a symbolic lambda-term AST for law verification at runtime, runs at compile time, and explicitly does not infer recursion or type-class operations like monads.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:04Generating code from types
- 2:36Macro implementation demo
- 4:22Type signature examples
- 14:43Theory behind the algorithm
- 20:03Proof search in intuitionistic logic
- 26:52Code generation from proofs
- 31:35Generating type class instances
- 39:50Automatic derivation limits
