On 11/3/05, TSa <[EMAIL PROTECTED]> wrote:
> So if A <: B, I would expect Role{B} <: Role{A} and Factory{A} <: Factory{B}
> on the following rational.
Well, it's possible that I'm abusing the terms, since I first heard
the terms from you and inferred what they meant.
However, there is a problem in your statement:
A <: B implies Role{B} <: Role{A}
Since Role{B} is not a type: it is a predicate. The way I put it (and
I think it is put this way in the document):
If Role{B} and A <: B, then Role{A} (for any role Role)
Similarly:
If Factory{A} and A <: B, then Factory{B} (for any factory Factory)
> Thinking of A beeing a proper subset of B we
> get the reverse relation for their complements because parts of the outside
> of A are inside of B. Functions in roles have type (R --> None(R)) and
> functions in factories have type (None(F) --> F) with R and F the implicit
> topic types of the role and factory respectively. Normal arrow subtyping
> rules then result in roles beeing *contravariant*, unary theories and
> factories beeing *covariant*, unary theories.
Hmm, okay. Then I probably reversed them (I need to read more about
arrow subtyping).
> OTOH, theory.pod talks about the topic type appearing in the invocant
> position of methods of roles, which subtypes covariantly. Note also that
> the return type is covariant. So I neither understand the part about roles
> having methods that return the type the role defines.
Let's see if I understand what you're asking. You're asking about:
role Foo {
method bar(--> Foo) {...}
}
Expanding this to a theory:
theory Foo{^T} {
method bar(^T: --> ^U <= Foo{^U}) {...}
}
This is different from:
theory Foo2{^T} {
method bar2(^T: --> ^T) {...}
}
We can see the difference when we have, say:
class Bar does Foo does Foo2 {...}
class Baz does Foo does Foo2 {...}
my $bar = Bar.new;
$bar.bar; # may return a Bar or a Baz
$bar.bar2; # may only return a Bar
If Foo2 were a role (that is, if it obeys the role relation above),
then the only thing bar2() could do would be to take some side-effect
action and then return the same object it was passed. Here's a proof:
Given ^T $x where Foo{^T}. Because of the role relation,
Foo{{$x}} (The singleton set {$x} does Foo). Therefore
the signature of bar in this instance is
:({$x} --> {$x}). Since $x was unrestricted, bar()
must be the identity on things that do Foo.
But of course, that's probably not what the author of the Foo role
intended. So we allow any Foo to be returned.
Did I answer your question?
Luke
