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