[Grace-core] Typing of Number

James Noble kjx at ecs.vuw.ac.nz
Mon Jun 20 20:29:24 PDT 2011


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

right...  

> If you want to define only Rational + Rational, Binary64 + Binary64,
> ..., then the type probably really needs to be something like:
>  type Number<T> {
>    +(other : Number<T>) -> Number<T>
>  }
> Number isn't doing a lot there though.

type Number {
 +(other: selfType) -> selfType 
}

which your proposed earlier would do it - although of course
it's not at all clear what "selfType" means in a structural world (is it?)

> I do think that if there's a
> Rational type it should be possible to constrain yourself to remaining
> within it somehow.

right.

> I also think Number + Number ought to work other
> than in very exceptional cases, by the principle of least surprise.

that's where things get odd.

The other thing Go does is (statically) type constants to "the right (static) type".
It's not so clear how we'd do this dynamically.
One option would be to have a "ConstantExact" or "ConstantInexact" type
which is a subtype of all the various other types so that constants work
properly even through the selfType.   ARGH.

(note that this would mean the selfType was *not* an exact selfType).
But that probably opens us up to yet more horrible issues I don't understand.

Kim??

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

we can do what DRuby does: have union types in the type system
so that we have "multi-dispatch on types" if you like, but not on methods.
That would need some other syntax to write it, something like:

class Number {
 method + : ((Rational,Rational)->Rational ) ||  ((Integer,Integer)->Integer) || ((Number,Number)->Number) 

so if it gets a rational & a rational we know it returns a rational, 
int & int gets int, anything else gets a number.

But still, isn't this an implicit conversion?   Grrr. 

> With double dispatch the static return type is the type of the
> argument (or Number), without self-type annotations and using only
> covariant type parameters instead. That types, and works OK for
> builtins. I'm not sure that it works so well for user-defined classes,
> but that might be unavoidable. It doesn't let Rational + Binary64 and
> Binary64 + Rational both return Binary64, though. Or Complex +
> Rational and Rational + Complex both do the arithmetically-correct
> thing.

well it can do the Right Thing but only with yet more dispatches I think.... 

> If that is the way it goes, what's the syntax for upper type bounds?

and yes, then you still have to describe the overall type of the method

> Because Go numbers don't have a common supertype with operations, and
> all the errors are detected statically. If Number + Number isn't
> defined the Number type is pretty meaningless.

Right. 


>>> As it stands the specification says that the standard library will try
> to coerce any Number to an integral when used as an index. Will it not
> do that? If it does, what happens for Binary64?

argh. I don't know. Perhaps that's not the Right Thing to say.

> In a purely structurally-typed world I'm not sure how the numeric
> types are distinguished anyway. I can come up with methods that would
> be unique to Rationals and IEEE floating-point types, but a
> hypothetical Integer32 and Integer64 seem like they'd implement
> exactly the same interface and be type aliases.

right. 
or you start introducing fake marker methods "I am int32" or something

> I don't think there is a perfect solution here, so one of the
> imperfect ones will have to do. I don't know which; none of them
> behave quite the way I'd expect up front.

it's probably worth thinking about some examples

James



More information about the Grace-core mailing list