<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">My book refers to these things as ClassType’s and they behave very different from object types (as you observe). I’ve been working to try to avoid writing down the ClassTypes as programmers will hate writing them down. The whole idea of statically determinable types (at least in my mind) was to have a system so transparent that the ClassTypes could easily be inferred by the system.<div class=""><br class=""></div><div class="">Perhaps I should return to that (provably type-safe) system and start over. My impression (and correct me if I am wrong) is that those interested in the dynamic language want things to be much more flexible than are compatible with a static type system, even one with type Dynamic.</div><div class=""><br class=""></div><div class="">I’m getting the sense that the simplicity is obtained by either dropping almost all restrictions or by going completely statically typed, while intermediate positions (e.g., banning overloading) make things more difficult.</div><div class=""><br class=""><div class="">
<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 class="">Kim</div><div class=""><br class=""></div></span><br class="Apple-interchange-newline">
</div>
<br class=""><div><blockquote type="cite" class=""><div class="">On Mar 16, 2015, at 2:06 PM, Andrew P Black <<a href="mailto:andrew.p.black@gmail.com" class="">andrew.p.black@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Kim,<div class=""><br class=""></div><div class="">What you are observing is that just because module m is correct, and can be proved so by a fairly simple type system, does <i class="">not</i> mean that every possible module m' that inherits from m and overrides arbitrary parts of m is also correct and type-safe. <br class=""></div><div class=""><br class=""></div><div class="">If you want to do static checks for this, it's always seemed to me that m needs two quite different types. The first is the user's type, or the interface type, which provides information about the external interface of m — which is what existing Grace types do.</div><div class=""><br class=""></div><div class="">The second is the heir's type, which provides information about the internal structure of m. In your example, it provides the information that a.new -> Alpha and Alpha <: type {x -> Number} (which is in the confidential interface type), but also that b.new uses a internally, with that type. </div><div class=""><br class=""></div><div class="">Figuring out what's in an heirs type seems like a good thesis project.</div><div class=""><br class=""></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span>Andrew</div><div class=""><br class=""></div></div></div></blockquote></div><br class=""></div></body></html>