Coinductive soundness of corecursive type class resolution

DOI10.1007/978-3-319-63139-4_18MaRDI QIDQ2409746zbMATH OpenOpenAlexFDO

Authors František Farka, Ekaterina Komendantskaya, Kevin Hammond

Publication date 13 October 2017

Full work available at URL https://arxiv.org/abs/1608.05233

zbMATH Keywords

coinductionHaskellHerbrand modelsHorn clausesresolutiontype classes

Mathematics Subject Classification ID

Logic in computer science (03B70) Logic programming (68N17) Functional programming and lambda calculus (68N18)

Abstract: 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 termi- nate. 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 induc- tively unsound with respect to the least Herbrand models. We establish incompleteness results for various fragments of the proof system.

Recommendations

• Proof relevant corecursive resolution
• A type-theoretic approach to resolution
• Coinductive subtyping for abstract compilation of object-oriented languages into Horn formulas
• scientific article; zbMATH DE number 2185708
• Soundness and completeness proofs by coinductive methods

Cited in

(6)

• Logic programming: laxness and saturation
• Proof relevant corecursive resolution
• scientific article; zbMATH DE number 5872252 (Why is no real title available?)
• Proof-relevant Horn clauses for dependent type inference and term synthesis
• Practical Proof Search for Coq by Type Inhabitation
• Coinduction in uniform: foundations for corecursive proof search with Horn clauses

This page was built for publication: Coinductive soundness of corecursive type class resolution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2409746)