As part of my work on gradual typing for Typed Clojure, I used a different approach than Typed Racket in importing and exporting top-level defines. It was initially by necessity, as Clojure namespaces are much simpler than Racket modules, but we discovered it was now possible to export macros defined in typed modules (unlike Typed Racket).

This work (and the ambition to add gradual typing to Typed Clojure) was eventually abandoned and was never merged into core.typed–perhaps a subject of a different blog post.

Typed Racket cannot export macros. This is because unsafe variables can escape via the macroexpansion of typed macros into untyped land and wreak havoc. Typed Racket always emits unsafe variables and adds contracts as needed — Typed Clojure does the opposite, and can export macros safely.

The drawback: all bindings must be able to generate contracts.

The Problem

Take the following Typed Racket program that defines a one argument function f that increments a number.

(define (f [x : Number])
  (add1 x))

Typed Racket type checks invocations of f when they occur in typed contexts.

(f 1)  ;> 1 : Number
(f 'a) ;> Type Checker: type mismatch
       ;  expected: Number
       ;  given: 'a

We can write macros that expand to usages of f. Typed Racket only checks the full expansion of macros.

(define-syntax (m stx)
  #'(f 'a))

(m) ;> Type Checker: type mismatch
    ;  expected: Number
    ;  given: 'a

Exporting such macros is disallowed in Typed Racket. Since the macroexpansion of m contains an unsafe reference to f, using this macro in untyped contexts can freely violate any invariants assumed by typed code.

A Solution: Typed Clojure

Typed Clojure takes a different approach. Let’s try the previous exercise in Typed Clojure. We define a function f that increments its argument.

(defn f [x :- Number]
  (inc x))

Typed Clojure then splits this definition into two parts: an unsafe definition f', which simply renames the original variable, and a safe definition f, which wraps the unsafe version in a cast based on the static type inferred for f'.

(defn f' [x :- Number]
  (inc x))
(def f (cast [Number -> Number] f'))

Calling f in typed code will rewrite it to the unsafe version.

(f 1) ; rewrites to (f' 1)
;=> 2 :- Number

(f 'a) ;rewrites to (f' 'a)
;  Type error, Expected Number found Symbol: 'a

Here’s the key idea: referring to f in a macro defaults to the safe binding f. Expansions in untyped contexts refer to f; expansion typed contexts are rewritten, and refer to f'. The type system rewrites post-expansion, since Typed Clojure operates on fully expanded code.

(defmacro m []
  (let [a 'a]
    `(f '~a)))

(m) ; expands:  (f 'a)
    ; rewrites: (f' 'a)
    ;  Type error, Expected Number found Symbol: 'a

Due to the normal expansion containing only occurrences of safe bindings, we can freely export this macro and be sure typed invariants are preserved.

Drawbacks

The approach we took in Typed Clojure has its drawbacks. Most pressingly, we must generate contracts for every top level form in advance. For sufficiently complicated types, this is simply not possible. Several solutions are possible. We might selectively disable contract generation on variables, but this exposes unsafe bindings in the same way Typed Racket avoids by disabling macro exports. We could provide users with the ability to assign their own contracts or types that are “good enough” for their purposes. We could also use a less strict contract system when we cast values in safe definitions.

Conclusion: Is this approach general?

Yes, but with the same drawbacks here: all typed bindings must be capable of generating contracts based on their types. It would be interesting to try this approach in Typed Racket and see how programs still type check — or even how many new programs can be written using macro exports.