Statements as Functions
As suggested in coredump's comments, we generally interpret imperative statements as syntactic sugar for a function application. Side-effects are represented as usual in pure functional languages: the function takes additional arguments representing the current state and returns additional results representing the updated state (these details possibly wrapped up and hidden behind something like a state monad depending on your preferred mathematical representation).
For example, consider this toy Python function:
def f(x):
y = x + 1
y = x * y
return y
Under denotational semantics, we could desugar each of the three statements in its body as lambdas. Setting aside some technical issues that I will get into at the end of the answer, that could look something like
⟦y = x + 1⟧ = λ(x, y). (x, x + 1)
where the function takes in the old values of x
and y
as inputs and produces their new values as outputs. If we further define
⟦y = x * y⟧ = λ(x, y). (x, x * y)
and
⟦return y⟧ = λ(x, y). y
,
then we can give denotational semantics for f
by composing its statements:
⟦f⟧ = ⟦return y⟧ ∘ ⟦y = x * y⟧ ∘ ⟦y = x + 1⟧ = λx. x² + x
Or, if it's easier to see in Python (please assume Python 2 here, since Python 3 got rid of tuple destructuring in lambda
parameters), we have essentially translated the original program to
increment = lambda (x, y): (x, x + 1)
multiply = lambda (x, y): (x, x * y)
return_y = lambda (x, y): y
f = lambda x: return_y(multiply(increment((x, None))))
which is something we could pretty directly write in a pure functional language using let
s.
(If this desugaring looks familiar, that's probably because you've seen it with do
notation in languages like Haskell, which makes sense to be the same, since the mutable variables can be thought of in terms of state monads. Similarly, more complicated statements, like loops, can be desugared in the same way you would desugar a loop written using do
notation and a continuation monad.)
Now, of course, this does start to blur the line with small-step operational semantics, where we also explicate a "before" and "after" state and give a formula relating them. The main difference is one of perspective: in denotational semantics we are literally thinking of a statement as a mathematical object, and we are free to manipulate it like any other function, whereas in operational semantics we more or less ignore that the statement can be thought of this way and instead focus on how it tells us to change the program state.
Compositionality
As David Young mentions in the comments, one issue that I've swept under the rug is how to decide on the signatures for these functions. For instance, do we curry the functions? How do we order the parameters and return values? Should the functions return values that we know by static analysis are unmodified? Etc.
No particular approach is wrong per se, in the sense that they will all give us correct results, but there is a convention to give every statement's interpretation the same signature: State → (State, Value)
.
Regarding side-effects on mutable variables, in the extreme, a State
includes a partial map from variable names to values of type Value
, and Value
is a union type covering all possible values that can be stored in program variables. That means that every statement has the exact same signature, and we can compose them freely.
Alternatively, if we want to have a little more type safety, we can make the variable storage in State
a partial dependent product that maps variables to values of the appropriate types, and read Value
in State → (State, Value)
as a placeholder for whatever type the statement returns, often the unit or bottom type since most statements have no return value. So, for example, the type of ⟦print('Hello, World!')⟧
would be State → (State, Unit)
since a print statement does not return anything meaningful, whereas ⟦exit(0)⟧
might have type State → (State, Bottom)
since execution cannot continue past this call.
Of course, State
may contain other kinds of state needed to represent other language-relevant side-effects. (Alternatively, you could think of each kind of state as tracked by a separate state monad.) As the OP, kaya3 - support the strike, mentions in the comments, that's where you would track things like terminal output since writing just ⟦print('Hello, World!')⟧ = λs.(s, ())
would elide the print
function's effect.