--- On Fri, 3/6/09, Jonathan S. Shapiro <[email protected]> wrote: > Problem: These two instance resolutions occur in different contexts, > and it is entirely possible that we will end up with two DISTINCT > instance resolutions.
Why is this a problem? When we were writing function g, the types 'a and char never unified precisely because we had no need for them to be the same. That 'a might ultimately end up being char doesn't matter - the correctness of g doesn't depend on the instances being coherent. Now, occasionally it might be nice to expose the instance chosen as a named parameter to g, but that's another issue. PS. What exactly causes replies to get posted in the right spot on the summary? From: Jonathan S. Shapiro <[email protected]> Subject: Re: [bitc-dev] Moose, rugs, and separate compilation To: "Discussions about the BitC language" <[email protected]> Date: Friday, March 6, 2009, 9:49 PM On Fri, Mar 6, 2009 at 3:56 PM, Gelf Mrogen <[email protected]> wrote: > I'm not sure I understand your optimization concern. If you write code > that's abstract, by making it depend on a number of type classes, then it > will tend to be hard to optimize it in a separate-compilation setting. But > if in compiling g you already have concrete types in mind, then the instance > used for them should be decided lexically in g and will not be overriden by > context later, right? Not always. In particular, not if those instances are resolved at g's caller. > Maybe you can provide an example of what you're > worried about here? Here is a contrived example. Consider a module B that has the following procedure: (define (contrived a a-bound b b-bound) (cond ((>= a a-bound) #f) ((>= b b-bound) #f) (otherwise #t))) contrived: (forall ((Ord 'a) (Ord 'b)) (fn 'a 'a 'b 'b -> bool)) >From this module we export a function g(): (define (g a a-bound) (contrived a a-bound #\c #\d)) g: (forall ((Ord 'a)) (fn 'a 'a -> bool)) Since the 'b from contrived does not escape into the signature of this procedure, The lexical context of g() will provide the instance of (Ord char) that is used to resolve the (Ord 'b) constraint in contrived(). The 'a from contrived remains part of the procedure signature, so it is not yet concretized and its constraints are not resolved here. And now in some module A we import g() and call it: (define (f) (g #\e #\f)) This resolves the (Ord 'a) constraint on f() to (Ord char), which (because the type variables are unified) will propagate to resolve the (Ord 'a) constraint for the instantiation of contrived that will eventually be called. Problem: These two instance resolutions occur in different contexts, and it is entirely possible that we will end up with two DISTINCT instance resolutions. That is: the two applications of "<" are invoking completely unrelated procedures, even though they are identically typed in the final, specialized procedure. It is tempting to imagine that we could adopt a different policy in which the resolution of 'a gets added to an environment of some sort, and when the instantiator goes to deal with the expansion of g() it consults this caller-provided environment before consulting the local one. In this example, the effect would be that we invoke the same version of "<" in both applications that appear in contrived(). Unfortunately, this does not generalize. Suppose we revise contrived() to read: (define (contrived a a-bound b b-bound) (cond ((== a a-bound) #f) ((>= b b-bound) #f) (otherwise #t))) contrived: (forall ((Eq 'a) (Ord 'b)) (fn 'a 'a 'b 'b -> bool)) So now the (Eq char) will get resolved in the lexical context of f() and the (Ord char) will get resolved in the context of g(). Assume that the resolution selected for (Eq char) is added to the instantiation environment that is in effect when g() is instantiated. (Ord char) isn't in that environment, so we need to resolve it in the environment of g(). But oh crud, (Ord char) is a subclass of (Eq char). It seems to me very dicey that in this situation we would end up resolving Ord in one environment while having its dependency get resolved from a completely unrelated environment. Does this example make the nature of the mess clearer? shap _______________________________________________ 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
