A constraint-based approach to guarded algebraic data types

Abstract

We study HMG( X ), an extension of the constraint-based type system HM( X ) with deep pattern matching, polymorphic recursion, and guarded algebraic data types . Guarded algebraic data types subsume the concepts known in the literature as indexed types , guarded recursive datatype constructors , (first-class) phantom types , and equality qualified types , and are closely related to inductive types . Their characteristic property is to allow every branch of a case construct to be typechecked under different assumptions about the type variables in scope. We prove that HMG( X ) is sound and that, provided recursive definitions carry a type annotation, type inference can be reduced to constraint solving. Constraint solving is decidable, at least for some instances of X , but prohibitively expensive. Effective type inference for guarded algebraic data types is left as an issue for future research.