[TYPES] Constraint-Based Type Inference for Guarded Algebraic Data Types

[Francois Pottier]

Hello all,

Vincent Simonet and I would like to announce the availability of the following
draft paper, which has been submitted to a journal. Comments of all kinds are
very much welcome.

  Title:
  Constraint-Based Type Inference for Guarded Algebraic Data Types

  URL:
  http://pauillac.inria.fr/~fpottier/publis/simonet-pottier-hmg.pdf

  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 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.

-- 
François Pottier
Francois.Pottier at inria.fr
http://pauillac.inria.fr/~fpottier/