HaloO,
Luke Palmer wrote:
Well, it's possible that I'm abusing the terms, since I first heard
the terms from you and inferred what they meant.
I'm honoured. Thanks. Please don't get me wrong. I appreciate the
document you wrote. I just want to help with peer reviewing it.
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):
At least the word 'predicate' doesn't appear in the current online version.
So, to clarify: Role{Foo} is the type level equivalent to the runtime or
concrete value level check ^Foo.does(::Role)? And Factory{Foo} means
something like ::Factory.makes(^Foo). Then I understand now the Bare{Word}
notation such that it states 'Bare holds for any Word'. As a side effect of
this understanding I also start to understand the auxiliary predicate
constructors taken from the usual comparison operator set like e.g.
V{X} && W{X} # conjunction
V{X} <= W{X} # ordering? subsumption? entailment? implication?
In which scopes are these predicates valid or usable? Which are the
all and existance quantifiers? Are glb and lub available? How are
these type level predicates related to the runtime junctions?
If Role{B} and A <: B, then Role{A} (for any role Role)
So, in predicate calculus that would be written
Role{B}, A <: B
----------------- [some name here (e.g. Role Implication)]
Role{A}
and
Similarly:
If Factory{A} and A <: B, then Factory{B} (for any factory Factory)
Factory{A}, A <: B
-------------------- [Factory Implication]
Factory{B}
The role could also be called structural equivalence. The factory case seems
more like a lost warranty in case of using other manufacturers stuff. As an
example think of any installed set A of Fedora packages as a subtype of a
larger set of installed packages B. Now the factory implication would mean
that if all packages in A are official Fedora packages this carries over to
the additional packages in B. But that strikes me as somewhat counter
intuitive---well, or it just shows that my example is bad ;)
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).
Here's my mental picture that I use to remember the rules which are
not easy to remember when stated formally.
covariant
+--------------------- <: ------------------+
| |
multi f2 ( Inv2 : Arg2 ) of Ret2 <: multi Ret1 f1 ( Inv1 : Arg1 )
| | | |
| +---- <: --------+ |
| |
+-------------- :> -------------------------+
contravariant
This nicely shows the contra direction for the non-invocant part of the sig.
In a certain sense Arrays have arrow type :( Int --> Item ) and Hashes have
:( Key --> Item ) where it is unclear if the Int and Key are in co- or
contra-variant position. Some thing is the case in referencial item types
with :( Ref --> Item ).
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}) {...}
}
I see. You introduce a new contraint type variable ^U which is
F-bounded by Foo, right? Or should that be called Role-bounded?
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:
Assuming s/Foo/Foo2/ as you pointed out.
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.
Ohh, you throw in one assumption or non-explicit axiom, which basically
states that ^T is immutable as long as $x persists. There is a difference
between the type identity :(^T: --> ^T) and the referential identity
method ($x) {modify $x; $x} --- not to mention value identity!
In OO the referential identity is usally assumed in the covariant param
position while it is not assumed in the contravariant param position,
that is :(^T --> ^T) versus sub ($x) {modify $x; $x}. In other words the
invocants of methods are returned implicitly in the read/write variable
they came in. Or put in yet another way, we could invent an invocant
part in the return type section of arrow types. But I guess that would
drive Perl6 way too far into the functional domain =8()
The above also describes my perception of the $. twigil notation which
are variables bound through the invocant(s). My mental picture beeing
one where a method is instanciated as a not yet invoked sub after selecting
the target code body in the dispatch process and binding the twigils of it
on the invocant(s). This models twigil variables of the $. form as a kind
of pointer into the object's state. The information how to perform this
binding travels along the lines of inheritance. For twigiled vars of the
private data form $: this knowledge is *not* forwarded in the inheritance
process. The non-twigiled forms of variables are lexically scoped without
relation to the object state.
Question: what is the current state of affairs in @Larry about the private
instance data notation? Is it still with an underscore as the first char in
the variable's name? Or are we back with $. and $: twigils?
On the same line of thought: is the has declarator also supported outside
of class declarations? As in
my $x has $.blahh;
$x.blahh = 42;
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?
If you perceived my remarks as question then my answer to your question
would be that you gave a remarkable answer! Sorry, if that doesn't come
across as funny. I'm non-native after all.
In a more serious mood, the answer is: you've explained quite a lot, thanks.
With that new information I'll re-read theory.pod. BTW, is
<http://svn.openfoundry.org/pugs/docs/notes/theory.pod> always the newest
version? It uses e.g. still ::T instead of ^T.
--
