Terminating constraint set satisfiability and simplification algorithms for context-dependent overloading

Brazilian Computer Society. Journal

Lucí¹  Rodrigo Ribeiro²  o⁴  Carlos Camarã⁶  lia Figueiredo⁷ 

[1]ã

[2]Instituto de Ciê

[3]gicas, Departamento de Computaç

[4]ncia da Computaç

[5]ncias Exatas e Bioló

[6]ncias Exatas, Departamento de Ciê

[7]o, Universidade Federal de Minas Gerais, Belo Horizonte, Brazil

[8]o, Universidade Federal de Ouro Preto, Ouro Preto, Brazil

关键词: Haskell;    Constraint set satisfiability;    Constraint set simplification;    Termination;   

DOI  :  10.1007/s13173-013-0107-9

学科分类：农业科学（综合）

来源: Springer U K

【 摘 要 】

Algorithms for constraint set satisfiability and simplification of Haskell type class constraints are used during type inference in order to allow the inference of more accurate types and to detect ambiguity. Unfortunately, both constraint set satisfiability and simplification are in general undecidable, and the use of these algorithms may cause non-termination of type inference. This paper presents algorithms for these problems that terminate on any given input, based on the use of a criterion that is tested on each recursive step. The use of this criterion eliminates the need of imposing syntactic conditions on Haskell type class and instance declarations in order to guarantee termination of type inference in the presence of multi-parameter type classes, and allows program compilation without the need of compiler flags for lifting such restrictions. Undecidability of the problems implies the existence of instances for which the algorithm incorrectly reports unsatisfiability, but we are not aware of any practical example where this occurs.

【 授权许可】

CC BY