Revamping the numeric classes

[Bjorn Lisper]

>> 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