Chapter 10 of Advanced Topics in Types and Programming Languages; gives a very comprehensive description of type inference by constraints solving.

They introduce the free program indentifiers of an environment $\Gamma$ with the pair of equations $fpi(\emptyset) = \emptyset$ and $fpi(\Gamma;x:\sigma) = fpi(\Gamma) \cup fpi(\sigma)$.

I would like some clarification for the $fpi(\sigma)$ term. Does it contains the set of free type variables ($ftv$)?

Specifically they say (page 408):

The sets of free type variables of a type scheme $\sigma$ and of a constraint $C$, written $ftv(\sigma)$ and $ftv(C)$, respectively, are defined accordingly... The sets of free program identifiers of a type scheme $\sigma$ and of a constraint $C$, written $fpi(\sigma)$ and $fpi(C)$, respectively, are defined accordingly. Note that $x$ if free in $x \preceq T$.

The last sentence seems to indicate that type variables are program identifiers.

Are there any other program identifiers? Do predicates and the name of ground types are program identifiers?

Is the result of $fpi(x \rightarrow integer)$ the set $\{x, integer, \rightarrow\}$?

  • $\begingroup$ In page 421, they say "...every satisfiable constraint $C$ such that $fpi(C)=\emptyset$..."; so I guess that predicates are not program identifiers, otherwise (obviously true) constrains like $\exists XY.X=Y$ would include the predicate $=$... or should they? $\endgroup$
    – manu
    Jan 15 '19 at 16:34
  • $\begingroup$ I've found the PhD Thesis of Martin Sulzmann "A General Framework for Hindley/Milner Type Systems with Constraints". It even has a Haskell implementation of HM(X) with two instances of X: the one that yields standard HM type system, and another for a dimension type system (seconds, and meters): citeseerx.ist.psu.edu/viewdoc/summary?doi= $\endgroup$
    – manu
    Jan 16 '19 at 13:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.