Logic Programming with Extensible Types (Lightning talk)
summary
Claim: Haskell code gains logic programming by a compile time extensible types par transformation that turns algebraic types into term types with optional variables and a DSL of goals. Implementation uses a term constructor as a sum type, a polymorphic unification on any data requiring a few typeclass operations, and combinators for conjunction disjunction exist and cut. Prototype is an interpreter that solves examples including a Sudoku and list of solutions but currently has poor unification performance and is work in progress.
AI-written summary · about
chapters (7)
- 0:00Logic programming in Haskell
- 1:05Motivation for embedding logic
- 2:36Extensible types for logic
- 5:35Demo of embedded DSL
- 7:45Compile-time transformation
- 9:34Limitations and future work
- 11:14Q&A
related talks
41mThe Dialectics of Type-Level Programming
52mWhat logic can teach us, Scala programmers
42mProgramming with Math
01h 34mFormal Logic Undressed
01h 01mLearning Propositional Logic with Logic Programming
30mConvenient Algebraic Programming with Coercive Subtyping
43mAn Imperishable Wonderland of Infinite Fun
23mReasoning about types and code