Understanding Computation (57 page)

These questions lead us to make some design decisions about what should be considered
valid
Simple
programs. For example, is «
x = 1; y = 2; x = x < y
» okay? It’s certainly fine according
to the dynamic semantics—nothing bad happens when it’s executed—but we might (or might not!)
be uncomfortable with allowing programs where the variables change from holding one type of
value to another during execution. That kind of flexibility might be valuable to some
programmers, but for others, it could act as a source of accidental errors.

From the perspective of someone designing the static semantics, it’s also more difficult
to handle a language where variables can change their types. At the moment, we’re assuming
that the type context arrives from some external source and remains unchanged throughout the
program, but we could opt for a more sophisticated system where the context is empty at the
beginning of the program and gradually builds up as variables are declared or assigned, in
the same way that the dynamic semantics gradually builds up the value environment as the
program executes. But this gets complicated: if statements could modify the type context,
then we’d need the
#type
method to return both a type and
a context, in the same way that the dynamic semantics’
#reduce
method returns a reduced program and an environment, so that an earlier
statement can pass an updated context to a later one. We’d also have to deal with situations
like «
if (b) { x = 1 } else { y = 2 }
» where different
execution paths produce different type contexts, as well as ones like «
if (b) { x = 1 } else { x = true }
» where those different
contexts actively contradict each other.
^[
89
]

Fundamentally, there is a tension between the restrictiveness of a type system and the
expressiveness of the programs we can write within it. A restrictive type system can be
good, because it provides strong guarantees that rule out lots of possible errors, but it’s
bad when it prevents us from writing the programs we want to write. A good type system finds
an acceptable compromise between restrictiveness and expressiveness, ruling out enough
problems to be worthwhile without getting in the way, while being simple enough for
programmers to understand.

We’ll resolve this tension by sticking with the uncomplicated idea
of a type context that’s provided by something outside the program
itself and doesn’t get updated by individual statements. This does rule
out certain kinds of program, and definitely avoids the problem of how
and where this type context originates, but it keeps the static
semantics simple and gives us a rule we can easily work with.

For assignment statements, then, let’s say that the type of the
expression should match the type of the variable to which its value is
being assigned:

class
Assign
def
type
(
context
)
if
context
[
name
]
==
expression
.
type
(
context
)
Type
::
VOID
end
end
end

This rule is good enough for all programs where we can decide the
type of each variable upfront and have it stay the same, which is a
tolerable constraint. For example, we can check the
While
loop whose dynamic semantics we
implemented in
Chapter 2
:

>>
statement
=
While
.
new
(
LessThan
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
5
)),
Assign
.
new
(
:x
,
Add
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
3
)))
)
=> «while (x < 5) { x = x + 3 }»
>>
statement
.
type
({})
=> nil
>>
statement
.
type
({
x
:
Type
::
NUMBER
})
=> #
>>
statement
.
type
({
x
:
Type
::
BOOLEAN
})
=> nil

The type system
we’ve built can prevent basic errors. By running a toy
version of a program according to these static semantics, we can find
out what types of value can appear at each point in the original
program, and check that these types match up correctly with what the
dynamic semantics is going to try to do when we run it. The simplicity
of this toy interpretation means that we get only limited information
about what might happen when the program is evaluated, but it also means
that we can do our checking easily and without complications. For
example, we can check a program that runs forever:

>>
statement
=
Sequence
.
new
(
Assign
.
new
(
:x
,
Number
.
new
(
0
)),
While
.
new
(
Boolean
.
new
(
true
),
Assign
.
new
(
:x
,
Add
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
1
)))
)
)
=> «x = 0; while (true) { x = x + 1 }»
>>
statement
.
type
({
x
:
Type
::
NUMBER
})
=> #
>>
statement
.
evaluate
({})
SystemStackError: stack level too deep

That program is definitely stupid, but it doesn’t contain any type errors: the loop
condition is a Boolean, and the variable
x
is
consistently used to store a number. Of course, the type system isn’t clever enough to tell
us whether a program is doing what we meant it to do, or even doing anything useful at all,
only whether its parts match up in the right way. And because it needs to be safe, just like
our
Sign
abstraction, it will sometimes give us an overly
pessimistic answer about whether a program contains any errors. We can see this if we extend
the above program with an extra statement:

>>
statement
=
Sequence
.
new
(
statement
,
Assign
.
new
(
:x
,
Boolean
.
new
(
true
)))
=> «x = 0; while (true) { x = x + 1 }; x = true»
>>
statement
.
type
({
x
:
Type
::
NUMBER
})
=> nil

The
#type
method returns
nil
to indicate an error because there’s a statement that assigns a Boolean
value to
x
, but there’s no way this could actually cause
a problem at runtime, because this statement will never get executed. Our type system isn’t
clever enough to spot this, but it gives us a safe answer, “this program
might
go wrong,” which is overly cautious but not incorrect.
Something in the program tries to assign a Boolean value to a numeric variable, so part of
it has the potential to go wrong, but
for other reasons
it never
actually will.

It’s not just infinite loops that cause problems. The dynamic
semantics has no problem with a program like this:

>>
statement
=
Sequence
.
new
(
If
.
new
(
Variable
.
new
(
:b
),
Assign
.
new
(
:x
,
Number
.
new
(
6
)),
Assign
.
new
(
:x
,
Boolean
.
new
(
true
))
),
Sequence
.
new
(
If
.
new
(
Variable
.
new
(
:b
),
Assign
.
new
(
:y
,
Variable
.
new
(
:x
)),
Assign
.
new
(
:y
,
Number
.
new
(
1
))
),
Assign
.
new
(
:z
,
Add
.
new
(
Variable
.
new
(
:y
),
Number
.
new
(
1
)))
)
)
=> «if (b) { x = 6 } else { x = true }; if (b) { y = x } else { y = 1 }; z = y + 1»
>>
statement
.
evaluate
({
b
:
Boolean
.
new
(
true
)
})
=> {:b=>«true», :x=>«6», :y=>«6», :z=>«7»}
>>
statement
.
evaluate
({
b
:
Boolean
.
new
(
false
)
})
=> {:b=>«false», :x=>«true», :y=>«1», :z=>«2»}

The variable
x
is used to store a number or a Boolean
depending on whether
b
is true or false, which is never a
problem during evaluation, because the program consistently uses either one or the other;
there’s no possible execution path where
x
is treated as
both a number and a Boolean. But the abstract values used by the static semantics don’t have
enough detail to be able to show that this is okay,
^[
90
]
so the safe approximation is to always say “this program might go wrong”:

>>
statement
.
type
({})
=> nil
>>
context
=
{
b
:
Type
::
BOOLEAN
,
y
:
Type
::
NUMBER
,
z
:
Type
::
NUMBER
}
=> {:b=>#, :y=>#, :z=>#}
>>
statement
.
type
(
context
)
=> nil
>>
statement
.
type
(
context
.
merge
({
x
:
Type
::
NUMBER
}))
=> nil
>>
statement
.
type
(
context
.
merge
({
x
:
Type
::
BOOLEAN
}))
=> nil

This system is focused on programs going wrong in a specific way: the dynamic semantics
of each piece of syntax has certain expectations about what types of values it will be
handling, and the type system checks those expectations to make sure that a number won’t
show up where a Boolean is expected and vice versa. But there are other ways for a program
to go wrong, and this static semantics doesn’t check for them. For example, the type system
pays no attention to whether a variable has actually been given a value before it’s used, so
any program containing uninitialized variables will pass the type checker and still fail
during evaluation:

>>
statement
=
Assign
.
new
(
:x
,
Add
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
1
)))
=> «x = x + 1»
>>
statement
.
type
({
x
:
Type
::
NUMBER
})
=> #
>>
statement
.
evaluate
({})
NoMethodError: undefined method `value' for nil:NilClass

Any information we get from the type system has to be taken with a
pinch of salt, and we have to pay attention to its limitations when
deciding how much faith to put in it. A successful execution of a
program’s static semantics doesn’t mean “this program will definitely
work,” only “this program definitely won’t fail in a particular way.” It
would be great to have an automated system that can tell us that a
program is free of any conceivable kind of bug or error, but as we saw
in
Chapter 8
, the universe just isn’t that
convenient.