[Grace-core] Typing of Number

[Michael Homer]

Hi,
I've been looking at implementing support for types in the language,
and as well as the syntactic ambiguities Kim mentions in the other
post I'm having trouble even putting them together. Since I will be
implementing the numeric types soon I started out writing a definition
for Number to parse and instantiate:
  type Number {
    +(Number) -> Number
  }
Fine so far, but when I move on to the subtypes (§4.1) there's a problem:
  type Binary64 {
    +(Number) -> Number
    isNaN -> Boolean
  }
  type Rational {
    +(Number) -> Number
    denominator -> Number
    numerator -> Number
  }
These types are fairly useless, since any operations on them discard
the type information:
  var a : Rational := 3
  var b : Rational := 4
  var c : Rational := a + b // Type error

The specification is currently a little ambiguous on whether these are
true types - if they are just classes implementing a shared public
interface then this isn't an issue, though they become pretty
difficult to use in other ways then as well. It seems like what they
need is a type variable for self (for which I have invented syntax; if
these are to be supported that will need to be specified):
  type Number { self : T ->
    +(T) -> T
  }
  type Binary64 {
    +(Binary64) -> Binary64
  }
  type Rational {
    +(Rational) -> Rational
  }
With this arrangement the previous problem is eliminated, but there is
a new (worse) one:
  var a : Rational := 3
  var b : Binary64 := 4.asBinary64
  var x : Number := a
  var y : Number := b
  var z : Number := x + y // Runtime error
There are other arrangements of type variables, parameter types, and
return types, all of which give the same kind of problem somehow.

The last example also shows up another question: what is the dynamic
type of the result of mixed-type arithmetic? Those operations must be
supported in order for the Number type to work, but it's unclear what
the type of Binary64 + Rational should be, with reasonable arguments
for different results. It could be Rational as the most precise type
(ignoring ±Inf and NaN), or Binary64 as the *least* precise type, or
Binary64 as the receiver. Only Binary64 (or Number) seems to be
typeable, given that methods are not overloaded.

It's simple enough to pick a defensible answer by fiat for the
built-in types, but user-defined numeric types should be possible as
well:
> Grace's libraries may support a range of additional numeric types,
> such as machine integers, bytes, longer and shorter floating point
> numbers, and complex numbers. These types don't need to be built-in:
> one of our design goals is to make library classes as convenient to
> use as built-in classes, so not being built-in does not mean that
> they are "second-class" in any way.
> [from <http://gracelang.org/applications/2010/11/18/built-in-objects-booleans-strings-and-numbers/>]
For these types to be possible they have to be interchangeable with
the built-in numeric types, and Number + Number needs to work for all
numbers (or does it? I can imagine number types that are entirely
incompatible with each other, but whether supporting those is worth
allowing unchecked runtime errors from arithmetic I don't know.
Infinities and NaNs might give rise to that from the builtins anyway).
It seems that they will all need to be coercible to Rational in order
for that to work, and consequently the return type of Number
operations is the dynamic type of the receiver, requiring
explicitly-typed self-references. The argument is coerced to the
receiver's type, giving these types:

  type Number { self : T ->
    +(Number) -> T
  }
  type Binary64 {
    +(Number) -> Binary64
  }
  type Rational {
    +(Number) -> Rational
  }

That does mean that something like this will not behave as expected:
  var complex : Complex := Complex.new(2, 1) // 2 + 1i
  (2 * complex) == 4 // True!
  (2 * complex).imaginary // Static error
  // But:
  (complex * 2).imaginary // OK
It does appear to give at least a consistent typing, and allow the
programmer to keep all calculations within Rational or Binary64 if
they wish. As soon as they're mixed together
you end up in no-man's land. There will be different semantics than
most other languages.

I'm not entirely certain that these types mean anything in a
structurally-typed world anyway, since someone can define a class
meeting the Rational interface with any behaviour and any storage, but
any other arrangements seem to make them totally irrelevant even on
the surface.

There are three other options I can see, all of which involve bigger
changes to how I understand the language to work today:
1) Open/extensible classes, where a new numeric type would be expected
to override Rational.+ and Binary64.+ to accept itself (as Ruby's
Complex type does).
2) "Reverse +" methods, where in the event of a type error
Rational.+(other : Complex) would invoke other.reverse_plus(self),
which figures out the right thing to do (as Python's Complex type
does).
3) Overloading method dispatch on return type (as in Haskell, or
Perl's wantarray()).
I presume #3 is right out, #1 seems to have been set aside, and #2 is
a little ugly. Both #1 and #2 make a mess of typing as well, as far as
I can tell.

Is my reasoning correct? If so, what should the syntax for self-type
annotations be? If not, how do these types work and how is that
expressed?
-Michael