[Grace-core] Typing of Number

[Andrew P. Black]

My sense is that we believed that Number should be the only numeric TYPE.  There would be many classes that implemented it, such as Rational, ComplexRational, Binary64, etc.  Maybe there is some very clever way that will let these be types, but I don't see it.

On 19 Jun 2011, at 19:58 , Michael Homer wrote:

>  it's unclear what
> the type of Binary64 + Rational should be, with reasonable arguments
> for different results.

It seems to me that the CLASS of the result has to be Binary64.  Whenever one does arithmetic with inexact numbers, the result must surely be an inexact number.  Maybe multiplying by exact zero is an exception, but in general, once inexact, always inexact

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

But the implementors of the libraries need to write the methods that make the new numbers work with the others.
For this purpose we need to very carefully design the protocol for Number, so that implementors of various Number classes know what they can expect from their arguments.  This will probably some rather confusing double-dsipatch protocol, analogous to Smalltalk's "convert to number and send".

> 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

We can coerce exact numbers to Rational, but not inexact numbers.  The (static) return type of an operation can depend only on the (static) types of the arguments, not on their values, or on their dynamic type, because doing otherwise means that we don't have static typing.  That is exactly why I think that Number must be the only type.

Michael suggested this subtyping:

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

I think that it would be clearer to write

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

and these types will also allow further subtyping.

I presume (for your next example to make sense) that you also intend

type Complex { self : C ->
  +(Number) -> C
}

Then 

var c : Complex := 2 + 1.i

1.i is a complex, 2 is a Rational.   The result clearly has to be a Number, not a Rational.

Even suppose that we use Michael's proposed creation method: 

const c := Complex.new(2,1)

then 2*c must clearly be Complex, so giving it a static type of Number can't work.

Note that correct arithmetic comes first.  If the type system won't permit correct arithmetic, then the type system needs to be fixed, not the other way around.  So no type system can ever make 2*(2+i) = 4.  Indeed, recall that the types can never affect the results of a computation; all that they can do is give advance warning that a given computation might go wrong.

	Andrew