I'm ashamed that I didn't see this years ago...
Rust picks an interesting position on whole-program compilation by defining
an intermediate solution: crates. As you all know, this got me thinking
about coherence and lexical scoping and all that, and I wonder if I haven't
just put some pieces together in a new way. Or maybe it is the Rust people
who have put these pieces together, but I haven't seen anything in their
writing yet to suggest that they realize what they have accomplished.
The question I'm pondering is: why do we *need* coherence? Or more
precisely, why do we need *global* coherence? Rust suggests that we might
get by with a middle position (local coherence?), but why do we need
coherence at all? One answer is: we need coherence because in the absence
of lexical resolution we need to ensure that there is just one answer. But
why is that?
If two values have the same type, we tend to take it for granted that they
support the same operations. When multiple constraint implementations exist
at a type, this may not be true. We could potentially wave our hands at
that by noting that the actual method implementations are *different*
functions,
so there's no behavioral conflict, and this all reverts back to the
operator resolution problem. Which is fine, but we still need to own this
as a problem for typing.
The answer has to do with eager unification. Or depending on your point of
view, perhaps it would be better to say that it has to do with eager
constraint resolution.
When we unify two types, we are introducing an equality constraint between
them. As a matter of implementation, we then declare internally that the
types actually *are* equal, to the extent of using the same type record
pointers within the compiler. If we later discover that the two types were
associated with competing instances, we're in trouble.
We actually rely on this kind of unification very heavily. In particular,
we rely on it to let us make types more concrete as we compile. So in
particular, if we see something like
'a \ Mumble('a) => 'a -> bool
and we later determine that 'a unifies with "int", we rewrite this type as:
int \ Mumble(int) => int -> bool
we then notice that "int" is a fully concrete type and try to resolve
Mumble(int). And if we can find such a resolution, we gleefully rewrite
this type as:
int -> bool
and drop the constraint entirely. I'm going to refer to this as "*resolution
erasure*". And now I can state the problem at the heart of this mess:
*resolution
erasure** is only correct if instances are coherent*. We've made an
optimistic assumption that may get violated at the call site in the absence
of coherence, and we have failed to document that assumption.
Rule: Two types are unifiable if and only if their constraints have the
same resolutions
Corollary: Unifying two types amounts to an affirmative assertion that
the resolutions must
match, which can be viewed as a constraint, which needs to be
documented.
In the absence of coherence, we need to rewrite this type as:
Mumble(int) ~ ParticularInstanceOfMumble => int -> bool
Informally: "This is a function from int to bool, and it's the right
overload exactly if your resolution of Mumble(int) unifies with
ParticularInstanceOfMumble. If it doesn't, then your assumption about the
functions that operate on 'int' don't match the compile-time assumptions,
and we don't have a match." When there are overlapping instances, we have
moved the link time error (which is a run-time error in the presence of
dynamic libraries) to compile time. *That alone is useful progress*. In
fact, I tentatively think it's the key to the entire mess. Tentatively
because it's hard to believe that this has been staring the PL community in
the face for so long without getting noticed, so I'm wondering what PL
paper I failed to read.
Once resolutions are documented syntactically, that leads to a second
obvious thing to do: provide a syntactic mechanism to *name* the resolution
so that a desired resolution can be specified at an interface boundary.
Naming a resolution in this fashion of course means that we are directing
the compiler that it *may not* perform eager resolution. If we hand-write
the original type (yes, the syntax is horrible - not important yet) as:
'a \ Mumble('a) ~ InstanceParameterName => InstanceParameterName :
Mumble('a) -> 'a -> bool
we could interpret this to mean that we intend the user to *tell* us the
instance explicitly by means of a named parameter. And yes, this makes
instances first-class, while preserving the requirement that instances can
correctly be treated as literal values for purposes of inlining and such.
Naming an instance advises the compiler that eager resolution on this type
class should not occur. And having some syntax to say this allows us to
name and pass resolutions explicitly at module boundaries.* *Which in turn
makes the entire language link safe and modular. I'll give an example where
this matters in a follow-up email.
None of this arises in CLR generics, mainly because CLR generic resolution
proceeds outside-in and is strictly lexical in nature.
OK. So how does this relate to Rust? Or more precisely, how does this
relate to crates and/or assemblies?
The original problem in Haskell was link safety. If we assume whole-program
compilation, then we can define an overload resolution rule for overlapping
instances and we can check for colliding instances and the program compiles
or it doesn't. The problem is that (a) the whole-program compilation
assumption fundamentally doesn't work at scale, and (b) there was no middle
position.
Crates/Assemblies provide a middle position. From a developer-social
perspective, we need a way to ensure that every deliverable boundary is
also a modularity boundary. it seems reasonable to me to say that two
groups, working independently, should use crates or assemblies as their
"deliverable boundary", and that the semantics of resolution might have
something to do with that deliverable boundary. And finally, I think that
the whole-program assumption *is* reasonable at the scale of
crates/assemblies. When whole-program compilation becomes an impediment,
you re-structure the program into more manageable crates/assemblies.
And if we combine that with my mumblings above, we get to the following set
of rules, which I think are both technically and socially feasible:
1. Within a crate/assembly, there must be a unique resolution for any
automatically resolved (i.e. an un-named) type class instance. Finding that
unique instance might involve overloading rules, e.g. so that overlapping
instances can be used.
2. A crate/assembly is a modularity boundary. In consequence is has an
interface signature. Within that signature, either:
a) Resolution assumptions must be documented as constraints, or
b) Resolutions must be named and passed as parameters
So for those of you out there who are type system experts, what part of the
problem *doesn't* this solve?
Jonathan
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
