[Grace-core] Typing of Number

[Andrew P. Black]

Michael

I was confused at first because I thought that you intend your lattice to be a supertype or subtype lattice, and I couldn't figure out which.  Then you pointed out that it is neither.  What you are proposing looks very much like the idea of the "generality hierarchy" that was used to do the numeric types in Smalltalk (in the BlueBlook, IIRC).

As you say, the issue is whether the benefits are worth the costs.   I'm wondering about "baking in" a simplified version of your generality hierarchy, just for the built-in Numeric types, where all of the meets and joins are explicitly written.

In the meantime, my task for today is to sketch an implementation of a single NUmber type that is implemented by multiple classes of objects.  The,perhaps, we can see if we can put your type annotations on it.

	Andrew

On 21 Jun 2011, at 22:21 , Michael Homer wrote:

> 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