Understanding Computation (56 page)

This is a more general version of the earlier trick with addition,
multiplication, and
Sign
. Even though
we’re not doing any actual addition or comparison of numbers, the static
semantics gives us an alternative way of “executing” the program that
still returns a useful result.

Instead of interpreting the expression «
1 + 2
» as a
program about
values
, we’re throwing away some detail and interpreting
it as a program about
types
, and the static semantics provides the
alternative interpretations of «
1
», «
2
», and «
+
», which let us run
this program-about-types to see what its result is. That result is less specific—more
abstract—than the one we’d get by running the program normally according to the dynamic
semantics, but it’s nonetheless a useful result, because we have a way of translating it
into something meaningful in the concrete world:
Type::NUMBER
means “calling
#evaluate
on
this expression will return a
Number
,” and
nil
means “calling
#evaluate
may cause an error.”

We almost have the complete static semantics of
Simple
expressions now, but we haven’t looked
at variables. What should
Variable#type
return? It depends what value
the variable contains: in a program like «
x =
5; y = x + 1
» the variable
y
has the type
Type::NUMBER
, but in «
x = 5; y = x < 1
» it has the type
Type::BOOLEAN
. How can we handle this?

We saw in
Small-Step Semantics
that the dynamic
semantics of
Variable
uses an
environment hash to map variable names onto their values, and the static
semantics needs something similar: a mapping from variable names onto
types
. We could call this a “type environment,” but
let’s use the name
type context
to avoid getting
the two kinds of environment mixed up. If we pass a type context into
Variable#type
, all it has to do is
look up that variable in the context:

class
Variable
def
type
(
context
)
context
[
name
]
end
end

Now that
#type
expects a
context
argument, we need to go back
and revise the other implementations of
#type
to accept a type context:

class
Number
def
type
(
context
)
Type
::
NUMBER
end
end
class
Boolean
def
type
(
context
)
Type
::
BOOLEAN
end
end
class
Add
def
type
(
context
)
if
left
.
type
(
context
)
==
Type
::
NUMBER
&&
right
.
type
(
context
)
==
Type
::
NUMBER
Type
::
NUMBER
end
end
end
class
LessThan
def
type
(
context
)
if
left
.
type
(
context
)
==
Type
::
NUMBER
&&
right
.
type
(
context
)
==
Type
::
NUMBER
Type
::
BOOLEAN
end
end
end

This lets us ask for the type of expressions that involve
variables, as long as we provide a context that gives them the right
types:

>>
expression
=
Add
.
new
(
Variable
.
new
(
:x
),
Variable
.
new
(
:y
))
=> «x + y»
>>
expression
.
type
({})
=> nil
>>
expression
.
type
({
x
:
Type
::
NUMBER
,
y
:
Type
::
NUMBER
})
=> #
>>
expression
.
type
({
x
:
Type
::
NUMBER
,
y
:
Type
::
BOOLEAN
})
=> nil

That gives us implementations of
#type
for all forms of expression syntax, so
what about statements? Evaluating a
Simple
statement returns an environment, not a
value, so how do we express that in the static semantics?

The easiest way to handle statements is to treat them as a kind of
inert expression: assume that they don’t return a value (which is true)
and ignore the effect they have on the environment. We can come up with
a new type that means “doesn’t return a value” and associate that type
with any statement as long as all its subparts have the right types.
Let’s give this new type the name
Type::VOID
:

class
Type
VOID
=
new
(
:void
)
end

Implementations of
#type
for
DoNothing
and
Sequence
are easy. Evaluation of
DoNothing
will always succeed, and evaluation
of
Sequence
will succeed as long as
the statements it’s connecting don’t have anything wrong with
them:

class
DoNothing
def
type
(
context
)
Type
::
VOID
end
end
class
Sequence
def
type
(
context
)
if
first
.
type
(
context
)
==
Type
::
VOID
&&
second
.
type
(
context
)
==
Type
::
VOID
Type
::
VOID
end
end
end

If
and
While
are
slightly more discerning. They both contain an expression that acts as a condition, and for
the program to work properly, the condition has to evaluate to a Boolean:

class
If
def
type
(
context
)
if
condition
.
type
(
context
)
==
Type
::
BOOLEAN
&&
consequence
.
type
(
context
)
==
Type
::
VOID
&&
alternative
.
type
(
context
)
==
Type
::
VOID
Type
::
VOID
end
end
end
class
While
def
type
(
context
)
if
condition
.
type
(
context
)
==
Type
::
BOOLEAN
&&
body
.
type
(
context
)
==
Type
::
VOID
Type
::
VOID
end
end
end

This lets us distinguish between a statement that will go wrong
during evaluation and one that won’t:

>>
If
.
new
(
LessThan
.
new
(
Number
.
new
(
1
),
Number
.
new
(
2
)),
DoNothing
.
new
,
DoNothing
.
new
)
.
type
({})
=> #
>>
If
.
new
(
Add
.
new
(
Number
.
new
(
1
),
Number
.
new
(
2
)),
DoNothing
.
new
,
DoNothing
.
new
)
.
type
({})
=> nil
>>
While
.
new
(
Variable
.
new
(
:x
),
DoNothing
.
new
)
.
type
({
x
:
Type
::
BOOLEAN
})
=> #
>>
While
.
new
(
Variable
.
new
(
:x
),
DoNothing
.
new
)
.
type
({
x
:
Type
::
NUMBER
})
=> nil

The only method left to implement is
Assign#type
. We
know it should return
Type::VOID
, but under what
circumstances? How do we decide if an assignment is well-behaved or not? We’ll want to check
that the expression on the righthand side of the assignment is sensible according to the
static semantics, but do we care what type it is?