[racket] Typed Racket procedure wrapping?

From: Asumu Takikawa (asumu at ccs.neu.edu)
Date: Tue Feb 5 16:17:14 EST 2013

On 2013-02-05 16:06:11 -0500, Joe Gibbs Politz wrote:
>    This worked in 5.3.1:
>
>    typed.rkt
>    =======
>    #lang typed/racket
>
>    (provide wrap)
>
>    (define: (wrap (p : Procedure)) : Procedure
>      (λ (_) p))
>
>    untyped.rkt
>    ===========
>    #lang racket
>
>    (require "typed.rkt")
>    (define f (λ (n) n))
>
>    ((wrap f) 5) ;; returns f itself; f is eq? to ((wrap f) 5)

It turns out that allowing values of `Procedure` type escape into
untyped code is unsound. In particular, you could use `wrap` to "cast"
any typed procedure into one that doesn't get protected when exported to
untyped code.

>    In 5.3.2, when running untyped.rkt, I get:
>
>    #<case-lambda-procedure>: arity mismatch;
>     the expected number of arguments does not match the given number
>      given: 1
>      arguments...:
>       5

I agree that this error message is bad. It's a result of changing the
type `Procedure` to use the contract `(case->)`. Maybe we should use a
custom contract here instead that produces a better error message.

Cheers,
Asumu

Posted on the users mailing list.