Proposal: Generating Contacts for Parametric Opaque Types
1 Current contract behavior for parametric, non-opaque types
Currently, Typed Racket makes relatively weak guarantees when using parametric structural types from untyped code. This is unfortunately necessary since parametricity really only exists as a static construct. Without instantiating the types, contracts cannot be made. This allows programs like the following to successfully run.
> (module typed typed/racket/base (provide (struct-out Foo)) (struct [A] Foo ([x : A] [y : A]) #:transparent)) > (require 'typed) > (Foo "a" 'b) (Foo "a" 'b)
Obviously, it would be impossible to know that "a" and 'b are of different types because the concept of "types" does not exist at runtime. However, the following program demonstrates how Typed Racket prevents this lack of knowledge from "infecting" the typed code.
> (module typed-concat typed/racket/base (require 'typed) (provide foo-concat) (define (foo-concat [foo : (Foo String)]) : String (string-append (Foo-x foo) (Foo-y foo)))) > (require 'typed-concat) > (foo-concat (Foo "a" 'b)) foo-concat: contract violation
expected: String
given: 'b
in: the (#:selector Foo-y) field of
the 1st argument of
(-> (struct/c Foo String String) any)
contract from: typed-concat
blaming: program
(assuming the contract is correct)
at: eval:4.0
This demonstrates that parametric structure types are something of a derived concept in Typed Racket, despite being technically only being possible due to the struct special form. Importantly, the fact that Foo is parametric does not cause any additional contracts to be generated since A is directly used as a field type. Contracts are only created at the point of instantiation.
2 Extending parametricity to opaque types
If parameterized types are a wholly static concept, they should, in theory, be able to be extended to opaque types. As an example, consider the posn structure from lang/posn. This structure contains two fields of any type, but 2htdp/image provides real-valued-posn? as a predicate for use in contracts. Ideally, we would be able to express this in Typed Racket as a parameterized type.
A naïve attempt to use such a type in typed code might look something like this:
; make Posn parametric (define-type Posn (All (A) htdp:posn)) (provide Posn) (require/typed lang/posn [#:opaque htdp:posn posn?]) (require/typed/provide lang/posn [make-posn (All (A) A A -> (Posn A))] [posn-x (All (A) (Posn A) -> A)] [posn-y (All (A) (Posn A) -> A)])
Sadly, this fails. Typed Racket attempts to apply a parametric->/c contract to the various posn functions, and the values are wrapped. The wrapping and unwrapping functions are not shared between functions, so attempting to retrieve values from posn instances raises contract errors. Furthermore, even if the wrappers were shared between functions, untyped code would recieved wrapped values, which would render them quite useless.
However, as mentioned above, all of the contract checking on these functions can be done from the typed side at runtime. Typed Racket just needs some information about how to correctly generate contracts on opaque types.
2.1 Creating an idealized syntax for describing parametric opaque imports
The rest of the code in this document will be somewhat hypothetical and demonstrative. In order to demonstrate the way the system should work, there needs to be some basic syntax that can express the required ideas. The issues of implemented such forms is a problem not addressed by this document, but it is assumed to be trivial in comparison to the other problems laid out.
The proposed syntax to instruct Typed Racket to formulate a parametric type is as follows:
(require/typed [#:opaque (Posn A) posn?] [make-posn (All [A] A A -> (Posn A))] [posn-x (All [A] (Posn A) -> A A)] [posn-y (All [A] (Posn A) -> A A)])
There are some important notes about this syntax.
The actual important part occurs within the #:opaque declaration. This declares Posn as a parametric opaque type. This will need to be something of a first-class member of Typed Racket’s type system, just as much as structure types are.
In the various function declarations, the type of A is inferred from the arguments, just as in any other parametric type declaration. No wrapping or unwrapping is needed via parametric->/c. This guarantee is important! As mentioned earlier, any wrapping or unwrapping required by these functions will break interoperability with untyped Racket.
2.2 Using parametric opaque types in typed code
Just as with parametric structure types, parametric opaque types can be handled purely by the static typechecker as long as they stay in typed code. Of course, the major difference is that parametric opaque types must interact with untyped code by definition, since they are opaque. Even trickier, we cannot generate contracts as simply as we did with our Foo structure and the foo-concat function that used its instantiation. Why? Consider the following code.
(: posn-2x ((Posn Real) -> Real)) (define (posn-2x p) (* 2 (posn-x p))) (posn-2x (make-posn 2 4))
This should work! But what if our untyped code misbehaves? What if, instead of getting (posn 2 4) from make-posn, the untyped code returns (posn 2 'error)? This is surprisingly problematic because, in posn-2x, there is no way for Typed Racket to validate the provided value at runtime! Since posn-y is never used, as far as Typed Racket knows, everything is going just fine. And that’s actually okay. The types aren’t broken because posn-x is correct. Ideally, we’d get a contract failure, but technically nothing has gone wrong here.
But what about the other case? What if the returned value is completely bogus? What if make-posn yields (posn #f #f)? Now we need to produce some kind of contract failure. Obviously, the call to posn-x in the typed code should be protected with a contract ensuring that the return value is a Real. That’s not too hard—problem solved!
Unfortunately, it’s unclear exactly how the contract should be attached to posn-x. It can’t be attached in require/typed because the contract depends entirely on the type instantiation. Indeed, the contract needs to be attached in an on-demand basis. Typed Racket needs to infer that the call to posn-x is being applied with Real as the concrete type, and it needs to produce a chaperoned function in place of posn-x that will ensure its return type satisfies real?.
The precise mechanism by which the typechecker would be able to handle such a situation is unknown to me. The best approach would probably hinge on ensuring optimal performance. Either way, it seems that such a solution is well within the range of Typed Racket’s operational functionality.
2.3 Using parametric opaque types with untyped code
This area is something I haven’t given a huge amount of thought to, though it is relevant: what should the behavior be when exporting identifiers that interact with parametric opaque types, especially when imported into untyped modules? For the most part, the behavior described for interactions in typed code seem to generalize to untyped code, maintaining the parallel between parametric structure types and parametric opaque types.
Just like in the original example given using a parametric structure type, it would be impossible to enforce such constraints in untyped code without type instantiation, similar to the equivalent problem from the typed side of things.
3 A request for feedback and proposal to implement parametric opaque types
At this point, I will take the opportunity to speak for myself and admit that I am not terribly familiar with how Typed Racket’s typechecker and type environment work on the inside. I am certainly willing to attempt to implement something like this myself, but seeing as this is all quite hypothetical from my perspective, it would help to get the opinions of those more familiar with how these things are implemented.
I do believe that the implementation of such a system has the possibility of permitting the use of various untyped idioms in typed code. Besides HtDP’s posn type, the jsexpr? type from the JSON library comes to mind with its support for custom nulls. This is an immediate application of such a feature, and I could see it being made useful in other areas as well.
I would appreciate any comments on this proposal as well as any aid anyone is willing to give me to assist in my eventual implementation of parametricity for opaque types. Please do not hesitate to critique or make suggestions, as this is still a very simple draft, and I recognize that it might need some major changes before being viable.