duelling theorists...
Jim and Palsberg add the syntax
This bothers me, because of the following example: in Jim and Palsberg's system, what is the meaning of the type expression
I see two possible (informal) interpretations of the above type expression: either
Assuming one of these interpretations is correct, is there a way to express the other interpretation? Or is this a useless goal? It seems to me that if we were to actually bind some name to each selftype for the type subexpressions, then we could unambiguously express either option.
selftype
, and deliberately choose to add this syntax, "rather than binding a name for selftype
in each object type." They state that the desired meaning can always be recovered, because each occurrence of selftype
comes with its context.This bothers me, because of the following example: in Jim and Palsberg's system, what is the meaning of the type expression
[makeref : [ref : selftype]]
?I see two possible (informal) interpretations of the above type expression: either
selftype
represents some subtype of the entire type expression, or it represents some subtype of the type subexpression [ref : selftype]
alone. I'm guessing that the former interpretation is correct, but I have not taken the time to go through the rules to verify this.Assuming one of these interpretations is correct, is there a way to express the other interpretation? Or is this a useless goal? It seems to me that if we were to actually bind some name to each selftype for the type subexpressions, then we could unambiguously express either option.
1 Comments:
Selftype always, in this type system, refers to the closest enclosing object type. This leaves some types unrepresentable, but the type theory is much easier when selftype always means precisely the one thing. I don't believe the other type is expressible in this system, but I hypothesize (without explicit justification) that any computation you could express in the other system can be simulated by a modified program in this one. This would be a meaningless statement, except (a) I believe the modification could be minor and (b) I'm not actually sure this is a Turing-complete language without extensions, so simulating other languages might not be trivial to prove.
Post a Comment
<< Home