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

[Kim Bruce]

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

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