[racket] Typed Racket vs. Haskell

On Sep 20, 2012, at 2:41 AM, thorsopia at lavabit.com wrote:

> Is it possible not to remove types?
> Vincent told me that one can "mix typed and untyped code" in Racket.
> How it's done in Racket (the implementation details)? How these modules interact? Could you give me some pointers?

1. Typed Racket programs do not rely on their types for semantics. Types are syntactic entities (as they should be) and they do not play a role for the execution of completely typed TR programs. 

2. You can turn type checking off for TR programs, and then types are just comments. [I do not know whether their syntax is checked.] 

3. You can also remove type annotations quite easily and get a Racket program out of it. 

[**] A TR module can call functions from an R module and vice versa. The key to our work is that this mutual calling mechanism is TYPE-SAFE (meaning we proved a type soundness theorem for the mix, and if you find a program that crashes, it is a bug in our implementation. In the limit, we will eliminate all such bugs.) -- The mechanism for accomplishing type safety is to translate types (which are merely syntax) into run-time assertions. The latter ensure that when an R module calls an (Int -> Int) function from an R module, the argument is an integer. Or when it is an ((Int -> Int) -> String) function, it checks that the argument is an (Int -> Int) function. This part is quite novel and based on reasonably recent research. 


> Why it's not possible in other Lisp-like languages (e.g. Guile)?

All of the above is possible in all other Lisp-like languages, e.g., Guile, Python, Perl, Clojure to name a few. 

It will take some work to reach the soundness level explained in [**]. For example, Common Lisp has the first three properties [1-3], it doesn't have [**]. At this point I am not aware of any Lisp-y language that accomplishes [1-3] + [**].