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

> 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.

> 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 <mailto: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 <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>
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20150129/6fc5a8fe/attachment.html>