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:

Reply via email to