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

I am willing to check the type and to strip the types from the source then. 

Meaning: 
 1. the programer gets only one kind of reassurance, namely, that the module's type specs are internally consistent 
 2. the generated untyped file is like any other untyped module in the code base. 





On Dec 20, 2012, at 10:48 AM, Sam Tobin-Hochstadt wrote:

> 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