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 <> wrote:
> On Jan 29, 2015, at 11:34 PM, Alexis King < 
> <>> 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 < 
>>> <>> 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 < 
>>> <>> 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 
>>>> <>.
>>>> 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:
>>>> <>
>>>> 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:
>>>> <>
  Racket Developers list:

Reply via email to