Compile-time Logic Programming in Scala: what for?
summary
Claim: Scala implicit resolution maps to Prolog-style logic so the compiler can perform compile-time Prolog via Scala implicits by encoding atoms as traits, terms as type parameters, and facts/rules as implicit defs. Uses HLists for heterogeneous lists, derives JSON typeclass writers and canBuildFrom instances, and proves an Akka Streams type-safe Akka Streams closed shape proof at compile time. Debugging uses -Xlog-implicits, the displaying compiler plugin and IntelliJ implicit hints. Limits include no multi-result inference, ambiguous implicit failures, and observed exponential compile-time blowup.
AI-written summary · about
chapters (7)
- 0:00Compile-time logic programming intro
- 2:23Prolog basics quick intro
- 12:16Prolog to Scala implicits
- 23:36Logic programming examples
- 30:42Type-safe graph validation
- 46:00Debugging implicit limits
- 48:33Conclusion
related talks
41mThe Dialectics of Type-Level Programming
45mLogic Meta Programming for Functional Languages
47mLogic Programming à la Carte
19mAutomated Verification of Fundamental Algebraic Laws
56mCalculating Intuitionistic Logic in Scala
19mType Inference Logics
22mCan Logic Programming Be Liberated from Predicates and Backtracking? (Lightning talk)
31mEmbedding Functional Logic Programming in Haskell via a Compiler Plugin