<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><br><div><div>On Jan 30, 2015, at 1:53 PM, Alexis King <<a href="mailto:lexi.lambda@gmail.com">lexi.lambda@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><meta http-equiv="Content-Type" content="text/html charset=utf-8"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class="">No, it doesn’t need to be wrapped in an opaque structure. Wrapping it in an opaque structure would add a layer of indirection for absolutely no gain. Remember, the value itself is already, by definition, <i class="">opaque</i>. The only way typed code can manipulate the value is by passing it to other functions imported via <font face="Courier" class="">require/typed</font>.</div><div class=""><br class=""></div><div class="">This means that contracts only need to be generated wherever those functions are called. This can be done without wrapping or unwrapping anything because all the information required to generate those contracts is known at expansion-time. The typechecker simply needs to insert the relevant contracts at the relevant locations.</div></div></blockquote><div><br></div><div>Imagine a program like this:</div><div>#lang typed/racket</div><div>(require typed/lang/posn)</div><div>(: p : (Posn Real Real)) ; I’m assuming Posn is parametric over 2 tvars, not 1</div><div>(define p (posn 1 2))</div><div>(: x : Real)</div><div>(define x (posn-x p))</div><div>As far as the type checker would check, it would check that the result of posn-x is a Real, but I think that the runtime contract it should also check that it returns 1, because posn could have been instantiated as (Posn 1 2).</div><div>#lang typed/racket</div><div>(require typed/lang/posn/mutable) ; like typed/lang/posn, but providing mutation too</div><div>(: p : (Posn Real Real))</div><div>(define p (posn 1 2))</div><div>(: x : Real)</div><div>(define x (posn-x p))</div><div>(set-posn-x! p 3)</div><div>(: x2 : Real)</div><div>(define x2 (posn-x p))</div><div>Here, even though the type checker only cares that it’s a number, it should check that x2 definition returns either 1 or 3, since both were provided as x values for the posn p.</div><div><br></div><div>For it to keep track of these at runtime, (and it would have to be runtime) the contracts would have to be with the actual posn value in an opaque structure, which would have contracts sort of like (new-∀/c) that would check these things, although I don’t think it would have to wrap the inner values, but just record them so that when posn-x is called on one of these things, it checks that it was one of the values that was passed in to either a constructor or setter function. </div><br><blockquote type="cite"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div><blockquote type="cite" class=""><div class="">On Jan 30, 2015, at 07:27, Alexander D. Knauth <<a href="mailto:alexander@knauth.org" class="">alexander@knauth.org</a>> wrote:</div><div class=""><div class="">
<div class=""> </div>
<div class="">On Thu, Jan 29, 2015, at 09:03 PM, Alexis King wrote:<br class=""></div>
<blockquote type="cite" class=""><div class="">It isn’t wrapped in an opaque structure. That wasn’t a part of my proposal, and while I didn’t think of it until you brought it up, I still think it’s unnecessary and doesn’t add any convenience.<br class=""></div>
</blockquote><div class=""> </div>
<div class="">I think the opaque structures would be necessary for the kind of "sharing wrappers between functions" that you describe just before section 2.1, except that instead of the sub-values being wrapped on the untyped side, the whole thing is wrapped on the typed side, and there is a contract that wraps it and unwraps it when it goes from untyped to typed and back. <br class=""></div>
<div class=""> </div>
<div class="">For parametric types, they have to also work if the type was constrained to the exact set of values that were provided, which means that if you provide two numbers, say 1 and 2, it has to return a posn with not just any two numbers, but values of the type (U 1 2), since A could have been constrained to (U 1 2). So it has to be wrapped somehow, and I think wrapping it on the typed side makes more sense. <br class=""></div>
<div class=""> </div>
<blockquote type="cite" class=""><div class="">Perhaps I’m not understanding you properly, but your “one-length string” idea sounds like it has little to do with this opaque type problem and more to do with the fact that you want refinement types in Typed Racket. I do, too! But I don’t think hacking the opaque type system is going to help you with that.<br class=""></div>
</blockquote><div class=""> </div>
<div class="">Well, yeah, refinement types would be the "real" solution for this particular example, but if I do want to constrain it to strings of length 1, opaque types are the only option for now, and they actually work fine. My point was you couldn't do this type of thing with the opaque structures and you would probably get weird errors if you tried. (See below because there might be a solution?)<br class=""></div>
<div class=""> </div>
<blockquote type="cite" class=""><div class="">(Also, as for the box example, I’m actually a little surprised that doesn’t contract error. Seems like a bug to me, but perhaps I’m missing some idiosyncrasies of the type system. Either way, it’s precisely that kind of craziness I was referring to when I compared casting parametric opaque types to casting mutable types.)<br class=""></div>
</blockquote><div class=""> </div>
<div class="">There is a bug report for it here, and the solution proposed by Sam Tobin-Hochstadt would be for cast to generate 2 contracts, one for the original type, one for the new type, but that never got implemented. <br class=""></div>
<div class=""><a href="http://bugs.racket-lang.org/query/?cmd=view&pr=13626" class="">http://bugs.racket-lang.org/query/?cmd=view&pr=13626</a><br class=""></div>
<div class=""> </div>
<div class="">Actually now that I think about it the two-contract solution might be able to solve the previous problem, since the original contract could unwrap the value before it is passed to the new contract? I'm not sure though. The value inside the cast would be from the typed side, then it is passed through the orig contract as if it were going to the typed side,</div></div></div></blockquote></div></div></blockquote><div><br></div><div>This was a typo, I meant to say “as if it were going to the untyped side"</div><br><blockquote type="cite"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div><blockquote type="cite" class=""><div class=""><div class=""><div class=""> which would unwrap it, and then that unwrapped value would be passed to the new contract as if it were flowing from the untyped side to the typed side. <br class=""></div>
<div class=""> </div>
<blockquote type="cite" class=""><div class=""> </div>
<div class=""><blockquote type="cite" class=""><div class="">On Jan 29, 2015, at 20:50, Alexander D. Knauth <<a href="mailto:alexander@knauth.org" class="" defang_rel="noreferrer">alexander@knauth.org</a>> wrote:<br class=""></div>
<div class=""> </div>
<div class=""><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""> </div>
<div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">On Jan 29, 2015, at 11:34 PM, Alexis King <<a href="mailto:lexi.lambda@gmail.com" class="" defang_rel="noreferrer">lexi.lambda@gmail.com</a>> wrote:<br class=""></div>
<div class=""> </div>
<blockquote type="cite" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><blockquote type="cite" class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class="">But the problem is that if it’s an opaque type then it can’t unwrap it once the value is returned from make-posn.<br class=""></div>
</div>
</blockquote><div class=""> </div>
</div>
<div class="">Yes, that’s precisely the problem. Your point about implementing everything as single-valued structs on the typed side is an interesting one, though I don’t think it ultimately solves any problems. The fact that the typed side knows<span class=""></span><i class="">nothing</i><span class=""></span>about the contents of the value is what makes this such a tricky problem.<br class=""></div>
<div class=""> </div>
<div class="">As for this:<br class=""></div>
<div class=""> </div>
<div class=""><blockquote type="cite" class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class="">But then you couldn’t do any operations on it except those that you use import with require/typed, right?<br class=""></div>
</div>
</blockquote><div class=""> </div>
</div>
<div class="">That’s completely correct. That’s why it’s “opaque.”<br class=""></div>
<div class=""> </div>
<div class=""><blockquote type="cite" class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class="">And what happens if you use cast on one of these things?<br class=""></div>
</div>
</blockquote><div class=""> </div>
</div>
<div class="">That’s a little more interesting. Using<span class=""></span><span class="font" style="font-family:Courier">cast</span><span class=""></span>on an object of this type would never fail (unless, of course, it didn’t actually satisfy the basic<span class=""></span><span class="font" style="font-family:Courier">posn?</span><span class=""></span>predicate), but it would possibly introduce failures in the future since it would affect the contracts generated for<span class=""></span><span class="font" style="font-family:Courier">posn-x</span><span class=""></span>and<span class=""></span><span class="font" style="font-family:Courier">posn-y</span>, for example.<br class=""></div>
<div class=""> </div>
<div class="">To make that more clear, casting a<span class=""></span><span class="font" style="font-family:Courier">(Posn Real)</span><span class=""></span>to a<span class=""></span><span class="font" style="font-family:Courier">(Posn String)</span><span class=""></span>would work fine until you tried to call<span class=""></span><span class="font" style="font-family:Courier">posn-x</span><span class=""></span>on the instance, in which case it would raise a contract error. Note that this isn’t really any different from casting mutable data types.<br class=""></div>
</div>
</blockquote><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""> </div>
<div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">But if it were wrapped in an opaque structure, then that structure wouldn’t satisfy the posn? predicate, unless of course the posn? predicate has a contract that unwraps it. So all of the operations on it would have to have contracts that would unwrap it. This might actually make sense if the type is meant to be actually opaque, but if it’s an opaque type that represents a normal non-opaque value, then it will still work as an opaque type, but it won’t be a normal non-opaque value anymore on the typed side. <br class=""></div>
<div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""> </div>
<div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">But the reason I asked about cast was because normally I can use cast with a value that has an opaque type, but it’s wrapped on the typed side in this opaque structure, then the contracts on the cast would see this opaque structure instead of the actual value. <br class=""></div>
<div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""> </div>
<div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">I’m thinking of an opaque typed representing a string with length 1, which I can use as long as I use either (cast x String) or (assert x string?) whenever I pass it to a string operation. But if it were an opaque type, I don’t think I could do that. There could be a 1string->string function that could take one of these 1strings and convert it to a string, but that seems like it should be unnecessary, but made necessary by this opaque structure thing. <br class=""></div>
<div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""> </div>
<div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">And for “this isn’t really any different from casting mutable data types,” look at this:<br class=""></div>
<div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><div class="">#lang typed/racket<br class=""></div>
<div class="">(: b : (Boxof Number))<br class=""></div>
<div class="">(define b (box 1))<br class=""></div>
<div class="">(set-box! (cast b (Boxof (U Number String))) "I am a string")<br class=""></div>
<div class="">(ann (unbox b) Number) ;"I am a string” ; not a contract error<br class=""></div>
<div class=""> </div>
</div>
<div class=""> </div>
<blockquote type="cite" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""> </div>
<div class=""><blockquote type="cite" class=""><div class="">On Jan 29, 2015, at 20:20, Alexander D. Knauth <<a href="mailto:alexander@knauth.org" class="" defang_rel="noreferrer">alexander@knauth.org</a>> wrote:<br class=""></div>
<div class=""> </div>
<div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><span class="highlight" style="background-color: rgb(255, 255, 255)"><span class="font" style="font-family:Charter, serif"><span class="size" style="font-size:18px">Furthermore, even if the wrappers </span></span></span><span class="highlight" style="background-color: rgb(255, 255, 255)"><i class=""><span class="font" style="font-family:Charter, serif"><span class="size" style="font-size:18px">were</span></span></i></span><span class="highlight" style="background-color: rgb(255, 255, 255)"><span class="font" style="font-family:Charter, serif"><span class="size" style="font-size:18px"> shared between functions, untyped code would recieved wrapped values, which would render them quite useless.</span></span></span><br class=""></div>
<div class=""> </div>
<div class="">If it’s not an opaque type, but something like a list, then this works, and the untyped code receiving wrapped values isn’t a problem here:<br class=""></div>
<div class=""><div class="">#lang typed/racket<br class=""></div>
<div class="">; make Posn parametric<br class=""></div>
<div class="">(define-type (Posn A) (List A A))<br class=""></div>
<div class="">(provide Posn)<br class=""></div>
<div class="">(require/typed/provide<br class=""></div>
<div class=""> "untyped.rkt"<br class=""></div>
<div class=""> [make-posn (All (A) A A -> (Posn A))]<br class=""></div>
<div class=""> [posn-x (All (A) (Posn A) -> A)]<br class=""></div>
<div class=""> [posn-y (All (A) (Posn A) -> A)]<br class=""></div>
<div class=""> [real-posn? [(Posn Any) -> Boolean]])<br class=""></div>
</div>
<div class=""><div class="">> (define p (make-posn 1 2))<br class=""></div>
<div class="">(make-posn #<A6> #<A6>) ; a printf that I put in make-posn from “untyped.rkt"<br class=""></div>
<div class="">> p<br class=""></div>
<div class="">- : (Listof Positive-Byte) [more precisely: (List Positive-Byte Positive-Byte)]<br class=""></div>
<div class="">'(1 2) ; unwrapped<br class=""></div>
<div class="">> (posn-x p)<br class=""></div>
<div class="">- : Integer [more precisely: Positive-Byte]<br class=""></div>
<div class="">1<br class=""></div>
<div class="">> (posn-y p)<br class=""></div>
<div class="">- : Integer [more precisely: Positive-Byte]<br class=""></div>
<div class="">2<br class=""></div>
<div class="">> (real-posn? p)<br class=""></div>
<div class="">- : Boolean<br class=""></div>
<div class="">#t<br class=""></div>
</div>
<div class=""> </div>
<div class="">Even though for a short time it's wrapped, it’s unwrapped as soon as make-posn returns, and then after that if it flows into untyped code again it’s not wrapped and functions like real-posn? work fine. <br class=""></div>
<div class=""> </div>
<div class="">But the problem is that if it’s an opaque type then it can’t unwrap it once the value is returned from make-posn.<br class=""></div>
<div class=""> </div>
<div class="">And I don’t think parametric opaque types could solve this unless all posns themselves were wrapped with an opaque struct on the typed side, which I guess does make sense now that I think about it. But then you couldn’t do any operations on it except those that you use import with require/typed, right? Or not? And what happens if you use cast on one of these things?<br class=""></div>
<div class=""> </div>
<div class=""> </div>
<div class=""><div class="">On Jan 29, 2015, at 9:25 PM, Alexis King <<a href="mailto:lexi.lambda@gmail.com" class="" defang_rel="noreferrer">lexi.lambda@gmail.com</a>> wrote:<br class=""></div>
<div class=""> </div>
<blockquote type="cite" class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class="">I recently ran into a problem in which opaque types (types imported from untyped code) cannot by parameterized by Typed Racket. I initially encountered this problem in <a href="https://github.com/lexi-lambda/racket-2htdp-typed/issues/1" class="" defang_rel="noreferrer">my attempt to port 2htdp/image to TR</a>.<br class=""></div>
<div class=""> </div>
<div class="">After some further consideration, I’m interested in adding support to make something like this possible, which would certainly have additional benefits beyond this specific use-case. I’ve outlined my proposal here:<br class=""></div>
<div class=""><a href="http://lexi-lambda.github.io/racket-parametric-opaque-types/" class="" defang_rel="noreferrer">http://lexi-lambda.github.io/racket-parametric-opaque-types/</a><br class=""></div>
<div class=""> </div>
<div class="">Any feedback, suggestions, or advice would be appreciated, especially from those who are familiar with Typed Racket’s internals.<br class=""></div>
<div class=""> </div>
<div class="">Thank you,<br class=""></div>
<div class="">Alexis<br class=""></div>
</div>
<div class="">_________________________<br class=""></div>
<div class=""> Racket Developers list:<br class=""></div>
<div class=""> <a href="http://lists.racket-lang.org/dev" class="" defang_rel="noreferrer">http://lists.racket-lang.org/dev</a><br class=""></div>
</blockquote></div>
</div>
</div>
</blockquote></div>
</div>
</blockquote></div>
</blockquote></div>
<div class=""> </div>
</blockquote><div class=""> </div>
</div>
</div></blockquote></div><br class=""></div></blockquote></div><br></body></html>