### 6` `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.

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.

Type variables are always scoped locally within a type expression.

Compare OCaml:

# function (x : 'a), (y : 'a) -> x;;

- : 'a * 'a -> 'a = <fun>

with

> (lambda ((x : 'a) (y : 'a)) x)

- ('a 'b -> 'a)

> (define f : ('a 'a -> 'a) (lambda (x y) x))

> f

- ('a 'a -> 'a)

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.