Okay, now I see what you’re saying. That’s a reasonable point, and it’s worth considering. Thanks for bearing with me.
> On Jan 30, 2015, at 13:24, Alexander D. Knauth <alexan...@knauth.org> wrote: > > > On Jan 30, 2015, at 3:59 PM, Alexis King <lexi.lam...@gmail.com > <mailto:lexi.lam...@gmail.com>> wrote: > >> No, the typechecker can’t make any assumptions about the results of opaque >> types. If you explicitly instantiate a Posn with the type Real, the >> typechecker should only guarantee the result will be Real. Annotate the type >> as (U 1 2), though, and obviously it would need to ensure that remains >> invariant. > > How about this program: > untyped.rkt: > #lang racket > (provide (all-defined-out)) > (define (make-posn x y) (list 3 y)) ; bad > typed.rkt: > #lang typed/racket > ; make Posn parametric > (define-type (Posn X Y) (List X Y)) > (require/typed "untyped.rkt" > [make-posn (All (X Y) X Y -> (Posn X Y))]) > (: p : (Posn Real Real)) > (define p (make-posn 1 2)) > This gives this error: > . . make-posn: broke its contract > promised: X3 > produced: 3 > in: the car of > the range of > (parametric->/c > (X3 Y4) > (->* > (X3 Y4) > () > (values (cons/c X3 (cons/c Y4 g6))))) > contract from: (interface for make-posn) > blaming: (interface for make-posn) > (assuming the contract is correct) > at: …./typed.rkt:5.16 > > I think it’s a good thing that it checks that it actually gives you the value > that you gave it, and not just something like 3 even if it happens to match > the type you want. And I think parametric opaque types should behave in a > similar way, and to do that you would need the opaque value to be wrapped in > another opaque structure, which would store either the contracts or the set > of values that would pass the contracts or something like that. > >> >>> On Jan 30, 2015, at 12:30, Alexander D. Knauth <alexan...@knauth.org >>> <mailto:alexan...@knauth.org>> wrote: >>> >>> >>> On Jan 30, 2015, at 1:53 PM, Alexis King <lexi.lam...@gmail.com >>> <mailto:lexi.lam...@gmail.com>> wrote: >>> >>>> 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, opaque. The >>>> only way typed code can manipulate the value is by passing it to other >>>> functions imported via require/typed. >>>> >>>> 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. >>> >>> Imagine a program like this: >>> #lang typed/racket >>> (require typed/lang/posn) >>> (: p : (Posn Real Real)) ; I’m assuming Posn is parametric over 2 tvars, >>> not 1 >>> (define p (posn 1 2)) >>> (: x : Real) >>> (define x (posn-x p)) >>> 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). >>> #lang typed/racket >>> (require typed/lang/posn/mutable) ; like typed/lang/posn, but providing >>> mutation too >>> (: p : (Posn Real Real)) >>> (define p (posn 1 2)) >>> (: x : Real) >>> (define x (posn-x p)) >>> (set-posn-x! p 3) >>> (: x2 : Real) >>> (define x2 (posn-x p)) >>> 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. >>> >>> 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. >>> >>>>> On Jan 30, 2015, at 07:27, Alexander D. Knauth <alexan...@knauth.org >>>>> <mailto:alexan...@knauth.org>> wrote: >>>>> >>>>> On Thu, Jan 29, 2015, at 09:03 PM, Alexis King wrote: >>>>>> 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. >>>>> >>>>> 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. >>>>> >>>>> >>>>> 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. >>>>> >>>>>> 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. >>>>> >>>>> 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?) >>>>> >>>>>> (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.) >>>>> >>>>> 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. >>>>> http://bugs.racket-lang.org/query/?cmd=view&pr=13626 >>>>> <http://bugs.racket-lang.org/query/?cmd=view&pr=13626> >>>>> >>>>> 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, >>> >>> This was a typo, I meant to say “as if it were going to the untyped side" >>> >>>>> 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. >>>>> >>>>>> >>>>>>> On Jan 29, 2015, at 20:50, Alexander D. Knauth <alexan...@knauth.org >>>>>>> <mailto: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 knowsnothingabout 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. Usingcaston an object of this type >>>>>>>> would never fail (unless, of course, it didn’t actually satisfy the >>>>>>>> basicposn?predicate), but it would possibly introduce failures in the >>>>>>>> future since it would affect the contracts generated >>>>>>>> forposn-xandposn-y, for example. >>>>>>>> >>>>>>>> To make that more clear, casting a(Posn Real)to a(Posn String)would >>>>>>>> work fine until you tried to callposn-xon 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
