# How does the free program identifiers (fpi) extend over constraints and type schemes in $HM(X)$?

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\}$$?

• 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? – manu Jan 15 '19 at 16:34
• 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=10.1.1.7.7745 – manu Jan 16 '19 at 13:45