An extension of HM(X) with bounded existential and universal data-types

  • Simonet V
  • 9


    Mendeley users who have this article in their library.
  • 4


    Citations of this article.


We propose a conservative extension of {HM(X)}, a generic constraint-based type inference framework, with bounded existential (a.k.a. abstract) and universal (a.k.a. polymorphic) data-types. In the first part of the article, which remains abstract of the type and constraint language (i.e. the logic X), we introduce the type system, prove its safety and define a type inference algorithm which computes principal typing judgments. In the second part, we propose a realistic constraint solving algorithm for the case of structural sub-typing, which handles the non-standard construct of the constraint language generated by type inference: a form of bounded universal quantification.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Vincent Simonet

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free