5 Types
syntax
(type ... -> type)
syntax
(type * ...+)
syntax
()
syntax
(Listof type)
syntax
(Boxof type)
syntax
(Vectorof type)
syntax
(Parameterof type)
syntax
(Hashof type type)
syntax
(Optionof type)
(define-type (Optionof 'a) (none) (some [v : 'a]))
syntax
'id
In the following example, the type checker determines that 'a must be replaced with Number:
> (define one : 'a 1) > one - Number
1
In the following example, the type checker determines that 'b stands for the argument type of a polymorphic function:
> (define (f [x : 'b]) x)
In the following examples, the type checker is unable to replace 'a consistently with the same type everywhere:
> (if (has-type #t : 'a) (has-type 1 : 'a) 2) eval:240:0: typecheck failed: Number vs. Boolean
sources:
1
#t
a
> (define x : 'a (list (has-type 1 : 'a))) eval:241:0: typecheck failed: Number vs. (Listof Number)
sources:
(list (has-type 1 : (quote a)))
Multiple uses of the same type variable (i.e., with the same id) are constrained to refer to the same type only when the uses have the same scope. A type variable’s scope is determined as follows:
When a type variable is encountered in a left-to-right parsing of a program and no same-named variable is already in scope, then the variable’s scope is set to the nearest enclosing define form, define-type form, lambda form, let right-hand side, letrec right-hand side, or let* right-hand side.
When a type variable is encountered in a left-to-right parsing of a program and some same-named variable is already in scope, the variable have the same scope (and are confined to have the same meaning).
For example, type variables introduced in separate definitions are always distinct, so in the following example, the first 'a can stand for Number while the second stands for String:
> (define one : 'a 1) > (define two : 'a "two")
A type variable used for a lambda argument is scoped to the entire lambda form, so the uses of 'a in the definitions of the following example refer back to that argument type, and the argument cannot have both Number and String type:
> (lambda ([x : 'a]) (local [(define one : 'a 1) (define two : 'a "two")] #f)) eval:244:0: typecheck failed: Number vs. String
sources:
"two"
1
a
Beware that the order of expressions can affect the scope of type variables within the expressions:
> (values (has-type 1 : 'a) (letrec ([f (lambda ([x : 'a]) x)]) f)) - (Number * (Number -> Number))
(values 1 #<procedure:f>)
> (values (letrec ([f (lambda ([x : 'a]) x)]) f) (has-type 1 : 'a)) - (('_a -> '_a) * Number)
(values #<procedure:f> 1)