<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">John,<div><br></div><div>We couldn't understand your example. Can you explain it?</div><div><br><div apple-content-edited="true">
<span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0; "><div>Kim</div><div><br></div></span></div><div><br><blockquote type="cite"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><div>Begin forwarded message:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;"><span style="font-family: Helvetica; font-size: medium; "><b>From: </b></span><span style="font-family:'Helvetica'; font-size:medium;">John Tang Boyland <<a href="mailto:boyland@pabst.cs.uwm.edu">boyland@pabst.cs.uwm.edu</a>><br></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;"><span style="font-family: Helvetica; font-size: medium; "><b>Subject: </b></span><span style="font-family:'Helvetica'; font-size:medium;"><b>INCOMPLETE: gradual typing + structural typing + typecase</b><br></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;"><span style="font-family: Helvetica; font-size: medium; "><b>Date: </b></span><span style="font-family:'Helvetica'; font-size:medium;">July 2, 2013 4:12:58 PM GMT+02:00<br></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;"><span style="font-family: Helvetica; font-size: medium; "><b>To: </b></span><span style="font-family:'Helvetica'; font-size:medium;"><a href="mailto:kim@cs.pomona.edu">kim@cs.pomona.edu</a><br></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;"><span style="font-family: Helvetica; font-size: medium; "><b>Cc: </b></span><span style="font-family:'Helvetica'; font-size:medium;"><a href="mailto:boyland@uwm.edu">boyland@uwm.edu</a><br></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px;"><span style="font-family: Helvetica; font-size: medium; "><b>Reply-To: </b></span><span style="font-family:'Helvetica'; font-size:medium;"><a href="mailto:boyland@uwm.edu">boyland@uwm.edu</a><br></span></div><br><div>Dear Kim,<br> Here's a start with a counter-example<br>whcih requires mutable fields:<br><br>Executive summary: Pick two of three:<br><br>- gradual typing<br>- structural (sub)types<br>- typecase<br><br>You can't have all three.<br><br><br>Definitions:<br><br>Gradual typing: The system can execute code in which some type<br>annotations on parameters/return types/names can be omitted, but<br>the execution result will be the same.<br><br><br>Structural object (sub)types: <br><br>Types for objects consist of names and types of methods.<br>Type system has structural subtyping<br>Type system permits recursive types.<br>Type system may or may not permit union types.<br><br><br>typecase:<br><br>There is a capability to test types as runtime either with<br>something like Scala's "match", or even like Java's "instanceof"<br><br><span class="Apple-tab-span" style="white-space:pre"> </span> if (x instanceof T) {<br><span class="Apple-tab-span" style="white-space:pre"> </span> ...<br><span class="Apple-tab-span" style="white-space:pre"> </span> } else {<br><span class="Apple-tab-span" style="white-space:pre"> </span> ...<br><span class="Apple-tab-span" style="white-space:pre"> </span> }<br><br><br><br>Assuming we have mutable fields, I can provide a very simple<br>counter-example:<br><br> type A = { a : A -> A }<br><span class="Apple-tab-span" style="white-space:pre"> </span>type B = { b : B -> B }<br><br><span class="Apple-tab-span" style="white-space:pre"> </span>val x = { var f : A = { def a(x) = x;<br> def b(y) = y; }<br> def get() = f;<br> def set(g) = f = g;<br> }<br><br>then x has type { get : {} -> A, set : A -> {} }<br>so if we write:<br><br><span class="Apple-tab-span" style="white-space:pre"> </span>if (x instanceof B) {<br><span class="Apple-tab-span" style="white-space:pre"> </span> print("1");<br><span class="Apple-tab-span" style="white-space:pre"> </span>} else {<br><span class="Apple-tab-span" style="white-space:pre"> </span> print("2"):<br> }<br><br>This code will print "2".<br><br>But if the annotation on "f" is erased, it can print "1".<br><br>John<br></div></blockquote></div><br></div>_______________________________________________<br>Grace-core mailing list<br><a href="mailto:Grace-core@cecs.pdx.edu">Grace-core@cecs.pdx.edu</a><br>https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core<br></blockquote></div><br></div></body></html>