Type Inference for GADTs, OutsideIn and Anti-unification
Published in SBLP - Brazilian Syposium on Programming Languages, 2018
Support for generalized algebraic data types (GADT) in extensions of Haskell allows functions defined over GADTs to be written without the need for type annotations in some cases, but it requires type annotations in most of them. This paper presents a type inference algorithm for GADTs that extends OutsideIn algorithm using anti-unification to capture the relationship between the types of arguments and result of GADT functions. This approach allows inference in cases where the relationship between types of pattern matches is explicit in the code, allowing the type annotation in cases where the relationship is not explicit.