This is an idea that I never got around to implementing, but I sort of
think is important. It's also pretty half-baked.
I came to it from a simple question: How do we know when two instances of
something like List('a) are free to use the same underlying implementation?
The answer seems obvious enough: the same implementation can be used for
List('a) and List('b) when the types 'a and 'b have the same size. This is
true because lists handle their element types in a very opaque way. What we
would like is a way to describe this semi-opaqueness.
To view this another way, the type of a "CopyWord" operation in a VM can
*almost* be described as:
HasSizeAndAlign('t, 4, 4) =>
CopyWord(ref mutable 't, ref 't)
Except that we have dropped something here. CopyWord must ensure type *
agreement*, but it doesn't care what the type actually *is* from an
operator point of view. Any type, so long as it is a four byte type at a
four byte alignment, can use the same *implementation* of CopyWord. We do
not mean here:
for ALL instantiations of 't meeting the constraints, this parameterized
function has an instantiation of 't that is the right one to use.
We mean, instead:
for EVERY instantiation of 't meeting the constraints, this function IS the
instantiation to use, REGARDLESS of the concrete instantiation of 't
In effect, I'm trying to capture what is happening at the erasure boundary,
where we drop down to untyped machine instructions. The distinction between
FORALL('a) and EVERY('a) is that we don't need to instantiate over 'a if we
already have an instantiation where the other constraints have been
satisfied.
This isn't existential type, because we need to know what the type is in
order to discharge the constraints.
So in this (notional) view, the typing of List('a) becomes something like:
union List('a) {
cons: { car: 'a; cdr: List('a) }
nil
}
every('a), HasSizeAndAlign('a, 'size::nat, 'align::nat) => List('a)
The intuition here is that instantiation is going to be driven by the
[implicit] forall on 'size and 'align, rather than being driven by the 'a.
In consequence, if you discover an instance with matching concrete types
for the 'size and 'align (note the clever/tricky use of the Nat kind here),
you are free to use that one.
Please do not take me to school yet on the notation. I freely concede that
it stinks. As usual, the *absence* of an every('a) marker means that the
type variable is universally quantified.
Now the interesting part of this (maybe) is the subsumption rules. In
particular: forall('a) subsumes every('a). So when we unify the constraints
in something like
def list_sum(l) : Word
let list_sum_help(accumulator, l)
switch( cell = list ) {
nil: { accumulator }
else { list_sum_help(cell.cdr, 1 + accumulator) }
in
list_sum_help(0, l)
we would initially get:
every('a), all('a),
HasSizeAndAlign('a, 'size::nat, 'align::nat), Arith('a) => list_sum: 'a ->
Word
but:
- all('a) implies a requirement for concrete instantiation, therefore
subsumes every('a)
- concrete('a) implies known size and alignment, subsuming
HasSizeAndAlign('a, 'size::nat, 'align::nat)
and that leaves us back with the expected type:
Arith('a) => list_sum: 'a -> Word
This intuition, I believe, has straightforward extension to type
preservation when emitting untyped machine code, and also (in a different
way) to typing in the fragile base class problem.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
