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.
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. (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.) > On Jan 29, 2015, at 20:50, Alexander D. Knauth <alexan...@knauth.org> wrote: > > > On Jan 29, 2015, at 11:34 PM, Alexis King <lexi.lam...@gmail.com > <mailto:lexi.lam...@gmail.com>> wrote: > >>> 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. >> >> 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 nothing about the contents of the value is what makes this such a >> tricky problem. >> >> As for this: >> >>> But then you couldn’t do any operations on it except those that you use >>> import with require/typed, right? >> >> That’s completely correct. That’s why it’s “opaque.” >> >>> And what happens if you use cast on one of these things? >> >> That’s a little more interesting. Using cast on an object of this type would >> never fail (unless, of course, it didn’t actually satisfy the basic posn? >> predicate), but it would possibly introduce failures in the future since it >> would affect the contracts generated for posn-x and posn-y, for example. >> >> To make that more clear, casting a (Posn Real) to a (Posn String) would work >> fine until you tried to call posn-x 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. > > 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. > > 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. > > 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. > > And for “this isn’t really any different from casting mutable data types,” > look at this: > #lang typed/racket > (: b : (Boxof Number)) > (define b (box 1)) > (set-box! (cast b (Boxof (U Number String))) "I am a string") > (ann (unbox b) Number) ;"I am a string” ; not a contract error > > >> >>> On Jan 29, 2015, at 20:20, Alexander D. Knauth <alexan...@knauth.org >>> <mailto:alexan...@knauth.org>> wrote: >>> >>> Furthermore, even if the wrappers were shared between functions, untyped >>> code would recieved wrapped values, which would render them quite useless. >>> >>> 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: >>> #lang typed/racket >>> ; make Posn parametric >>> (define-type (Posn A) (List A A)) >>> (provide Posn) >>> (require/typed/provide >>> "untyped.rkt" >>> [make-posn (All (A) A A -> (Posn A))] >>> [posn-x (All (A) (Posn A) -> A)] >>> [posn-y (All (A) (Posn A) -> A)] >>> [real-posn? [(Posn Any) -> Boolean]]) >>> > (define p (make-posn 1 2)) >>> (make-posn #<A6> #<A6>) ; a printf that I put in make-posn from >>> “untyped.rkt" >>> > p >>> - : (Listof Positive-Byte) [more precisely: (List Positive-Byte >>> Positive-Byte)] >>> '(1 2) ; unwrapped >>> > (posn-x p) >>> - : Integer [more precisely: Positive-Byte] >>> 1 >>> > (posn-y p) >>> - : Integer [more precisely: Positive-Byte] >>> 2 >>> > (real-posn? p) >>> - : Boolean >>> #t >>> >>> 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. >>> >>> 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. >>> >>> 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? >>> >>> >>> On Jan 29, 2015, at 9:25 PM, Alexis King <lexi.lam...@gmail.com >>> <mailto:lexi.lam...@gmail.com>> wrote: >>> >>>> 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 my attempt to port 2htdp/image to TR >>>> <https://github.com/lexi-lambda/racket-2htdp-typed/issues/1>. >>>> >>>> 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: >>>> http://lexi-lambda.github.io/racket-parametric-opaque-types/ >>>> <http://lexi-lambda.github.io/racket-parametric-opaque-types/> >>>> >>>> Any feedback, suggestions, or advice would be appreciated, especially from >>>> those who are familiar with Typed Racket’s internals. >>>> >>>> Thank you, >>>> Alexis >>>> _________________________ >>>> Racket Developers list: >>>> http://lists.racket-lang.org/dev <http://lists.racket-lang.org/dev>
_________________________ Racket Developers list: http://lists.racket-lang.org/dev
