Horn clauses and first-order resolution are commonly used to implement type classes in Haskell. Several corecursive extensions to type class resolution have recently been proposed, with the goal of allowing (co)recursive dictionary construction where resolution does not terminate. This paper shows, for the first time, that corecursive type class resolution and its extensions are coinductively sound with respect to the greatest Herbrand models of logic programs and that they are inductively unsound with respect to the least Herbrand models. We establish incompleteness results for various fragments of the proof system.
CITATION STYLE
Farka, F., Komendantskaya, E., & Hammond, K. (2017). Coinductive soundness of corecursive type class resolution. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10184 LNCS, pp. 311–327). Springer Verlag. https://doi.org/10.1007/978-3-319-63139-4_18
Mendeley helps you to discover research relevant for your work.