[racket-dev] supplying typed and untyped entry points, take 2

On Mon, Dec 17, 2012 at 9:34 PM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
> Okay. I propose we figure out how to allow people programming in Typed Racket,
> and deploy two copies of the code without performance overhead for either T or U
> code.

I don't see how we can do this without violating the integrity of the
type system.  Consider the following module:

#lang typed/racket
(provide f)
(: f : (Pair String String) -> String)
(define (f x) (car x)

To use this from untyped code, we need a contract around `f`,
otherwise the application of `car` can fail.  If we allow the
application of `car` to fail, then our type system isn't telling us
what we thought about the behavior of this program.  One way in which
this manifests itself is that we couldn't optimize the version that's
called from untyped code.

We could do your idea of writing out a separate file that uses `#lang
typed/racket/no-check` with the contents of the file, but (a) we would
have tricky issues with requiring the appropriate one and (b) this
seems like it's just giving up on safe typed-untyped interoperation
because it's expensive.

Sam