[racket-dev] A proposal for parametric opaque types in Typed Racket

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

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, 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
>> <alexander at knauth.org> wrote:
>>
>>
>> On Jan 29, 2015, at 11:34 PM, Alexis King
>> <lexi.lambda at 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. 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
>>>> <alexander at 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.lambda at 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[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/
>>>>>
>>>>> 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
>



Links:

  1. https://github.com/lexi-lambda/racket-2htdp-typed/issues/1
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20150130/bf1a3064/attachment-0001.html>