[Grace-core] Typing of Number

[Michael Homer]

On Tue, Jun 21, 2011 at 11:35 AM, Michael Homer <mwh at ecs.vuw.ac.nz> wrote:
> On Tue, Jun 21, 2011 at 9:02 AM, James Noble <kjx at ecs.vuw.ac.nz> wrote:
>>> Also, Michael's lament:
>>>
>>>> with the "once inexact,
>>>> always inexact" behaviour you'd [often] end up with "everything inexact",
>> This is also an argument that the static type system should be able to track this distinction.
>
> Well, right. It is valid to say that it just can't, but then the
> numeric types don't achieve very much.
>
> I do think that if there's a
> Rational type it should be possible to constrain yourself to remaining
> within it somehow. I also think Number + Number ought to work other
> than in very exceptional cases, by the principle of least surprise.
>
> If mixed-type operations are allowed, I don't see how the type system
> can track "anything with Binary64 results in Binary64" without
> multiple dispatch.
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.

I'm not sure how that type lattice is defined or extended, and it's a
big chunk of complexity in the type system for a special case (albeit
an important one), but it is at least possible to make it work. There
can still be error cases but they're hopefully much more obscure. Is
that complication worthwhile?
-Michael