Functional dependencies are a popular extension to Haskell’s typeclass 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 FC. 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 FC.
@inproceedings{haskell2017a,
title = {Elaboration on Functional Dependencies},
author = {Georgios Karachalias and Tom Schrijvers},
year = {2017},
booktitle = {ACM SIGPLAN Haskell Symposium},
url = {/Research/papers/haskell2017a.pdf},
abstract = {Functional dependencies are a popular extension to Haskell’s typeclass
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 FC.
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 FC.
},
}