<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;"><br><div><div>On Jan 29, 2015, at 11:34 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=windows-1252"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><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.</div></div></blockquote><br class=""></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 <i class="">nothing</i> about the contents of the value is what makes this such a tricky problem.</div><div class=""><br class=""></div><div class="">As for this:</div><div class=""><br 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?</div></div></blockquote><br class=""></div><div class="">That’s completely correct. That’s why it’s “opaque.”</div><div class=""><br 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?</div></div></blockquote><br class=""></div><div class="">That’s a little more interesting. Using <font face="Courier" class="">cast</font> on an object of this type would never fail (unless, of course, it didn’t actually satisfy the basic <font face="Courier" class="">posn?</font> predicate), but it would possibly introduce failures in the future since it would affect the contracts generated for <font face="Courier" class="">posn-x</font> and <font face="Courier" class="">posn-y</font>, for example.</div><div class=""><br class=""></div><div class="">To make that more clear, casting a <font face="Courier" class="">(Posn Real)</font> to a <font face="Courier" class="">(Posn String)</font> would work fine until you tried to call <font face="Courier" class="">posn-x</font> 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.</div></div></blockquote><div><br></div><div>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. </div><div><br></div><div>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. </div><div><br></div><div>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. </div><div><br></div><div>And for “this isn’t really any different from casting mutable data types,” look at this:</div><div><div>#lang typed/racket</div><div>(: b : (Boxof Number))</div><div>(define b (box 1))</div><div>(set-box! (cast b (Boxof (U Number String))) "I am a string")</div><div>(ann (unbox b) Number) ;"I am a string” ; not a contract error</div><div><br></div></div><br><blockquote type="cite"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><br class=""><div><blockquote type="cite" class=""><div class="">On Jan 29, 2015, at 20:20, Alexander D. Knauth <<a href="mailto:alexander@knauth.org" class="">alexander@knauth.org</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><meta http-equiv="Content-Type" content="text/html charset=windows-1252" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class=""><span style="font-family: Charter, serif; font-size: 18px; line-height: 24px; background-color: rgb(255, 255, 255);" class="">Furthermore, even if the wrappers </span><span style="margin: 0px; padding: 0px; font-family: Charter, serif; font-size: 18px; line-height: 24px; background-color: rgb(255, 255, 255); font-style: italic;" class="">were</span><span style="font-family: Charter, serif; font-size: 18px; line-height: 24px; background-color: rgb(255, 255, 255);" class=""> shared between functions, untyped code would recieved wrapped values, which would render them quite useless.</span></div><div class=""><br 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:</div><div class=""><div class="">#lang typed/racket</div><div class="">; make Posn parametric</div><div class="">(define-type (Posn A) (List A A))</div><div class="">(provide Posn)</div><div class="">(require/typed/provide</div><div class=""> "untyped.rkt"</div><div class=""> [make-posn (All (A) A A -> (Posn A))]</div><div class=""> [posn-x (All (A) (Posn A) -> A)]</div><div class=""> [posn-y (All (A) (Posn A) -> A)]</div><div class=""> [real-posn? [(Posn Any) -> Boolean]])</div></div><div class=""><div class="">> (define p (make-posn 1 2))</div><div class="">(make-posn #<A6> #<A6>) ; a printf that I put in make-posn from “untyped.rkt"</div><div class="">> p</div><div class="">- : (Listof Positive-Byte) [more precisely: (List Positive-Byte Positive-Byte)]</div><div class="">'(1 2) ; unwrapped</div><div class="">> (posn-x p)</div><div class="">- : Integer [more precisely: Positive-Byte]</div><div class="">1</div><div class="">> (posn-y p)</div><div class="">- : Integer [more precisely: Positive-Byte]</div><div class="">2</div><div class="">> (real-posn? p)</div><div class="">- : Boolean</div><div class="">#t</div></div><div class=""><br 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. </div><div class=""><br 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.</div><div class=""><br 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?</div><div class=""><br class=""></div><br class=""><div class=""><div class="">On Jan 29, 2015, at 9:25 PM, Alexis King <<a href="mailto:lexi.lambda@gmail.com" class="">lexi.lambda@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite" class=""><meta http-equiv="Content-Type" content="text/html charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" 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="">my attempt to port 2htdp/image to TR</a>.<div class=""><br 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:</div><div class=""><a href="http://lexi-lambda.github.io/racket-parametric-opaque-types/" class="">http://lexi-lambda.github.io/racket-parametric-opaque-types/</a></div><div class=""><br class=""></div><div class="">Any feedback, suggestions, or advice would be appreciated, especially from those who are familiar with Typed Racket’s internals.</div><div class=""><br class=""></div><div class="">Thank you,</div><div class="">Alexis</div></div>_________________________<br class=""> Racket Developers list:<br class=""> <a href="http://lists.racket-lang.org/dev" class="">http://lists.racket-lang.org/dev</a><br class=""></blockquote></div><br class=""></div></div></blockquote></div><br class=""></div></blockquote></div><br></body></html>