HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Constraint-Based Type Inference for Guarded Algebraic Data Types

Abstract : Guarded algebraic data types subsume the concepts known in the literature as indexed types, guarded recursive datatype constructors, and first-class phantom types, and are closely related to inductive types. They have the distinguishing feature that, when typechecking a function defined by cases, every branch may be checked under different assumptions about the type variables in scope. This mechanism allows exploiting the presence of dynamic tests in the code to produce extra static type information. We propose an extension of the constraint-based type system HM(X) with deep pattern matching, guarded algebraic data types, and polymorphic recursion. We prove that the type system is sound and that, provided recursive function definitions carry a type annotation, type inference may be reduced to constraint solving. Then, because solving arbitrary constraints is expensive, we further restrict the form of type annotations and prove that this allows producing so-called tractable constraints. Last, in the specific setting of equality, we explain how to solve tractable constraints. To the best of our knowledge, this is the first generic and comprehensive account of type inference in the presence of guarded algebraic data types.
Document type :
Complete list of metadata

Cited literature [44 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 8:49:15 PM
Last modification on : Thursday, February 3, 2022 - 11:14:11 AM
Long-term archiving on: : Sunday, April 4, 2010 - 8:04:49 PM


  • HAL Id : inria-00070544, version 1



Vincent Simonet, François Pottier. Constraint-Based Type Inference for Guarded Algebraic Data Types. [Research Report] RR-5462, INRIA. 2005, pp.65. ⟨inria-00070544⟩



Record views


Files downloads