I've had a side conversation going with Ben Kloosterman. One result was
that I re-read the original
paper<http://scg.unibe.ch/archive/papers/Scha03aTraits.pdf>on traits.
The traits idea worked its way into the PL community after I
left to work on microkernels. Several people have since tried to explain
them to me unsuccessfully. It is interesting how the simplest ideas are the
hardest to describe, and can sometimes be the hardest to acquire as a
result. Makes me wonder if my brain is ossifying.
Here's the original definition of traits with some addenda from me in
square braces. Traits have the following properties:
1. A trait *provides* a set of methods that implement behavior.
2. A trait *requires* a set of methods that [are imagined to] serve as
parameters for the provided behavior. [The "serve as parameters" reflects
envisioned use. The essential property is that traits specify a set of
required methods.]
3. Traits do not specify any state variables, and the methods provided
by traits never access state variables directly. [Though traits can be
obviously extended with properties.]
4. Classes and traits can be composed from other traits, but the
composition order is irrelevant. Conflicting methods must be *explicitly*
resolved.
The original definition had two more properties concerning composition, but
these seem to be consequences of the properties above rather than defining
properties of traits.
Observe: We can imagine degenerate traits in which either the *provided* or
the *required* methods are empty. Traits therefore subsume interfaces.
Observe: The "required methods" of a trait could *almost* be expressed as
"required traits". The caveat is that this induces a lattice ordering
constraint on trait definitions. At first glance this appears to violate
the freedom of composition ordering expressed in the 4th property, but that
can be recovered by rewriting.
Observe: Traits can be parametric, and I'm going to assume this below.
Observe: Traits are types. It makes perfectly good sense to write "x as
SomeTrait" and get a reference of type SomeTrait.
Observe: Traits can be unioned. In particular, we can interpret "trait
traitA = traitB + traitC" as a means of specifying construction of an
interface method table.
*Review: HAS-FIELD*
I'm going to switch gears for a minute for a mildly ironic side note about
language design at my own expense. As a designer, you spend enormous
amounts of time on something that you think is important. In BitC's case,
that was mutability inference and parametricity over mutation. Along the
way you throw in some number of minor brain farts that seem trivial at the
time (and mostly are). One of them will turn out to be the thing your
language is known for. Given my luck in naming things (EROS, Coyotos,
BitC#), I am terrified this will come to be known as "Shapiro's Law of
Brain Farts".
Be that as it may, I'm starting to think that the interesting brain fart in
BitC is going to turn out to be HAS-FIELD.
HAS-FIELD got thrown in as an attempt to account (in the type system) for
the capsule method invocation rewrite. I wasn't ready to bite off the
subtyping problem that goes with inheritance yet, but I needed a way to do
existential types. That in turn seemed to need a way to say that the
rewrite:
x.methodName(y) => X:: methodName(x, y)
is legal exactly if:
x : X, y:Y and
has-field(X, methodName, (X, Y) .-> ())
where the notation ".->" distinguishes an object method from a function.
Originally it was called has-method, but at some point I noticed that it
also accounted for the genericity of "def f x = { x.y }". At that point I
renamed it and introduced ".->". It seemed to me at the time that this kind
of genericity kind of wanted a story in the type system, and might turn out
to account for a lot of forms of non-hierarchical reuse.
*Traits Can [Almost] Be Modeled By Type Classes*
Given has-field, we can express the trait:
trait SampleTrait 'X 'Y 'Z {
requires f : 'X .-> 'Y
provides g : 'Y .-> 'Z
}
as a type class;
has-field('this, f, 'X .-> 'Y) =>
typeclass SampleTrait 'this 'X 'Y 'Z {
'this.g : 'Y .-> 'Z
}
where the syntax "type.id" has the intended meaning that "id" is a member
of "type" - though in the presence of Koenig-style overload resolution I'm
not sure what "member" means anymore. In the type class world we would
probably have written this as:
typeclass SampleTraitRequirements 'this 'X 'Y {
'this.f : 'X .-> 'Y
}
SampleTraitRequirements 'this 'X 'Y =>
typeclass SampleTrait 'thix 'X 'Y 'Z {
'this.g : 'Y .-> 'Z
}
So given a notion of method type (as opposed to function type) and the
ability to express a has-field constraint, it turns out that type classes
subsume traits *up to* inheritance. Actually, type classes are strictly
more powerful than traits, because they are type relations. This means that
they can express *provides* and *requires* constraints across multiple
types simultaneously. Not sure if that's useful, but from a language design
perspective it's nice when one thing eliminates the need for another. In a
language with type classes and object methods, traits are just syntactic
sugar.
The missing piece here is that type classes are not types. Which raises the
question: well, why are Traits types then? The answer is that Traits
tacitly assume a 'this type, and the trait itself is effectively an
existential wrapper of that. But Bruno Oliveira's work suggests that type
classes can be viewed as types. And if nothing else we can certainly
recognize those type classes that are equivalent to traits.
BitC in its current *implementation* assumes that object methods are bound
at compile time, but that's certainly not a requirement of the type system
or the language semantics. Which means that having ".->" in the type system
gets us very close to typing single inheritance. The missing piece is
subtyping. Which is a whole can of worms, but it seems good to take notice
of it. Given only Capsules (object methods without inheritance), we still
have something very powerful here.
I'm sure the folks who tried to reconcile interfaces and type classes in
Java got further down this path than I have yet; I haven't caught up with
that paper quite yet.
*Type System Implications*
This seems good. I'm now convinced that we can build a sensible type system
out of all of this. We clearly can't do sound and complete inference in F<.
But for the first time I'm ready to think we might be able to craft a type
system that *describes* both single inheritance and type classes in a
single framework. Which means that my concern about interoperability with
existing OO language might have a solution.
That's not to say that I *want* single inheritance. We need existential
types, but capsules provide that, and they might be good enough. What makes
me very happy here is beginning to see a type system that *might* be able
to express the constraints of interoperability.
*Traits, Type Classes, and Inheritance*
If traits can be modeled by type classes, then where does inheritance come
into this? Especially in the presence of Koenig-style member resolution,
which allows us to add functionality to classes after the fact. On the face
of it, there is no marginal expressiveness provided by inheritance unless
it is somehow a consequence of subtyping.
In the presence of the HAS-FIELD constraint, subtyping as a constraint on
*parameters* seems to be subsumed. What's left is subtyping at assignments
(partially evading monomorphism). But Trait types subsume that as well. So
what's the real difference between inheritance and traits? I'm beginning to
think that it comes down to one semantic issue and one implementation issue.
The semantic issue: treating a subtype as a supertype involves an implicit
cast. From an inference perspective, there is a huge difference between:
'Sub :< 'Sup, sup : 'Sup, sub : 'Sub => sub := sup (subtype
assignment)
'T implements 'Trait, t: 'T, trait : 'Trait => trait := t as 'Trait
(trait object construction)
The first breaks inference. The second doesn't.
The implementation issue is that trait reference creation is object
construction, and therefore involves storage allocation. Upcast, by
contrast, involves no allocation. At first glance that seems innocuous, but
it has a bunch of unpleasant implications if we want to be able to write
non-allocating programs.
I suppose we could argue that the ability to perform (checked) downcasts
isn't provided by trait types. I'm of the school that thinks downcasts are
a rights amplifying operation to be avoided, so I guess I see that as an
improvement. It does present a missing piece from the standpoint of type
system reconciliation.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
