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, andguarded algebraic data types. Guarded algebraic data types subsume the concepts known in the literature asindexed types,guarded recursive datatype constructors,(first-class) phantom types, andequality qualified types, and are closely related toinductive 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 ofX, but prohibitively expensive. Effective type inference for guarded algebraic data types is left as an issue for future research.

This publication has 26 references indexed in Scilit: