PLAI Typed Language

The plai-typed language is a statically typed language that resembles the plai language, though with a smaller set of syntactic forms and built-in functions.

The body of a plai-typed module is a sequence of definitions and expressions. Like the plai languages the module exports all top-level definitions. When a plai-typed module is imported into a module that does not use plai-typed, the imports have contracts (matching reflecting the exported bindings’ types).

1 Definitions

In a define-type declaration, the contract/predicate position for variant fields changes to a colon followed by a type. In addition, define and lambda forms support type annotations on arguments and for results. The syntax is otherwise merely restricted from the normal PLAI language.

When a module-path is not wrapped with typed-in or opaque-type-in, then module-path must refer to a module that is implemented with plai-typed.

When module-path is wrapped with typed-in, then only the specified ids are imported from module-path, and the type system assumes (without static or additional dynamic checks) the given type for each id.

When module-path is wrapped with opaque-type-in, then the corresponding type-ids are bound as opaque datatypes, where predicate-id from module-path is a run-time predicate (used for contracts as needed for cooperation with untyped code) for instances of the datatype.

(module sub plai-typed

(define n 8))

(require 'sub)

(+ n 1)

(module+ test

(test 11 (add-one 10)))

(define (add-one n)

(+ 1 n))

A macro of the form

(define-syntax-rule (id pattern ...) template)

is equivalent to

(define-syntax id

(syntax-rules ()

[(id pattern ...) template]))

2 Expressions

An expression can be a literal constant that is a number (type number), a string (type string), a symbol (type symbol) written with quote or ', an S-expression (type s-expression) also written with quote or ', #t (type boolean), #f (type boolean), or a character (type char). An expression also can be a bound identifier (in which case its type comes from its binding).

The dispatching mode, symbol or number, is inferred from the id-or-numbers, which must all be symbols or numbers for a given use of case. If no clause provides a number or symbol, then symbol dispatch is inferred.

The type of each elem is independent.

The s-exp-symbol? function determines whether an S-expression is a symbol; in that case, s-exp->symbol acts the identity function to produce the symbol, otherwise an exception is raised. The symbol->s-exp function similarly acts as the identity function to view a symbol as an S-expression.

The other functions work similarly for numbers, strings, booleans, and lists of S-expressions.

See also module+.

3 Types

The void identifier also works as an expression of type (-> void).

4 Syntactic Literals

5 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.

6 Untyped with Typed Syntax

The define-syntax, define-syntax-rule, module+, and require forms from plai-typed/untyped are the bindings from racket/base instead of plai-typed.