[racket] Typed Racket vs. Haskell

At Thu, 20 Sep 2012 02:41:02 -0400 (EDT),
thorsopia at lavabit.com wrote:
> > The required "translation" step will be mostly
> > removing the type declarations.  Doing the same with Haskell etc would
> > most likely be much harder.
> 
> Is it possible not to remove types?

Yes. A Typed Racket is a Racket program, so Racket can run it just fine.

What Eli was saying is that if you want to port it to, say, Guile, part
of the work will be removing the types, and part of it will be porting
the resulting Racket program to Guile.

> Vincent told me that one can "mix typed and untyped code" in Racket.

Here's a simple example:

    ;; in file typed.rkt
    #lang typed/racket
    (provide louder)
    (: louder : String -> String)
    (define (louder s) (string-append s "!"))

    ;; in file untyped.rkt
    #lang racket
    (require "typed.rkt")
    (displayln (louder "I can call typed code"))

The first module is written in Typed Racket, and the second in untyped
Racket. If you run "untyped.rkt", it prints "I can call typed code!", as
expected.

You can also require untyped code from typed code using `require/typed'.

> How it's done in Racket (the implementation details)? How these modules
> interact? Could you give me some pointers?

Typed Racket modules compile to Racket modules, which interact with
other Racket modules via the module system. To make sure that typed
functions don't get invalid inputs from untyped code, the Racket
contract system checks everything that goes from untyped to typed code.

For example, if the untyped module above tried to do

    (louder 3)

this would raise an error, since `louder' only accepts strings.

For more details about how contracts are used for typed-untyped
interaction, you can read
    http://www.ccs.neu.edu/racket/pubs/dls06-tf.pdf

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

Typed Racket relies on several important pieces of infrastructure that
Racket provides: the module system, the contract system, and Racket's
language extension facilities (including, but not limited to the macro
system), among others.

For more information about how the Typed Racket implementation uses
these mechanisms, you can read
    http://www.ccs.neu.edu/racket/pubs/pldi11-thacff.pdf

Other systems that provide similar infrastructure could build their own
Typed Racket-like systems, too. Typed Clojure and Typed Ironscheme are
two such projects. IIUC, Guile has most of the necessary puzzle pieces,
too. But even with the necessary infrastructure, building such a system
remains a large engineering undertaking.

Vincent