The current BitC specification requires that type class instances be
globally non-overlapping. This is not scalable. As programs grow, it is
inevitable that collisions will occur. As we introduce dynamic linking
and dynamic instantiation, it is inevitable that working programs will,
under this rule, at some point cease to function because a library
introduces a colliding type class. This is not okay.
There is a further problem that we sometimes want to provide
specializations of type classes for certain types. The current scheme
provides no good way to deal with that either.
There are no good answers in principle to these problems. There are only
debuggable answers and manageable answers.
We propose to address both problems by resolving type class instances
lexically. The methods of a type class are determined in the lexical
context in which the type class is instantiated. When a type class is
instantiated, the lexically nearest (i.e. the latest appearing) instance
that unifies with the instantiating type relation will be used. [This
means that general instantiations should appear before more concrete
instantiations, and it avoids the classic C++ ambiguous overload
issues.]
So we now need to state where each type class is instantiated.
Definition: Given a function whose signature is:
(forall ((TC1 'a) (TC2 'b) (TC3 'a 'b))
(fn ('a) bool))
we say that a type class constraint is "public" if all of the type
variables occurring in that constraint are fully determined by the
parameter and return types of the function. This intentionally includes
any type variable that is resolved as a consequence of a type function.
We say that a type class is "private" if at least one of the constituent
type variables of its type relation is NOT fully determined when the
argument and return types of the function are known. In the example
above, TC1 is public and TC2, TC3 are private.
Policy: The instantiation of a private type class over a definition D is
determined in the lexical context of D. The instantiation of a public
type class occurs in the lexical context of D's caller. So given:
(deftypeclass (Arith 'a) ...)
(define (add-one x) (+ x 1)))
: (forall ((Arith 'a)) (fn ('a) 'a))
(define (add-one-int32 x:int32)
(add-one x))
: (fn (int32) int32)
the instance of (Arith int32) that will be used in add-one depends on
where it is called from, because Arith is a public type class
constraint. In the example above, it is resolved in the lexical context
of ADD-ONE-INT32.
Given:
(deftypeclass (Arith 'a) ...)
(define add-internally
(let ((counter 0:int32))
(lambda (x)
(set! counter (+ counter 1)))))
: (fn ('a) 'a)
the instance of (Arith int32) used to perform the addition on x is
private, and is therefore resolved in the lexical context of
ADD-INTERNALLY.
The messy case is when we see something like:
(deftypeclass (Arith 'a) ...)
(define add-one-with-counter
(let ((counter 0:int32))
(lambda (x)
(set! counter (+ counter 1))
(+ x 1))))
: (forall ((Arith 'a)) (fn ('a) 'a))
This one is both awkward and confusing. The problem here can be seen by
considering two seemingly similar expressions:
(add-one-with-counter 1:int32)
(add-one-with-counter 1.0:float)
In the first expression both additions will be performed by an
instantiation of (Arith int32), but the types of x and counter are
independently selected. There are three sensible choices, none of which
are obviously right:
1. Because a public resolution of (Arith int32) exists, it is used
wherever an instance of (Arith int32) is required -- even the
private instance.
2. Because a *private* resolution of (Arith int32) exists, it is
used wherever an instance of (Arith int32) is required.
3. Because the types of x and counter are selected independently,
the two addition operations induce independent constraints. One
is public and the other is private, and the consequence is that
they use independent resolutions. The public one is resolved in the
caller context and the private one is resolved in the callee
context.
Choice [3] makes more sense when you look at the second expression,
where it is clear that the two additions must involve independent
instances (Arith int32) and (Arith float), and it is also clear that one
is public and the other is private.
I am very torn here. I dislike the possibility that two different
implementations of addition over int32 might end up used in this type of
situation, but I also think that consistency of instantiation is
important. Fortunately, I suspect that (a) the situation is rare, and
(b) when it happens, it is likely to happen over ground types.
>From an implementation standpoint, we do not know at the time we compile
add-one-with-counter how the argument types will be instantiated. This
means that we need to check for the lexical visibility of the private
(Arith int32) in both cases, even if we later end up using the public
instance. Once we have to check, I think that we should go ahead and
resolve those references eagerly. That is: I think we should follow the
goal of consistency here, and stick to the rule that public constraints
are resolved by the caller while private constraints are resolved by the
callee.
So that is what we propose to do. Reactions and critiques are very
welcome.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
