Coinductive soundness of corecursive type class resolution

František Farka*, Ekaterina Komendantskaya, Kevin Hammond

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)
31 Downloads (Pure)


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.

Original languageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation
Subtitle of host publicationLOPSTR 2016
Number of pages17
ISBN (Electronic)9783319631394
ISBN (Print)9783319631387
Publication statusPublished - 25 Jul 2017

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


  • Coinduction
  • Haskell
  • Herbrand models
  • Horn clauses
  • Resolution
  • Type classes

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Coinductive soundness of corecursive type class resolution'. Together they form a unique fingerprint.

Cite this