An Independent History of Implicit Language Application
summary
The talk shows how recursion and recursive data structures can be encoded at the type level in Scala by using a type-level fixed point and an ifix/list-like encoding. It demonstrates a small engine implemented with case classes and infix type constructors (about a seven-line core) that generates inductive lists and leverages Scala’s type inference to move work into the typechecker, and it notes practical issues around termination and tooling integration.
AI-written summary · about
chapters (11)
- 0:00Implicit language intro
- 1:00Fixed point operator
- 3:00Recursion and higher-order functions
- 6:38Fixed point functions
- 9:11Fixed point in Scala types
- 11:02Type inference and case classes
- 13:57Type-level lists with fixed point
- 16:30Terminating inductive lists
- 18:06Engine versus typing search
- 19:34Scala type inference integration
- 20:35Q&A
related talks
47mIdris For (Im)practical Scala Programmers
24mLet the Scala compiler work for you
45mTypelevel Programming 101: The Subspace of Scala
46mImplicits Inspected and Explained
43mDon't Fear the Implicits: Everything You Need to Know About Typeclasses
01h 02mPrinciples and tools to cleverly model your data in Scala
29mIntroduction to Recursion Schemes
30mDotty and types: the story so far