Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

Cited literature [44 references]  Display  Hide  Download

https://hal.inria.fr/inria-00070544
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 8:49:15 PM
Last modification on : Thursday, October 22, 2020 - 12:22:01 PM
Long-term archiving on: : Sunday, April 4, 2010 - 8:04:49 PM

Identifiers

  • HAL Id : inria-00070544, version 1

Collections

Citation

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

Share

Metrics

Record views

172

Files downloads

292