Constraint-Based Type Inference for Guarded Algebraic Data Types. Vincent Simonet and Francois Pottier.
* 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 typing assumptions. 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.
*

Seems rather interesting.

## Recent comments

6 hours 4 min ago

6 hours 22 min ago

10 hours 42 min ago

11 hours 18 min ago

12 hours 3 min ago

12 hours 23 min ago

12 hours 46 min ago

12 hours 58 min ago

13 hours 30 min ago

13 hours 39 min ago