[Grace-core] Typing of Number

[James Noble]

ahh, our emails seem to have cross in the aether

> Actually, that isn't right - it just requires some bigger changes to
> the type system than I'd been contemplating.

well I don't think we have an agreed type system yet!
even the syntax is still in flux

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

not sure Rational->Binary64, because Rational is exact an unlimited and Binary64 isn't.

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

Hmm, I don't know anything that does that -
(because you've got an implicit existential I think in there:
-> \E U : U = LUB(T,S) 

and I recall something about Fortress allowing that.
The Fortress spec is in the svn...

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

I don't know. I'd hope we don't need to go there, so that (at least early on)
people can explain things (even if it means they are in a setting where
they don't have the full generality of the whole library - a "language level")

I wonder what other languages do - what the "best practice" is.

O'CAML (or one of the camels, anyway)  had different operators for floating
point -  #+ vs + :-)

the again, I still like Smalltalk's like that the primary design of the langauge
was *NOT* to replicate fortran

James