[racket] Typed Racket: problem with interaction between typed/untyped modules

From: Sam Tobin-Hochstadt (samth at ccs.neu.edu)
Date: Fri Dec 2 17:59:00 EST 2011

On Fri, Dec 2, 2011 at 5:38 PM, Ismael Figueroa Palet
<ifigueroap at gmail.com> wrote:
> I'm trying to implement a function wrapper, that given any function returns
> a function of the same type, but that maybe applies a different argument. So
> far I haven't been successful, and based on previous questions to the mail
> list it seemed that I needed to go to an untyped module because I couldn't
> constraint values to a given type.

In general, I don't think that any solution is going to work here.
You can't take arbitrary functions and apply them to specific
arguments (such as the string "blabla") in a type-safe way.

In you particular example, the function `f' is a constant function.
But what if it expected `Integer' as its argument?  Then your untyped
code would be violating the type invariants.

However, you can make your program work just by removing the
parameterization over `A', and replacing that with `Any'.  Then your
program is safe, and your untyped module can safely call the function
with any value it wants.  However, you have to guarantee that the
typed function can accept any kind of value (which `f' does, but other
functions might not).

As an additional note, the `CAST' operation you describe below, can't
do exactly what you expect, because it's runtime semantics depends on
how you instantiate `B'.  But that would mean that you'd have to
generate code for the `CAST' without knowing what `B' is.  Typed
Racket, like ML or Haskell, doesn't pass type parameters around as
values, so you can't do this.

> Module2
> #lang typed/racket
> (struct: (A) T ([value : A]))
> (require/typed "untyped-wrap.rkt"
>                [untyped-wrap (Procedure Any -> (T Any))])
> (: wrap (All (A B) ((A -> (T B)) A -> (T B))))
> (define (wrap fun value)
>   [CAST (untyped-wrap fun value) (T B)])
> (: f (Any -> (T One)))
> (define (f x) (T 1))

sam th
samth at ccs.neu.edu

Posted on the users mailing list.