In Haskell, we have two rules:
1. All instances are defined at global scope.
2. Instances may not collide.
These are very convenient. Taken in combination they mean that there is
only one scope in which instances are resolved. This is pleasant, because
it means we don't have to answer an awkward question. The question is: "in
what scope is an instance resolved?" The three candidate answers are:
1. In the scope where the constraint is first introduced [lexical
constraint resolution]
2. In the scope where the operator appears [lexical operator resolution]
3. In the scope of the type variable.
Consider the following procedure:
def WriteObject outStream i =
let OMarshall int = OrphanedInstance in
outStream << i
outStream
If "<<" is resolved in the scope of the type variable, then the local
binding of OMarshall int has no effect on the resolution of "<<", and the
type of the procedure is:
WriteObject: OMarshal 'a => OStream -> 'a -> OStream
If "<<" is resolved lexically (either way), then the procedure has two
different types depending on the resolution of 'a:
WriteObject: OMarshall 'a => OStream -> 'a -> OStream
WriteObject: OMarshall(int) = OrphanedInstance => OStream -> int -> OStream
And isn't that a kick in the head? So how did this happen?
First, in general, if we have:
'a \ Constraint('a) and 'b \ Constraint('b) and 'a ~ 'b
Then we want:
'a \ Constraint('a) ~ 'b \ Constraint('b)
and if we have
'a \ Constraint('a) and T \ Constraint(T) = OrphanedInstance and 'a ~ T
Then we want:
'a \ Constraint('a) ~ T \ Constraint(T) = OrphanedInstance
and if we perform this unification, we need to document it in the procedure
scope, *because* the instance is orphaned.
Now one way to handle this is to declare that automatic instance bindings,
like type variable bindings, are scoped to the procedure, and the let
syntax is just a convenience sugar. Personally I find that syntactically
confusing, but never mind. It's also counter-intuitive. Why should the
automatic binding float to the top when an explicit binding clearly should
not:
def WriteObjectAlt outStream i =
let m = OrphanedInstance : OMarshall int in
outStream m.<< i
outStream
should the intent of these two bindings (one explicitly named, the other
explicitly extending the resolution environment) be different? As someone
(William or Ben, I think) asked: should we be introducing knowledge of
behavior into the type at all?
Let me say outright that I'm not sure the first example is a good syntax
for extending the resolution environment, and I'm not sure that extending
the automatic resolution environment locally is a good idea at all. That
said, it's not a red herring, because I snuck something past you up above.
When a procedure is exported from an assembly, it's type variables
propagate to the scope of the assembly interface, not just to the procedure
scope. So we get a scope structure that looks like:
Symbols and types exported from assembly
Non-exported symbols at assembly global scope
locally let-bound symbols
And since it's possible to bind an orphaned instance without exporting it,
this has some of the feel of an extension of the automatic instance
environment. But if the orphaned instance escapes into the module-layer
type environment, that's a bit of a mess. My point, though, is that
removing the syntax for extending the automatic instance environment
doesn't take it out of the language semantics.
Meanwhile, it isn't so pretty to declare that instances bind at the scope
of the type variable. Consider:
def ConflictedEnvironments outStream i =
let ans = i #postfixop# in
let OMarshall typeof(i) = OrphanedInstance in
outStream << i
outStream << someNonExportedGlobal
ans
In this case, if someGlobal just so happens to be the same concrete type as
i, but the two don't unify, the resolution environments for "<<" are
different in the two uses. How lovely!
Of course, if we *really* think that lexical resolution is the right thing,
then the local environment extension in WriteObject is just that: a
*local* extension.
We intentionally did a local override on the binding environment. Maybe the
result of that override shouldn't propagate outside the binding at all. But
if *that* is the case, then should:
def HopelesslyConflictedEnvironments outStream i =
outStream << i
let OMarshall typeof(i) = OrphanedInstance in
outStream << i
outStream
get two distinct resolutions of "<<" because they occur in different
lexical contours? Personally I think that's a *really* bad idea, because it
leads to an outcome where Constraint 'a can have *multiple* resolutions
that need to be documented at the procedure interface.
Sigh. Aren't type systems fun!
Jonathan
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
