Here is Rust's solution to the coherence problem:
https://mail.mozilla.org/pipermail/rust-dev/2011-December/001036.html
Based on a quick read, it looks like the second solution I initially
proposed, namely the instance is a "phantom type" of sorts included in
the constructed type, and so trying to use an incompatible instance
results in an type error.
Sandro
On 16/04/2012 12:25 AM, Jonathan S. Shapiro wrote:
> It won't surprise anyone here that I've spent a good bit of background
> cycles thinking about how the instance coherence problem might be
> solved. I want to lay out my thinking as best I can. I have not had a
> chance to read the various papers that have been recommended recently.
> It would not surprise me if this approach is similar to what is being
> done in other languages.
>
> *Inlining - What is the Issue?*
> *
> *
> Let me start by clarifying an apparent confusion that I have created
> concerning inlining.
>
> In BitC, Arith('a) is a type class that defines, among other things, the
> type class method +:'a x 'a -> 'a. Where 'a turns out to be int32, we
> rely on inlining to allow the compiler to notice that this is a case of
> hardware-supported addition. This is done as follows:
>
> * The specializer renders a + b:int32 as a procedure call;
> approximately: +_int32_int32__int32(x, y).
> * The preamble has marked +:int32 x int32 -> int32 as having an
> external implementation.
> * There is a header file that supplies this implementation as a/ C
> macro/, with the effect that the primitive + operator is seen by the
> C compiler.
>
> This is obviously a C-specific implementation. The point is that the
> proper mechanism for deriving ground operators is to treat the operators
> as regular procedure calls and then inline the concrete implementations
> so as to expose the hardware operations. With this model, optimizations
> can be implemented entirely within the typed framework.
>
> The requirement to do this is mainly that we be able to do early binding
> on ground operators at ground types. The main impediment to this in
> practice is the possibility that a late coherence failure may be discovered.
>
> *JIT - What is the Issue?*
> *
> *
> There is no issue in my mind with JIT. The issue is that any JIT system
> brings in a large and complicated pile of runtime code. I would
> therefore prefer that code generation be possible in controlled AOT
> form. In particular, I'd /really/ like to see us implement the JIT
> system this way!
>
>
> *Instance Coherence*
> *
> *
> So on to the real subject of the note. The goal is to replace the
> requirement for instance coherence with a lesser requirement for
> instance selection determinism.
>
> Objectives:
>
> 1. Timing of binding should be continuous. It should be clearly
> specified what constitutes sufficient information to make a durable
> binding/selection decision for instances. By "durable", I mean
> binding/selection decisions that will remain correct as more
> information about the program becomes apparent. This means, in
> particular, that the compiler must be able to know that early
> binding/selection decisions are not hazarded by late discovery of
> incoherent instances.
> 2. As Sandro (and others) have suggested, it should be possible to
> explicitly specify cases where eager binding/selection (therefore
> instantiation) should be applied.
> 3. In particular, early binding for ground types and ground operators
> is imperative. It is clearly intolerable if we are unable to
> implement int32 addition without an indirect procedure call.
> 4. Explicitly directed instantiation is acceptable.
>
> Proposal:
>
> The main problem is to switch from an ambient instance resolution
> process to a lexical instance resolution process. Once resolution is
> specified as lexically resolved in the usual way, the overwhelming
> majority of instance coherence issues simply go away.
>
> In order for this to work, however, we must distinguish between
> /importing/, which makes the _name_ of an instance visible in the
> importing unit, and /opening/, which brings a named instance into the
> instance resolution contour. As part of this distinction, we will
> require that all instance definitions be named, mainly so that they can
> be opened by name.
>
> An instance for a type class TC('a, 'b, ... 'z) is resolved in the
> resolution contour in which all of the type variables 'a ... 'z become
> concrete.
>
> It is permitted to have overlapping, open instances in a single
> resolution contour. It is /not/ permitted to have two precisely matching
> instances in a single resolution contour. Ambiguous instance matches are
> resolved by adopting the /latest/ open instance in the resolution
> contour. Thus:
>
> instance TC('a, 'b) { ... } // fine
> instance TC('a, int) {...} // okay - /partially/ shadows previous
> instance TC(char, char) {...} // okay - /partially shadows /previous
> instance TC(char, char) {...} // error - /fully/ shadows previous
> instance TC(int, 'a) {...} // okay - ambiguous at TC(int, int), but
> preferred as the later resolution
>
> Note that because of the opening process, an instance declared in a
> distant module cannot impact the behavior of my module without my
> consent. The notable exception to this is instances declared and opened
> in the preamble, because all preamble imports are performed as opening
> imports.
>
> Can anybody state a place where this approach fails to deal with
> instance coherence?
>
>
> Jonathan
>
>
> _______________________________________________
> bitc-dev mailing list
> [email protected]
> http://www.coyotos.org/mailman/listinfo/bitc-dev
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
