a function mapping all finite sets to integers. A function which returns the cardinality of a set would be a value of this type. Quantifiers can only appear top level. For instance, a type is excluded by the syntax of types. Also monotypes are included in the polytypes, thus a type has the general form , where is a monotype. Equality of polytypes is up to reordering the quantification and renaming the quantified variables (-conversion). Further, quantified variables not occurring in the monotype can be dropped. Context and typing To meaningfully bring together the still disjoint parts (syntax expressions and types) a third part is needed: context. Syntactically, a context is a list of pairs , called assignments, assumptions or bindings, each pair stating that value variable has type All three parts combined give a typing judgment of the form , stating that under assumptions , the expression has type . Free type variables In a type , the symbol is the quantifier binding the type variables in the monotype . The variables are called quantified and any occurrence of a quantified type variable in is called bound and all unbound type variables in are called free. Additionally to the quantification in polytypes, type variables can also be bound by occurring in the context, but with the inverse effect on the right hand side of the . Such variables then behave like type constants there. Finally, a type variable may legally occur unbound in a typing, in which case they are implicitly all-quantified. The presence of both bound and unbound type variables is a bit uncommon in programming languages. Often, all type variables are implicitly treated all-quantified. For instance, one does not have clauses with free variables in Prolog. Likewise in Haskell, where all type variables implicitly occur quantified, i.e. a Haskell type a -> a means here. Related and also very uncommon is the binding effect of the right hand side of the assignments. Typically, the mixture of both bound and unbound type variables originate from the use of free variables in an expression. The constant function K = provides an example. It has the monotype . One can force polymorphism by . Herein, has the type . The free monotype variable originates from the type of the variable bound in the surrounding scope. has the type . One could imagine the free type variable in the type of