Logic Programming with Extensible Types (Lightning talk)
Logic programming allows structuring code in terms of predicates or relations, rather than functions. Although logic programming languages present advantages in terms of declarativeness and conciseness, the introduction of static types has not become part of most popular logic programming languages, increasing the difficulty of testing and debugging of logic programming code. This paper demonstrates how to implement logic programming in Haskell, thus empowering logic programs with types, and functional programs with relations or predicates. We do so by combining three ideas. First, we use extensible types to generalize a type by a parameter type function. Second, we use a sum type as an argument to introduce optional variables in extensible types. Third, we implement a unification algorithm capable of working with any data structure, provided that certain operations are implemented for the given type. We demonstrate our proposal via a series of increasingly complex examples inspired by educational texts in logic programming, and leverage the host language’s features to make new notation convenient for users, showing that the proposed approach is not just technically possible but also practical.
Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change
16:00 - 17:30 | |||
16:00 30mTalk | MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs PADL Felipe Gorostiaga IMDEA Software Institute, Martin Ceresa IMDEA Software Institute, César Sánchez IMDEA Software Institute | ||
16:30 30mTalk | Checking Concurrency Coding Rules PADL Lars-Åke Fredlund Universidad Politécnica de Madrid, Ángel Herranz Universidad Politécnica de Madrid, Julio Mariño Universidad Politécnica de Madrid | ||
17:00 10mTalk | Can Logic Programming Be Liberated from Predicates and Backtracking? (Lightning talk) PADL Michael Hanus Kiel University | ||
17:10 10mTalk | Logic Programming with Extensible Types (Lightning talk) PADL Ivan Perez NASA Ames Research Center, Ángel Herranz Universidad Politécnica de Madrid, P: Julio Mariño Universidad Politécnica de Madrid |