Elaboration on Functional Dependencies: Functional Dependencies Are Dead, Long Live Functional Dependencies!

Karachalias, G; Schrijvers, T

Karachalias, G (reprint author), Katholieke Univ Leuven, Leuven, Belgium.

ACM SIGPLAN NOTICES, 2017; 52 (10): 133


Functional dependencies are a popular extension to Haskell's type-class system because they provide fine-grained control over type inference, resolve ambiguities and even enable type-level computations. Unfortunately, several aspects of Haskell's functional dependencies are ill-understood. In particular, the GHC compiler does not properly enforce the functional dependency property, and rejects well-typed programs because it does not know how to elaborate them into its core language, System F-C. This paper presents a novel formalization of functional dependencies that addresses these issues: We explicitly capture the functional dependency property in the type system, in the form of explicit type equalities. We also provide a type inference algorithm and an accompanying elaboration strategy which allows all well-typed programs to be elaborated into System F-C.

Download PDF

Full Text Link