HaloO,
Larry Wall wrote:
.WHAT gives you an value
of undef that happens to be typed the same as the object in $x,
presuming your metaobject believes in types.
Why does the metaobject have to believe in types? I think it
suffices to define that .WHAT returns a unique binding in the
scope of interest. This binding can naturally be checked with
=:= e.g. as in 3.WHAT =:= 4.WHAT =:= Int. Interesting is
that you need parens for negative numbers (-2).WHAT =:= Int.
Well, you can write that as WHAT -3 =:= Int.
.HOW gives you the
metaobject that manages everything else for this object. It might
or might not believe in classes or types.
Fair enough. I infer that the HOW deals with non-MMD dispatch only.
That is, MMD is purely WHAT based. Now consider
subset Even of Int where {$_ % 2 == 0}
multi foo (Int $x) { "Int" }
multi foo (Even $x) { "Even }
MMD collects the applicable targets first. That results in foo(3)
returning "Int" as expected. But foo(2) throws an exception because
the Even constraint allowed the second target into the set of
candidates. This is because 2.WHAT =:= Int is an exact match in both
cases. Now how do we use the constraints as tie breakers? That amounts
to comparing {$_ % 2 == 0} to {$_ .does: Int}. That might be possible
here because 2.WHAT.of =:= Int and the presence of a subset declaration
documents the programmer's intent nominally.
But when the subset is instead written
subset Even of Num where {$_ % 2 == 0}
then foo(2) says "Int" because 2.WHAT =:= Int is more specific than
Num *before* any subset declarations are used for tie breaking. Do we
want this behavior?
Now I assume the infix:<as> takes the WHAT of its rhs and stores
it in the WHAT of the lhs if the value of the lhs meets the constraint
of the rhs.WHAT. Whether that constitutes a mutation or not, is
debatable. This makes foo(2 as Num) return "Even" as expected.
Now I bring a container into my contemplation.
my Num $two = 2;
It is conjectured that this Num constraint on the container
behind the name $x somehow acts as the infix:<as> before. That
is foo($two) returns "Even". This implies that a container
*erases* type information in its FETCH method. Note that this
does not change the HOW dispatch on the value in $two. So e.g.
$two.add(2) dispatches e.g. to Int::add(Int ::T $other --> T).
BTW, this also implies that the ::T syntax captures the WHAT
of the arguments bound to $other so that it can be stuffed
into the WHAT of the return value. The compiler might actually
do that automatically. That is the genericity John Dluglosz is
talking about. Note that this WHAT assignment can fail!
sub foo (Int ::T $x is rw --> T) { $x++; }
$two = 2 as Even; # assignment OK, Even .does: Num
my $y = foo($two); # 3 as Even fails!
Even though the assignment $y = 3 would work, foo fails
to adhere to its own constraint! Typing is tricky business.
Note that $two == 3 as expected. The actual implementation
of ++ dispatches to 2.HOW, of course. That instanciates
the 3 with 3.WHAT =:= Int as usual. A corollary here is
that '2 as Even === 2' is false. Or does === check the HOWs?
The thing that is bothering me is to define a partial order
on the WHATs, i.e. a binary, reflexive, transitive and
anti-symmetric relation <: and perhaps its companion :>
that is not !<: because that drops the =:= case. In the spec
this goes as "type narrowness" or "topological order".
Since the typing shall be nominal I propose the syntax
subset Even <: Int where {$_ % 2 == 0}
to mean that containers carrying that type as their constraint
*automatically* re-assign the WHAT to Even whenever a matching Int
comes in. The rhs of <: is a pre-constraint in this case. The dispatcher
does the same when an Int versus Int tie occurs as above and
re-dispatches with this new type. An 'of' subset would not have
this automatic re-typing behavior.
The type checker might or might not be able to proof the validity
of <: in general but an implementation can restrict the sub-language
applicable in a where block to make the type system decidable.
For so-called mutable types this re-typing can become more involved.
That is there is a 1:1:n relation between the HOW and WHICH on the one
hand and the WHATs on the other. This sort of means that the WHAT
becomes a junction.
class C does A does B {...} # enters C into WHAT space
my $y = C.new; # $y.WHAT =:= C
my $b <: B; # automatically re-typing container
my $a <: A; # means e.g. my A $a is autotype
$b = $y; # now $y.WHAT =:= B
$a = $y; # now $y.WHAT =:= (A&B)
This last assignment has to enter the meet type (A&B) into the
type lattice because simply re-typing a B to an A is not possible
unless A <: B holds. This needs to be declared explicitly somewhere.
The declaration of class C doesn't do that, of course. So programs
not using <: don't incur the type calculation overhead.
If we repeat the above sequence with a class D and a variable $x
respectively, the value of $x ends up in the identical WHAT (A&B)
instance set. But the HOW of the instances of this WHAT becomes
inhomogeneous in the way how the combined roles A and B are done.
Note that this WHAT based MMD doesn't do anything with the objects.
This can be done only through the HOW dispatch. Another effect is
that (A|B) is never entered into WHAT space automatically. There
must be extra syntax to implement a join type that contains instances
outside of (A&B). My idea is to write
class C does A|B {...}
my B $b = C.new; # type error
my A $a = C.new; # type error
Correspondingly 'does A&B' would behave so that fresh instances
of C get WHAT (A&B) right from the start not lazily by constraint
checking of containers and dispatchers the value passes through.
This type calculus also can be applied when containers are bound
together.
class Cab does A does B {...}
class Ca does A {...}
my $x = C.new; # $x.WHAT =:= C
my $b <: B;
my $a <: A;
$a = $x; # OK, $x.WHAT =:= A
$b := $a; # OK, $x.WHAT =:= A&B
$a = Ca.new; # type error, constraint is now A&B
This constraint merging upon binding should be done for all containers,
BTW.
You can do type reasoning with the WHAT type just as you can with
a real value of the same type. Int is a prototypical integer from
the standpoint of the type system, without actually having to *be*
any particular integer.
Isn't it then more practical to make
my Int $x; # no initialization
mean
my Int $x = one(Int);
and do the reasoning junctively?
In contrast, the .HOW object for Int is very much *not* an Int.
Perl doesn't know or care what the type of the .HOW object is, as
long as it behaves like a metaclass in a duck-typed sort of way.
It's probably a mistake to try to use the type of the .HOW object in
any kind of type-inferential way.
I agree. But note that HOW and WHAT compete for the same slots
in the namespace which lets me think that we might need the
pseudo-namespaces HOW and WHAT besides things like OUR, MY,
OUTER, CALLER or GLOBAL.
: That is, how can the
: program look at $x and ask for the constraints that are placed on it?
Placed by the variable, or by the type of the contents? The
constraints on the value are solely the concern of whatever kind of
object it is. If you mean the constraints of the container, then
VAR($x).WHAT will be, say, Scalar of Int where 0..*,
You mean a non-negative Int, right?
and VAR($x).of
probably can tell you that it wants something that conforms to Int.
I'm not sure if the "of" type should include any constraints, or just
return the base type. Probably a .where method would return extra
constraints, if any.
Note that constraints are special closures that always return either
True or False, never throw exceptions and have no side effects. To
use them for type checking is easy. You just call them with a value.
But how do you compare them other than exhaustively sampling them?
Regards, TSa.
--
"The unavoidable price of reliability is simplicity" -- C.A.R. Hoare
"Simplicity does not precede complexity, but follows it." -- A.J. Perlis
1 + 2 + 3 + 4 + ... = -1/12 -- Srinivasa Ramanujan
