I promised a follow-up with an illustrating case where we don't want to
resolve instances eagerly.
Consider the following procedure:
fn ArrayMin(ar: 'a[bound])
let min := ar[0] in
for (i = 0; i < bound; i++)
if ar[i] < min
min := ar[i]
return min
Note that "i" is of type int, and that we apply '<' to it. That requires us
to resolve Ord(int). So far so good.
Separately, we apply '<' to ar[i], which means that we have a constraint
"'a \ Ord('a)". Fine.
Note that 'a is a type supplied by our caller, and that the caller's
resolution environment for Ord('a) may not match ours.
And so, if ArrayMin is instantiated over an array having element type
'int', we need two *possibly distinct* resolutions of Ord(int).
As long as ArrayMin doesn't appear as an exported (or imported) symbol at a
crate boundary, that's all fine. Ord(int) will resolve the same way both
times, because of the rules we have imposed on intra-crate instance
resolution.
But if ArrayMin appears at a crate boundary, then we need to do one of two
things:
1. Document the assumption that Ord(int) resolves the way we assumed, or
2. Name the resolution so that the caller can provide one.
In the second case we won't be able to inline the instance in some
implementations, but we can fall back to a VTable-like implementation.
The point is that the "int" being used for the indexing operation isn't
operationally interchangeable with the "int" element type, even though they
are both values of type "int". It's almost as if we are back-propagating a
newtype requirement.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
