# Revamping the numeric classes

**Bjorn Lisper
**
lisper@it.kth.se

*Thu, 8 Feb 2001 10:02:23 +0100 (MET)*

>>* It is quite similar in spirit to the concept of principal type in
*>>* Hindley-Milner type systems. An expression can have many types but
*>>* only one "best" (most general) type in that system.
*
>*Now, I'm not any kind of expert on this, but isn't the most general
*>*HM type one that encompasses the others, and *not* one out of a set of
*>*ambigous (and mutually exclusive) types?
*
In a sense. You define a partial order on types by a < a' (a more general
than a') if there is a substitution s of type variables such that
a' = sa. The interesting property of HM type systems is that for each term t
and all type judgements t:a that can be derived, there is a type judgement
t:a' such that a' < a. a' is called the most general type of t.
What I suggested was to define a different relation between types, measuring
"relative liftedness". We can call it "<<". Now, if it is the case that for
all judgements t -> t':a in the type system I sketch, there is a judgement
t -> t'':a' where a' << a, the we can select the transformation to be
t -> t''. t'' will then have a "most general type" among the possible
transformed terms, but wrt << rather than <.
Ambiguity between types depends on the ordering between types that you
consider!
Björn Lisper