274 lines
11 KiB
TeX
274 lines
11 KiB
TeX
\begin{schemeregion}
|
|
\section{Typing Terms}
|
|
\label{sect:type-one}
|
|
|
|
The implementation of Typed Scheme illustrates like no other language
|
|
design experiment the power of PLT Scheme's macro system. In this
|
|
section, we explain the process for type-checking a single definition
|
|
or expression, with a focus on type annotations and the use of type
|
|
environments. The following section extends the implementation to
|
|
handle modules.
|
|
|
|
Typed Scheme is designed to interoperate with PLT Scheme's existing
|
|
macro and module systems. In particular, typed programs should be able
|
|
to use existing macros (provided they produce typecheckable code) and
|
|
define and use new macros. Since it is generally impossible to derive
|
|
type rules for arbitrary macros, the type-checker must analyze the
|
|
program after expansion has eliminated all occurrences of macros and
|
|
reduced the program to core syntax. This is also the strategy adopted
|
|
by the ACL2 theorem prover for Common Lisp~\cite{acl2-book}.
|
|
|
|
\begin{figure}
|
|
\begin{schemedisplay}
|
|
langs ;; typed-scheme
|
|
(provide (rename-out top-interaction HPtop-interaction))
|
|
(define-syntax (top-interaction stx)
|
|
(syntax-case stx ()
|
|
[(top-interaction . term)
|
|
(let ([expanded-term
|
|
(local-expand #'term 'top-level null)])
|
|
(type-check-top-level expanded-term)
|
|
expanded-term)]))
|
|
ELIDED
|
|
\end{schemedisplay}
|
|
\caption{\variablefont{typed-scheme} module}
|
|
\label{fig:first-typed-scheme-module}
|
|
\end{figure}
|
|
|
|
The type-checker hooks into the compilation process as a macro using
|
|
the \scheme{HPtop-interaction} interface described in
|
|
section~\ref{sect:syntax:hooks}. The type-checking macro receives the
|
|
original unexpanded program, and it calls \scheme{local-expand} to
|
|
fully expand the program for analysis. The type-checker then either
|
|
approves the expanded program or raises an error, aborting
|
|
compilation. Figure~\ref{fig:first-typed-scheme-module}
|
|
shows the beginning of the \scheme{typed-scheme} language module.
|
|
|
|
The type-checker has rules for each primitive syntactic form. It knows
|
|
how to assign types to Scheme constants. It also knows the types of
|
|
the Scheme primitive operators.
|
|
%
|
|
When it encounters a programmer-introduced variable, however, it needs
|
|
to find the type of the variable, and although that information is
|
|
present in the original program, type information is not part of fully
|
|
expanded, core Scheme code.
|
|
%
|
|
The rest of this section discusses the treatment of variable types and
|
|
the communication between Typed Scheme's binding forms and its
|
|
type-checker across macro expansion.
|
|
|
|
\subsection{Variables}
|
|
|
|
Typed Scheme requires type annotations on binding occurrences of
|
|
many variables;
|
|
type-checking depends on that information. Consequently, the typed
|
|
binding forms and the type-checker employ a protocol regarding the
|
|
communication of variable types.
|
|
|
|
Type annotations are local to the terms where they appear. They must
|
|
be robust in the face of local expansion and re-expansion. Since the
|
|
type-checker works on the fully-expanded program, it makes sense to
|
|
put the type annotations into the program.
|
|
%
|
|
At the same time, the result of expansion is a core Scheme term, and
|
|
Scheme's primitive syntactic forms are unaware of types and do not
|
|
accept Typed Scheme's typed binding syntax. Syntax properties provide
|
|
an appropriate method for implementing the protocol by attaching type
|
|
information to terms.\footnote{\citet{ch:ultimate-label} present an
|
|
alternative method for communicating this information through phases
|
|
of a compiler.}
|
|
|
|
\begin{quotation}\noindent
|
|
\textbf{The Variable Protocol:} Every typed binding form decorates its
|
|
declared variables with a type attached to the \scheme{'type-label}
|
|
syntax property of the bound identifiers.
|
|
\end{quotation}
|
|
|
|
Typed Scheme implements the variable protocol by defining typed
|
|
binding forms such as \scheme{lambda:} as macros that convert the
|
|
\scheme{[variable : type]} variable syntax into primitive binding
|
|
forms with the types attached to the \scheme{'type-label} syntax
|
|
property of the variable names.
|
|
%
|
|
Figure~\ref{fig:typed-binding-forms} shows the definition of typed
|
|
binding macros. The \scheme{lambda:} macro expands into the primitive
|
|
\scheme{lambda} form. For each formal parameter name, it creates a new syntax
|
|
object with a \scheme{'type-label} property holding the type.
|
|
%
|
|
Likewise, the \scheme{define:} macro handles typed definitions. The
|
|
first clause handles the simple case with just a name being bound to a
|
|
value. The second clause handles the function definition syntax by
|
|
desugaring it to a \scheme{define:} form with an explicit
|
|
\scheme{lambda:} form. It also synthesizes the function type from the
|
|
argument types and the result type, adding it to the expanded
|
|
definition.
|
|
%
|
|
The \scheme|:| annotation form, used chapter~\ref{chap:overview},
|
|
works similarly to \scheme|define:|. In this section, we focus on
|
|
\scheme|define:| for simplicity.
|
|
|
|
\begin{figure}
|
|
\begin{schemedisplay}
|
|
(define-syntax (lambda: stx)
|
|
(syntax-case stx (:)
|
|
[(lambda: ([formal : formal-type] ...) . body)
|
|
(with-syntax ([(typed-formal ...)
|
|
(map
|
|
(lambda (id type)
|
|
(syntax-property id 'type-label type))
|
|
(syntax->list #'(formal ...))
|
|
(syntax->list #'(formal-type ...)))])
|
|
#'(lambda (typed-formal ...) . body))]))
|
|
|
|
(define-syntax (define: stx)
|
|
(syntax-case stx (:)
|
|
[(define: var : type expr)
|
|
(identifier? #'var)
|
|
(with-syntax ([tvar (syntax-property #'var 'type-label #'type)])
|
|
#`(define #,tvar expr))]
|
|
[(define: (f [formal formal-type] ...) : result-type . body)
|
|
#'(define: f : (formal-type ... -> result-type)
|
|
(lambda: ([formal formal-type] ...) . body)))])
|
|
\end{schemedisplay}
|
|
\caption{Typed definition and binding forms}
|
|
\label{fig:typed-binding-forms}
|
|
\end{figure}
|
|
|
|
The type-checker, at the other end of the protocol, consumes the
|
|
syntax properties produced by the typed binding forms. When the
|
|
type-checker encounters a binding form, it scans the bound variables
|
|
and extracts their types with the \scheme{get-id-type} procedure:
|
|
\begin{schemedisplay}
|
|
;; get-id-type : identifier $\rightarrow$ type
|
|
(define-for-syntax (get-id-type id)
|
|
(let ([type (syntax-property id 'type-label)])
|
|
(unless type (raise-missing-type-error id))
|
|
type))
|
|
\end{schemedisplay}
|
|
|
|
The type-checker maintains a two-part type-environment. One part holds
|
|
the types of global variables, including variables defined via
|
|
\scheme{define:} and all primitive variables. The other part holds the
|
|
lexical variables, such as those bound by \scheme{lambda:} and other
|
|
local binding forms. Figure~\ref{fig:type-env} shows the outline of the
|
|
environment module. The \scheme{declare-type!} operation updates the
|
|
global type environment; \scheme{extend-env} extends the local type
|
|
environment; and \scheme{lookup-env} finds the type of an identifier,
|
|
searching first the local bindings then the global bindings.
|
|
|
|
|
|
\begin{figure}
|
|
\begin{schemedisplay}
|
|
langs ;; env
|
|
(provide (all-defined-out))
|
|
|
|
;; An environment is a (list-of binding).
|
|
|
|
;; A binding is (make-binding identifier type).
|
|
(define-struct binding (id type))
|
|
|
|
;; the-type-env : environment
|
|
;; Associates global variables with their types.
|
|
;; Initially contains types for the scheme primitives.
|
|
(define the-type-env ELIDED)
|
|
|
|
;; declare-type : identifier type $\rightarrow$ void
|
|
;; Add a type association to the global type environment.
|
|
(define (declare-type! id type) ELIDED)
|
|
|
|
;; empty-env : environment
|
|
;; The empty lexical environment.
|
|
(define empty-env null)
|
|
|
|
;; extend-env : environment (list-of binding) $\rightarrow$ environment
|
|
(define (extend-env env bindings) ELIDED)
|
|
|
|
;; lookup-type : lexical-env identifier $\rightarrow$ type
|
|
;; Searches the lexical environment, then the global environment.
|
|
(define (lookup-type env var) ELIDED)
|
|
\end{schemedisplay}
|
|
\caption{Type Environment}
|
|
\label{fig:type-env}
|
|
\end{figure}
|
|
|
|
The type-checker consumes the information attached to bound
|
|
variables. Figure~\ref{fig:type-checker} lists the code for the
|
|
type-checker. When the type-checker encounters a definition, it
|
|
extracts the type annotations from the bound identifiers and extends
|
|
the type environment with the new type association. It finally checks
|
|
that the declared type matches the type computed for the right-hand
|
|
side expression. When the type-checker encounters an expression, it
|
|
switches to expression mode.
|
|
|
|
The \scheme{type-check-expr} procedure computes the type of the
|
|
expression.
|
|
%
|
|
\begin{figure}[h!]
|
|
\begin{schemedisplay}
|
|
;; type-check-top-level : syntax $\rightarrow$ void
|
|
(define-for-syntax (type-check-top-level form)
|
|
(syntax-case form (define)
|
|
[(define var expr)
|
|
(let* ([var-type (get-id-type #'var)])
|
|
(declare-type! #'var var-type)
|
|
(let ([expr-type (type-check-expr #'expr empty-env)])
|
|
(check-type var-type expr-type form)))]
|
|
[expr
|
|
(type-check-expr #'expr empty-env)]))
|
|
|
|
;; type-check-expr : syntax lexical-env $\rightarrow$ type
|
|
(define-for-syntax (type-check-expr expr env)
|
|
(syntax-case expr (lambda HPapp ELIDED)
|
|
[var
|
|
(identifier? #'var)
|
|
(lookup-type env #'var)]
|
|
[(lambda (formal ...) body)
|
|
(let* ([formal-types
|
|
(map get-id-type (syntax->list #'(formal ...)))]
|
|
[formal-bindings
|
|
(map make-binding
|
|
(syntax->list #'(formal ...))
|
|
formal-types)]
|
|
[body-type
|
|
(type-check-expr #'body
|
|
(extend-env env formal-bindings))])
|
|
(make-function-type formal-types body-type))]
|
|
[(HPapp op arg ...)
|
|
(let ([op-type (type-check-expr #'op env)]
|
|
[arg-types
|
|
(map (lambda (arg) (type-check-expr arg env))
|
|
(syntax->list #'(arg ...)))])
|
|
(check-function-type op-type #'op)
|
|
(check-types (function-type-params op-type)
|
|
op-types
|
|
expr)
|
|
(function-type-result op-type))]
|
|
ELIDED))
|
|
\end{schemedisplay}
|
|
|
|
{\small
|
|
These functions are defined using \scheme{define-for-syntax},
|
|
which creates a value binding in the compile-time environment, so
|
|
the \scheme{top-interaction} macro can use the procedures.}
|
|
|
|
\caption{The type-checker}
|
|
\label{fig:type-checker}
|
|
\end{figure}
|
|
%
|
|
In the simplest case, variable reference, the type-checker
|
|
just looks up the type in the type environment. If the variable is not
|
|
present, the \scheme{lookup-env} procedure raises an error.
|
|
%
|
|
When the type-checker sees a \scheme{lambda} form, it gathers the
|
|
types of the bound variables and extends the type environment before
|
|
checking the body in the extended environment. It also uses the types
|
|
of the formals, in addition to the computed type of the body, to
|
|
create the type of the function.
|
|
%
|
|
Finally, the application case involves finding the type of the
|
|
operator, verifying that it is a function type of the right arity, and
|
|
checking the expected parameter types against the actual parameter
|
|
types. If the application is valid, the result is the function's
|
|
result type.
|
|
\end{schemeregion}
|