[Grace-core] Typing of Number

[Michael Homer]

On Tue, Jun 21, 2011 at 3:26 PM, Michael Homer <mwh at ecs.vuw.ac.nz> wrote:
> Actually, that isn't right - it just requires some bigger changes to
> the type system than I'd been contemplating. Given self-types, a
> numeric tower (digraph really), and a least-upper-bound operation,
> there's a mathematically correct well-typed solution:
>  type Number { self : T <: Number ->
>    +(other : S <: Number) -> LUB(T, S)
>  }
> where Rational -> Complex -> Quaternion, Rational -> Binary64 ->
> Binary128, Binary64 -> ComplexBinary64, and so on. The implementations
> would be nasty but all the types work out, and Rational + Rational =
> Rational, Rational + Binary64 = Binary64, Rational + Complex ->
> Complex, and Number + Number = Number without error.

To bring this up again with more detail: I think there is a way to
have well-typed mixed arithmetic that gives the mathematically-correct
result. The implementation would be nontrivial, and it would still be
possible to have dynamic errors in some cases, but the common cases
should be able to be made to work.

The idea is that as well as self-type annotations and bounded type
variables there would be the possibility of referring to the
least-upper-bound type of two types, determined with reference to a
properly-constructed lattice of types, which would look something like
this: <http://ecs.vuw.ac.nz/~mwh/number.png>. The return type of an
operation would be the least upper bound of the receiver and argument
types, the point where the paths following the arrows from each type
join up. The type definition would be something like this:
  type Number { self : selfType ->
    +(other : T <: Number) -> LUB(selfType, T)
  }
where "<:" gives an upper-bounded type variable and LUB uses that
lattice for (static) least-upper-bound calculation.

With that type Rational + Rational gives a Rational, but both Rational
+ Binary64 and Binary64 + Rational give Binary64, and Complex and
Rational interoperate cleanly. When one type is not known exactly the
least-upper-bound relation will still give a valid supertype
statically. The lattice doesn't necessarily represent the subtype
relation, just the desired outcome, so Rational need not be a subtype
of Binary64. It is a descendant in the lattice in order to preserve
the annotation of inexactness, while Rational -> Complex because it's
the more expressive.

On the implementation side the numeric classes will be pretty ugly,
but no more so than they would be if the static return types were
always Number. They would have to perform typecasing or double
dispatch and ensure that the ultimate dynamic return type fit within
the static, which may require some sort of flow-sensitive analysis to
confirm. It's still possible for some types not to be compatible with
each other, either by design (consider GF(n) or matrix types) or lack
of implementation, but all of the common cases should be covered with
the expected behaviour. At least the builtins and familiar
mathematical types should just work without explanation.

I don't know how that lattice is defined or extended (if it isn't
based on subtyping), and I'm not sure whether the same feature is
useful anywhere else. This approach should allow everything to behave
in the intuitive way, at the expense of all the complexity I just
described behind the scenes. I don't know whether it's worth the
baggage in order to have Numbers behave like numbers, but it should be
possible.
-Michael