7 Type Checking and Inference
Type checking and inference is just as in ML (Hindley-Milner), with a few small exceptions:
Functions can take multiple arguments, instead of requring a tuple of arguments. Thus, (Number Number -> Number) is a different type than either ((Number * Number) -> Number), which is the tuple variant, or (Number -> (Number -> Number)), which is the curried variant.
Since all top-level definitions are in the same mutually-recursive scope, the type of a definition’s right-hand side is not directly unified with references to the defined identifier on the right-hand side. Instead, every reference to an identifier—
even a reference in the identifier’s definition— is unified with a instantiation of a polymorphic type inferred for the definition. Compare OCaml:
# let rec f = fun x -> x
and h = fun y -> f 0
and g = fun z -> f "x";;
This expression has type string but is here used with type int
with
(define (f x) x)
(define (h y) (f 0))
(define (g y) (f "x"))
; f : ('a -> 'a)
; h : ('a -> Number)
; g : ('a -> String)
A minor consequence is that polymorphic recursion (i.e., a self call with an argument whose type is different than that for the current call) is allowed. Recursive types, however, are prohibited. Polymorphic recursion is not decidable, so see #:fuel in Untyped, Lazy, and Fuel Modes.
The usual value restriction applies for inferring polymorphic types, where expression matching the following grammar (before macro expansion, unfortunately) are considered values:
value-expr = (lambda (id/ty ...) expr) | (lambda (id/ty ...) : type expr) | (values value-expr ...) | (list value-expr ...) | empty | (cons value-expr value-expr) | (hash value-expr ...) | (variant-id value ...) | 'datum | id | string | character | number | boolean where variant-id is none, some, or a constructor bound by define-type.
Variables are mutable when set! is used, but assignment via set! is disallowed on a variable after a polymorphic type has been inferred for it (e.g., in an interaction after type checking is complete).
Since all definitions are recursively bound, and since the right-hand side of a definition does not have to be a function, its possible to refer to a variable before it is defined. The type system does not prevent “reference to identifier before definition” errors.
Interactive evaluation (e.g., in DrRacket’s interactions window) can redefine identifiers that were previously defined interactively or that were defined in a module as mutable. Redefinition cannot change the identifier’s type. Due to a limitation of the type checker, identifiers of polymorphic type cannot be redefined or redeclared. Type declarations are allowed in interactive evaluation, but a declared type is never treated as a polymorphic type.
When typechecking fails, the error messages reports and highlights (in pink) all of the expressions whose type contributed to the failure. That’s often too much information. As usual, explicit type annotations can help focus the error message.