[Grace-core] Fwd: INCOMPLETE: gradual typing + structural typing + typecase

[Kim Bruce]

John,

We couldn't understand your example.  Can you explain it?

Kim


> Begin forwarded message:
> 
>> From: John Tang Boyland <boyland at pabst.cs.uwm.edu>
>> Subject: INCOMPLETE: gradual typing + structural typing + typecase
>> Date: July 2, 2013 4:12:58 PM GMT+02:00
>> To: kim at cs.pomona.edu
>> Cc: boyland at uwm.edu
>> Reply-To: boyland at uwm.edu
>> 
>> Dear Kim,
>>   Here's a start with a counter-example
>> whcih requires mutable fields:
>> 
>> Executive summary: Pick two of three:
>> 
>> - gradual typing
>> - structural (sub)types
>> - typecase
>> 
>> You can't have all three.
>> 
>> 
>> Definitions:
>> 
>> Gradual typing: The system can execute code in which some type
>> annotations on parameters/return types/names can be omitted, but
>> the execution result will be the same.
>> 
>> 
>> Structural object (sub)types: 
>> 
>> Types for objects consist of names and types of methods.
>> Type system has structural subtyping
>> Type system permits recursive types.
>> Type system may or may not permit union types.
>> 
>> 
>> typecase:
>> 
>> There is a capability to test types as runtime either with
>> something like Scala's "match", or even like Java's "instanceof"
>> 
>> 	  if (x instanceof T) {
>> 	     ...
>> 	  } else {
>> 	     ...
>> 	  }
>> 
>> 
>> 
>> Assuming we have mutable fields, I can provide a very simple
>> counter-example:
>> 
>>        type A = { a : A -> A }
>> 	type B = { b : B -> B }
>> 
>> 	val x = { var f : A = { def a(x) = x;
>>                                def b(y) = y; }
>>                  def get() = f;
>>                  def set(g) = f = g;
>>                }
>> 
>> then x has type { get : {} -> A, set : A -> {} }
>> so if we write:
>> 
>> 	if (x instanceof B) {
>> 	    print("1");
>> 	} else {
>> 	    print("2"):
>>        }
>> 
>> This code will print "2".
>> 
>> But if the annotation on "f" is erased, it can print "1".
>> 
>> John
> 
> _______________________________________________
> Grace-core mailing list
> Grace-core at cecs.pdx.edu
> https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailhost.cecs.pdx.edu/pipermail/grace-core/attachments/20130702/ec30f30c/attachment-0001.html>