=Paper=
{{Paper
|id=Vol-3072/paper23
|storemode=property
|title=A Filter Model for the State Monad
|pdfUrl=https://ceur-ws.org/Vol-3072/paper23.pdf
|volume=Vol-3072
|authors=Ugo de'Liguoro,Riccardo Treglia
|dblpUrl=https://dblp.org/rec/conf/ictcs/deLiguoroT21
}}
==A Filter Model for the State Monad==
https://ceur-ws.org/Vol-3072/paper23.pdf
A Filter Model for the State Monad (short
paper)
Ugo de’Liguoro and Riccardo Treglia
Dipartimento di Informatica, Università degli Studi di Torino, Corso Svizzera 185,
10149 Torino, Italy
ugo.deliguoro@unito.it riccardo.treglia@unito.it
Abstract. We consider an untyped computational lambda calculus
equipped with primitives to read and write from a global store. The
calculus is modeled into a solution of a domain equation involving the
state monad. We introduce an intersection type theory with subtyping
such that the induced filter model is a solution of such an equation.
Finally we define a type assignment system which is sound and complete
w.r.t. any model of the calculus.
Keywords: Intersection types · Computational λ-calculi · State Monad
1 An untyped imperative λ-calculus and its semantics
We conceive the calculus λimp as an untyped call-by-value λ-calculus extended
with two operators to read and write from a store. To model such side-effects,
we choose a monadic setting.
In Wadler’s formulation [12], a monad is a triple (T, unit, ?) where T is a type
constructor, and for all types D, E, unitD : D →
− TD and ?D,E : TD × (D → −
TE) → − TE are such that (omitting subscripts and writing ? as an infix opera-
tor):
(unit d) ? f = f d, a ? unit = a, (a ? f ) ? g = a ? λλ d.(f d ? g).
Instances of monads are partiality, exceptions, input/output, store, non deter-
minism, continuations.
Following [7], an untyped computational calculus has a model that is the solution
of the equation D ∼ =D → − TD in the category Dom of domains, namely the
call-by-value reflexive object.
Such domain equation implies that we have just two types: the type of values
D, and the type of computations TD.
Since now D ∼ =D→ − TD, we have:
? : TD × (D → − TD ∼
− TD) → = TD × D →
− TD
Copyright © 2021 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0)
2 U. de’Liguoro, R. Treglia
Therefore, as in [4] the syntax of the monadic calculus is
Val : V, W ::= x | λx.M Com : M, N ::= [V ] | M ? V
To model λimp we instantiate T to a variant of the state monad defined as
SX = S → − (X × S)⊥ , where S is a suitable space of states, and (·)⊥ is the lifting
monad. A natural choice for S is (a subspace of) L →− D (with the order induced
by that one of D), where D is the intended domain of values. However, D is the
solution of the domain equation D ∼ =D→ − SD, which is clearly circular.
To break the circularity, we define the mixed-variant bi-functor G : Domop ×
Dom → − Dom by G(X, Y ) = F X → − (Y × F Y )⊥ , where F X = L → − X,
F h = h ◦ and G(f, g)(x) = (g × F g)⊥ ◦ α ◦ F f where f : X 0 → − X, g : Y → − Y0
and α ∈ G(X, Y ). Now it is routine to prove that G is locally continuous (see
e.g. [8]) so that, by the inverse limit technique, we can find the initial solution
to the domain equation D ∼ =D→ − G(D, D). Now let us define SD X = F D → −
(X × F X)⊥ , that is a functor and a monad, and we conclude:
Theorem 1. There exists a domain D such that the state monad SD is a so-
lution in Dom to the domain equation: D ∼
=D→
− SD D. Moreover, it is initial
among all solutions to such equation.
It remains to define the operators to read and write from the store, for which we
use ideas from [9–11]: get` : (D →
− SD D) → − SD D and set` : D × SD D → − SD D;
so the syntax of λimp is completed by
Com : M, N ::= . . . | get` (λx.M ) | set` (V, M ) (` ∈ L)
The additional operators are actually two families of operators, indexed over
the denumerable set of locations: get` (λx.M ) reading the value V associated to
the location ` in the current state, and binding x to V in M ; set` (V, M ) which
modifies the state assigning V to `, and then proceeds as M . The operational
semantics is given in [5].
Denotational Semantics. The triple (SD , unit , ?) is a monad, where (unit d) ς
= (d, ς) and (m ? d) ς : let (d0 , ς 0 ) = m ς in (d d0 )ς which is ⊥ if m ς = ⊥, and
d∈D∼ =D→ − SD D.
The semantics à la Plotkin and Power [9–11] of get` and set` , is given by Jget` K :
(SD D)D → − SD D where Jget` K d ς = d (ς `) ς, and Jset` K : D ×SD D → − SD D where
Jset` K(d, c) ς = c(ς[` 7→ d]) and c ∈ SD D = S → − (D × S)⊥ and ς[` 7→ d] is the
store sending ` to d and it is equal to ς, otherwise.
Then we interpret values from Val in D and computations from Com in SD D
via the maps J·KD : Val → − Env → − D and J·KSD : Com → − Env → − SD D, where
Env = Var → − D is the set of environments interpreting term variables.
Definition 1. A λimp -model is a structure D = (D, SD , J·KD , J·KSD ) such that:
1. D is a domain s.t. D ∼
=D→
− SD D, where SD is the state monad;
A Filter Model for the State Monad (short paper) 3
2. for all e ∈ Env, V ∈ Val and M ∈ Com:
JxKD e = e(x) Jλx.M KD e = λd ∈ D. JM KSD e[x 7→ d]
J [V ] KSD e = unit (JV KD e) JM ? V KSD e = (JM KSD e) ? (JV KD e)
Jget` (λx.M )KSD e = Jget` K(Jλx.M KD e) Jset` (V, M )KSD e = Jset` K(JV KD e, JM KSD e)
By unravelling definitions and applying to an arbitrary store ς ∈ S, the last two
clauses can be written:
Jget` (λx.M )KSD e ς = JM KSD (e[x 7→ ς(`)]) ς
Jset` (V, M )KSD e ς = JM KSD e (ς[` 7→ JV KD e])
For M, N ∈ Com, we say that the equation M = N is true in D, notation
|=D M = N , if JM KSD e = JN KSD e for all e ∈ Env.
Proposition 1. The following equations are true in any λimp -model D:
1. [V ] ? (λx.M ) = M [V /x]
2. M ? λx.[x] = M
3. (L ? λx.M ) ? λy.N = L ? λx.(M ? λy.N )
4. get` (λx.M ) ? W = get` (λx.(M ? W ))
5. set` (V, M ) ? W = set` (V, M ? W )
The above proposition states that the three monadic equations (parts (1) to (3))
are true in any model, while parts (4) and (5) imply that the operators set and
get are algebraic.
2 The filter model construction
Following Abramsky [1], domains in a suitable category can be described via
an intersection type theory. A type theory is a structure ThA = (LA , ∧, ≤A , ωA )
where LA is the language of ThA , inducing the algebraic domain A (see below),
namely a set of type expressions closed under ∧; ωA ∈ LA is a special constant,
and ≤A is a pre-order over LA such that α ≤A ωA for all α ∈ LA and α ∧ α0 is
the meet of α, α0 w.r.t. ≤A .
A non empty F ⊆ LA is a filter of ThA if it is upward closed and closed under
intersection; let FA be the set of filters of ThA ; then (FA , ⊆) is a domain. We
seek theories ThD and ThS such that FD ∼ = [FD →− FS →− (FD × FS )⊥ ].
Actually, we consider four theories, whose definitions are mutually inductive,
derived by applying operators in the above equation. Indeed these are specific
functors that can be represented as type theoretical constructors. We recall that
if ThA , ThB are type theories, then we may define for α ∈ LA and β ∈ LB the
following languages:
LA⊥ ψ ::= α | ψ ∧ ψ 0 | ωA⊥ bottom theory
LA×B π ::= α × β | π ∧ π 0 | ωA×B product theory
LA→ − β | φ ∧ φ0 | ωA→
− B φ ::= α → −B arrow theory
LS,A σ ::= h` : αi | σ ∧ σ 0 | ωS store theory
4 U. de’Liguoro, R. Treglia
Then the respective theories are:
ThA⊥ : α ≤A α0 =⇒ α ≤A⊥ α0
ThA×B : ωA×B ≤A×B ωA × ωB (α × β) ∧ (α0 × β 0 ) ≤A×B (α ∧ α0 ) × (β ∧ β 0 )
α ≤A α 0 β ≤B β 0 =⇒ α × β ≤A×B α0 × β 0
ThA−
→B : →B ≤A−
ωA− →B ωA −
→ ωB (α − → β 0 ) ≤A−
→ β) ∧ (α − → (β ∧ β 0 )
→B α −
α0 ≤A α β ≤B β 0 =⇒ α −
→ β ≤A− 0
→B α −→ β0
ThS,A : h` : αi ∧ h` : α0 i ≤S,A h` : α ∧ α0 i α ≤A α0 =⇒ h` : αi ≤S,A h` : α0 i
We assume that ∧ and × take precedence over → − , and that →− associates to
the right, so that δ → − τ ∧ τ 0 reads as δ →
− (τ ∧ τ 0 ) and δ 0 →
− σ0 →
− δ 00 × σ 00 reads
as δ 0 →
− (σ 0 →
− (δ 00 × σ 00 )).
We obtain a solution of the domain equation in terms of domains of filters.
Theorem 2. If ThD = ThD→ − SD , ThS = ThS,D , ThC = Th(D×SD)⊥ , ThSD =
− C are defined by mutual induction, then FD ∼
ThS → = [FD →
− FSD ].
A λimp -model. To show that FD is a λimp -model we have to define the following
operators:
unit : FD →− FSD ? : FSD × FD → − FSD
get` : FD →
− FSD set` : FD × FSD → − FSD
This can be done as follows:
unit F F = Filt{σ −→ δ × σ ∈ LSD | δ ∈ F }
G ?F F = Filt{σ −→ δ 00 × σ 00 ∈ LSD | ∃ δ 0 , σ 0 . σ −
→ δ × σ0 ∈ G & δ0 −
→ σ0 −
→ δ 00 × σ 00 ∈ F }
F
get` (F ) = Filt{(h` : δi ∧ σ) − → κ ∈ LSD | δ − → (σ − → κ) ∈ F }
setF 0
` (F, G) = Filt{σ −→ κ ∈ LSD | ∃δ ∈ F. h` : δi ∧ σ 0 − → κ ∈ G & ` 6∈ dom(σ 0 )}
where FiltX is the least filter including the set X.
Theorem 3. (FD , SFD , J·KFD , J·KFSD ) is a λimp -model.
Type assignment system. A typing context is a finite set Γ = {x1 : δ1 , . . . , xn :
δn } with pairwise distinct xi ’s and with δi ∈ LD for all i = 1, . . . , n; with Γ as
before, we set dom(Γ ) = {x1 , . . . , xn }; finally, by Γ, x : δ we mean Γ ∪ {x : δ} for
x 6∈ dom(Γ ). Type judgments are of either forms Γ ` V : δ or Γ ` M : τ . Define
` ∈ dom(σ) if ∃δ 6= ωD . σ ≤S h` : δi; then the rules of the type assignment
system are listed below.
Γ, x : δ ` M : τ
(var) (λ)
Γ, x : δ ` x : δ Γ ` λx.M : δ →
− τ
Γ `V :δ 0 0 0 0 00 00
Γ `M :σ→
− δ ×σ Γ `V :δ →
− σ →
− δ ×σ
(unit) (?)
Γ ` [V ] : σ →
− δ×σ 00 00
Γ `M ?V :σ →
− δ ×σ
Γ, x : δ ` M : σ →
− κ Γ `V :δ Γ ` M : (h` : δi ∧ σ) →
− κ ` 6∈ dom(σ)
(get) (set)
Γ ` get` (λx.M ) : (h` : δi ∧ σ) →
− κ Γ ` set` (V, M ) : σ →
− κ
A Filter Model for the State Monad (short paper) 5
0 0
Γ `T :ϕ Γ `T :ϕ Γ `T :ϕ ϕ≤ϕ
(ω) (∧) (≤)
0 0
Γ `T :ω Γ `T :ϕ∧ϕ Γ `T :ϕ
See [5] for an explanation of the rules of this system.
Definition 2 (Type interpretation). Let TypeEnv = TypeVar → − ℘(D) be
the set of the interpretations of type variables α, ranged over by ξ; then we define
the sets: JδKξ ⊆ D, JσKξ ⊆ S = [L → − D], JκKξ ⊆ C = (D × S)⊥ , Jτ Kξ ⊆ SD D by
the following inductive clauses:
1. JαKξ = ξ(α) and Jδ → − τ Kξ = {f ∈ [D → − SD D] | f (JδKξ ) ⊆ Jτ Kξ },
2. Jh` : δiKξ = {s ∈ S | s(`) ∈ JδKξ },
3. Jδ × σKξ = JδKξ × JσKξ ,
4. Jσ →
− κKξ = {g ∈ [S → − (D × S)⊥ ] | g(JσKξ ) ⊆ JκKξ },
5. Jϕ ∧ ϕ0 Kξ = JϕKξ ∩ Jϕ0 Kξ , for ϕ, ϕ0 of the same sort,
6. JωD Kξ = D, JωS Kξ = S, JωC Kξ = C = (D × S)⊥ , and JωSD Kξ = SD D.
The following definition is standard in literature, see [2] Def. 17.1.3.
Definition 3 (Semantic Satisfiability). Let e be a term environment and ξ
a type environment:
1. e, ξ |=D Γ if e(x) ∈ JΓ (x)KD
ξ for all x ∈ dom (Γ );
2. Γ |=D V : δ (Γ |=D M : τ ) if
e, ξ |=D Γ implies JV KD e ∈ JδKξ (JM KSD e ∈ Jτ Kξ );
3. Γ |= V : δ (Γ |= M : τ ) if Γ |=D V : δ (Γ |=D M : τ ) for all models D.
Theorem 4 (Soundness and Completeness).
Γ ` V : δ ⇔ Γ |= V : δ and Γ ` M : τ ⇔ Γ |= M : τ
The proof of soundness is by induction on the type derivation; the completeness
is proved using Theorem 3 and the fact that the interpretation of a term in the
filter model coincides with the set of types that can be assigned to it.
Final remarks. In the present work we gave a sketch of some of the issues
that can be encountered in investigating the semantics of an untyped imperative
λ-calculus and, albeit not in full details, outlined how a filter model for the state
monad can be derived once the domain equation defining the specific call-by-
value reflexive object is understood and dissected.
Although filter models have been extensively discussed in the literature, see
e.g. [6], to our knowledge this is the first construction of such a model for an
imperative lambda calculus.
In [3] we constructed a filter model for the pure computational λ-calculus, namely
without operations nor constants, where the underlying monad is generic. In
that work we highlighted that this construction requires some conditions on
interpretation of intersection types. Here such conditions are naturally satisfied
by the type theory and assignment system tailored for the state monad. An open
issue is the investigation whether there is a uniform construction of filter models
for calculi with algebraic operators over generic monads.
6 U. de’Liguoro, R. Treglia
References
1. Abramsky, S.: Domain theory in logical form. Ann. Pure Appl. Log. 51(1-2), 1–77
(1991). https://doi.org/10.1016/0168-0072(91)90065-T
2. Barendregt, H.P., Dekkers, W., Statman, R.: Lambda Calculus with Types. Per-
spectives in logic, Cambridge University Press (2013)
3. de’Liguoro, U., Treglia, R.: Intersection types for the computational lambda-
calculus. CoRR abs/1907.05706 (2019)
4. de’Liguoro, U., Treglia, R.: The untyped computational λ-calculus and its
intersection type discipline. Theor. Comput. Sci. 846, 141–159 (2020).
https://doi.org/10.1016/j.tcs.2020.09.029, https://doi.org/10.1016/j.tcs.
2020.09.029
5. de’Liguoro, U., Treglia, R.: Intersection types for a computational lambda-calculus
with global state (2021), https://arxiv.org/abs/2104.01358
6. Dezani-Ciancaglini, M., Honsell, F., Alessi, F.: A complete characterization of com-
plete intersection-type preorders. ACM Trans. Comput. Log. 4(1), 120–147 (2003)
7. Moggi, E.: Computational Lambda-calculus and Monads. Report ECS-LFCS-88-
66, University of Edinburgh, Edinburgh, Scotland (1988)
8. Pierce, B.C.: Basic category theory for computer scientists. Foundations of com-
puting, MIT Press (1991)
9. Plotkin, G.D., Power, J.: Notions of computation determine monads. In: FOS-
SACS 2002. Lecture Notes in Computer Science, vol. 2303, pp. 342–356.
Springer (2002). https://doi.org/10.1007/3-540-45931-6 24, https://doi.org/10.
1007/3-540-45931-6\_24
10. Plotkin, G.D., Power, J.: Algebraic operations and generic effects. Appl. Categor-
ical Struct. 11(1), 69–94 (2003). https://doi.org/10.1023/A:1023064908962
11. Power, J.: Generic models for computational effects. Theor. Comput. Sci. 364(2),
254–269 (2006)
12. Wadler, P.: Monads for functional programming. In: Advanced Functional Pro-
gramming, First International Spring School on Advanced Functional Program-
ming Techniques. Lecture Notes in Computer Science, vol. 925, pp. 24–52. Springer
(1995). https://doi.org/10.1007/3-540-59451-5 2