[Grace-core] Typing of Number

[James Noble]

>>>>> 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.
> 
> This is surely up to the object being indexed.  For some objects, with continuous behavior, having non-integral indexes makes perfect sense.  For others, it does not.   

yes that's fair enough.
Still there is the question: for things like arrays or collections, that do want 
integral (actually a Natural, positive nonzero integer) index: 
should the language require explicit conversions when 
 - a non-integral type is passed in (float, double, complex etc)
 - when an integral but non Natural type is passed (byte, etc etc)

> Do you mean "distinguished from each other" or "distinguished from non-numeric types"?

both I think: primarily distinguished from each other but this implies distinguished from non-numeric types.

> Binary64 and Binary128 have the same behavior as types.  And maybe that's exactly right: you want to be able to replace the Binary64 constructor methods by Binary128 constructors, and have the program continue to be type-correct, but with a more exact result. 

that only requies Binary128 is a subtype of Binary64. 

> There is of course an efficiency argument for prohibiting re-implementation of integer: if you can tell from the type that a value has the particular built-in machine integer representation, you can emit machine instructions rather than method requests.  But it precludes the nice automatic conversion to BigNums that are so convenient.  Didn't we have some principles that covered this.

(looks it up)
we've got:
 * The execution of the language should not depend on a program’s static types.
 * Efficiency is not a concern of this language design.
 * The language should support a simple performance model for simple programs. 

pragmatically we at least need to be able to link to C or Java libraries.

I think that it would be good e.g. to be able to say (and check statically) 
that some computation is really in bytes, or machine integers (modulo 2^32 arithmetic :-), or floats
and lives only within those types.    And I can see that - for those really restricted things -
there should be no implicit conversions to types like Number or Rational. I think.
This doesn't mean that literals can't be "contextual";
nor does it mean that such types can't be a *subtype* of Number or Numeric or something, without _conversions_

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

> This sounds reasonable.  It also sounds reasonable to allow operations like addition of a complex number to a rational and taking the square-root of a rational, both of which will of course take you our of the rationals.
> 
> Is there a proposal for reconciling these two apparently reasonable, but conflicting, desires?


I don't know.
Even adding a complex to a rational is tricky: however it is implemented
it means + on rational must accept either a rational OR a complex
with different return types depending on the argument types...

I  fear we need to think about more actual examples. 
Here's a nasty one:

say we have something like this:

a : unsignedByte  
b : unsignedByte
 
a := 255
b := 1 

print a + b    //  what should be printed?  Go I think would print 0? unsignedByte is basically arithmetic mod 256

//-------------

a : Number  
b : Number 
a := 255
b := 1 

print a + b // had better print 256!! 

// ------------- 

OK so that goes to show things aren't that simple - in particular Go's rules
about typing constants via static type contexts can't really work for Grace.
I should have spotted that earlier.

the question then is: what would we have to add to the unsignedByte example to make it all work,
and how horrible is that?

1.ub and 255.ub  (to force conversion to a byte?)

at least that keeps everything explicit.  
then (1.ub + 255.ub) = 0.ub
while (1 + 255) = 256

***hopefully*** people wouldn't feel the need to start teaching about .b until rather late!

> Another place to look for inspiration is the numeric types in Fortress.  A lot of smart mathematically-inclined people thought very hard about those.  But Fortress uses types to define semantics.

right. perhaps we have to look there too.

> Any of these variations can work.  I kind of like the last one, but the LOOJ-style system may be less jarring for people if we decide to have a SelfType.

OK yep, so one question is - does SelfType make sense if it is *not* exact? 

James