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

I think you’re reading too far into what I’m proposing, though I admit I probably didn’t give enough context. I’ve been talking with Sam about this issue on IRC, so he knows what I’m talking about, but I’ll try and clarify here.

This entire thing is just a fix for the problem described in Section 2 <http://lexi-lambda.github.io/racket-parametric-opaque-types/#(part._.Extending_parametricity_to_opaque_types)>. When using require/typed to import “opaque” types from untyped code, the imported types cannot be polymorphic. This entire proposal is simply a way to make that possible.

In Section 2.1, A is used in a number of places, but it is just a type parameter. See the typed struct definition in Section 1. A does not refer to a specific type but any type. Posn essentially becomes a new type combinator than can make new types by supplying it with any other type.

The other functions imported in Section 2.1 simply make use of Typed Racket’s polymorphic type utilities to make use of the fact that Posn is now a polymorphic type. The concepts here are simple. No semantics are being changed, it’s just extending parameterization to opaque types.

Sections 2.3 and 2.2, in contrast, are simply describing mechanisms for implementing the functionality outlined in 2.1.

Now to answer your points.

> - Should an A only be a base type like String or Symbol

A can by any type. It’s a type parameter. (Posn A) is like (Boxof A).

> - Do you mean to infer the type of the first thing put into the struct as the exact type for everything else?

No, not really. Remember that Posn is an opaque type. TR has no idea it’s actually implemented as a struct. Perhaps the JSExpr example given in Section 3 will help to illustrate that generality. This will just leverage the existing polymorphic type inference mechanisms TR already provides.

> - Would "first class members" prevent me from filling a struct with members of (define-type (Option A) (U 'None (Some A))), where "Some" is a struct with one field?

No, as I said, you can supply any type for A. By “first class member” of the type system, I simply meant that these types would have to be built-in to TR as a special case—they cannot be derived from the existing type constructs provided by TR. This is similar to how structure types are “first class” in TR—the struct form is “magical” and cannot be reimplemented in terms of other TR primitives.

I hope that helps to make things a little more clear.

> On Jan 29, 2015, at 19:44, Benjamin Greenman <blg59 at cornell.edu> wrote:
> 
> This has bothered me too, but I've realized that I was on the wrong track.
> 
> The string "a" and symbol 'b are not different types. A struct (Foo "a" 'b), or (list "a" 'b), is a homogeneous data structure of type (U String Symbol) just like Alexander said. This really upsets me -- I like the Hindley Milner world where the compiler warns me if I make a list [1, "two"] and forces me to wrap the int and string into a new datatype. But Typed Racket is not HM.
> 
> About the proposal, I'm confused about what the syntax in Section 2.1 should do -- what is a "first class member of Typed Racket's type system"?
> - Should an A only be a base type like String or Symbol
> - Do you mean to infer the type of the first thing put into the struct as the exact type for everything else?
> - Would "first class members" prevent me from filling a struct with members of (define-type (Option A) (U 'None (Some A))), where "Some" is a struct with one field?
> 
> I totally agree that "something needs fixing", but I'm not sure what.
> 
> 
> 
> On Thu, Jan 29, 2015 at 10:13 PM, Alexis King <lexi.lambda at gmail.com <mailto:lexi.lambda at gmail.com>> wrote:
> Or Any for that matter. I know. The fact that it could be literally anything was sort of the point.
> 
>> On Jan 29, 2015, at 19:10, Alexander D. Knauth <alexander at knauth.org <mailto:alexander at knauth.org>> wrote:
>> 
>> Um, for this:
>> (module <http://docs.racket-lang.org/reference/module.html#%28form._%28%28quote._~23~25kernel%29._module%29%29> typed typed/racket/base
>>     (provide <http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._provide%29%29> (struct-out <http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._struct-out%29%29> Foo))
>>     (struct <http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._struct%29%29> [A] Foo ([x : <http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29> A] [y : <http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29> A]) #:transparent))
>> 
>> (Foo "a" 'b)
>> Should be fine because Foo could be instantiated at the type (U String Symbol).
>> 
>> 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>
>> 
> 
> 
> _________________________
>   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/1568ffac/attachment.html>