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 lter model is a solution of such an equation. Finally we de ne a type assignment system which is sound and complete w.r.t. any model of the calculus.
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-e ects, we choose a monadic setting.
In Wadler's formulation [
Following [
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
Therefore, as in [
Val : V; W ::= x j x:M
Com : M; N ::= [V ] j M ? V
To model imp we instantiate T to a variant of the state monad de ned 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 de ne 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 : X0 ! X, g : Y ! Y 0
and 2 G(X; Y ). Now it is routine to prove that G is locally continuous (see
e.g. [
It remains to de ne the operators to read and write from the store, for which we use ideas from [9{11]: get` : (D ! SDD) ! SDD and set` : D SDD ! SDD; so the syntax of imp is completed by
Com : M; N ::= : : : j get`( x:M ) j set`(V; M ) (` 2 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
modi es the state assigning V to `, and then proceeds as M . The operational
semantics is given in [
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 2 D = D ! SDD.
The semantics a la Plotkin and Power [9{11] of get` and set`, is given by Jget`K : (SDD)D ! SDD where Jget`K d & = d (& `) &, and Jset`K : D SDD ! SDD where Jset`K(d; c) & = c(&[` 7! d]) and c 2 SDD = 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 SDD via the maps J KD : Val ! Env ! D and J KSD : Com ! Env ! SDD, where Env = Var ! D is the set of environments interpreting term variables. De nition 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 ! SDD, where SD is the state monad; 2. for all e 2 Env, V 2 Val and M 2 Com:
JxKDe = e(x) J x:M KDe = d 2 D: JM KSDe[x 7! d] J [V ] KSDe = unit (JV KDe) JM ? V KSDe = (JM KSDe) ? (JV KDe) Jget`( x:M )KSDe = Jget`K(J x:M KDe) Jset`(V; M )KSDe = Jset`K(JV KDe; JM KSDe) By unravelling de nitions and applying to an arbitrary store & 2 S, the last two clauses can be written:
Jget`( x:M )KSDe & = JM KSD(e[x 7! &(`)]) &
Jset`(V; M )KSDe & = JM KSDe (&[` 7! JV KDe]) For M; N 2 Com, we say that the equation M = N is true in D, notation j=D M = N , if JM KSDe = JN KSDe for all e 2 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
lter model construction
Following Abramsky [
A non empty F LA is a lter of ThA if it is upward closed and closed under intersection; let FA be the set of lters 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 de nitions are mutually inductive, derived by applying operators in the above equation. Indeed these are speci c functors that can be represented as type theoretical constructors. We recall that if ThA, ThB are type theories, then we may de ne for 2 LA and 2 LB the following languages:
LA? LA B LA!B LS;A ::= j ^ 0 j !A? ::= j ^ 0 j !A B ::= ! j ^ 0 j !A!B ::= h` : i j ^ 0 j !S bottom theory product theory arrow theory store theory
ThA? :
A 0 =)
A? 0 ThA B : !A B A B !A
!B ( A 0
B 0 =) ) ^ ( 0 A B 0
0 0) A B ( ^ 0) ( ^ 0) ThA!B : !A!B A!B !A ! !B ( ! ) ^ ( ! 0) A!B ! ( ^ 0) 0 A
B 0 =) !
A!B 0 ! 0 ThS;A : h` : i ^ h` : 0i S;A h` : ^ 0i A 0 =) h` : i S;A h` : 0i 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 lters. Theorem 2. If ThD = ThD!SD, ThS = ThS;D, ThC = Th(D SD)? , ThSD = ThS!C are de ned by mutual induction, then FD = [FD ! FSD]. A imp-model. To show that FD is a imp-model we have to de ne the following operators: unit : FD ! FSD get` : FD ! FSD
? : FSD set` : FD
FD ! FSD FSD ! FSD
unit F F = Filtf ! 2 LSD j 2 F g G ?F F = Filtf ! 00 00 2 LSD j 9 0; 0: ! 0 2 G & 0 ! 0 ! 00 get`F (F ) = Filtf(h` : i ^ ) ! 2 LSD j ! ( ! ) 2 F g set`F (F; G) = Filtf 0 ! 2 LSD j 9 2 F: h` : i ^ 0 ! 2 G & ` 62 dom( 0)g 00 2 F g where FiltX is the least lter including the set X.
Theorem 3. (FD; SFD ; J KFD ; J KFSD ) is a imp-model.
Type assignment system. A typing context is a nite set = fx1 : 1; : : : ; xn : ng with pairwise distinct xi's and with i 2 LD for all i = 1; : : : ; n; with as before, we set dom( ) = fx1; : : : ; xng; nally, by ; x : we mean [ fx : g for x 62 dom( ). Type judgments are of either forms ` V : or ` M : . De ne ` 2 dom( ) if 9 6= !D: S h` : i; then the rules of the type assignment system are listed below.
; x : ` x : ` [V ] : ! ; x : ` M : ! (var)
(unit) ` get`( x:M) : (h` : i ^ ) ! ` M : ! 0 0
` V : 0 ! 0 ! 00 (get) ` T : ' ` T : '0
(^)
` T : !
See [
` T : ' ^ '0 ` T : ' '
'0 ` T : '0 ( ) De nition 2 (Type interpretation). Let TypeEnv = TypeVar ! }(D) be the set of the interpretations of type variables , ranged over by ; then we de ne the sets: J K D; J K S = [L ! D]; J K C = (D S)?; J K SDD by the following inductive clauses: 635421...... JJJJJJh!'`DK^!:K='iK0=KKK (=D===),JfJfJas'Kg!nK2Sd2KS\J[SJ=jJ!'!sKS(0K`,,()KD,J2!fo=CJrKSKf'f)=;g?',2]C0j[oDg=f(Jt!(hDeKSs)DamDS )e]J?js,Kfoar(gJtn,,dK J)!SDK J K g, = SDD.
The following de nition is standard in literature, see [
if e(x=)D2 JM : ) if 2. j=D V : ( j 3. e; j=j=VD: i(mpj=lieMsJ V: KD) ief 2 Jj=KD (VJ M: KS(D ej=2DJ MK ):; ) for all models D. Theorem 4 (Soundness and Completeness).
` V : , j= V : and ` 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 lter 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 lter model for the state monad can be derived once the domain equation de ning the speci c call-byvalue re exive object is understood and dissected.
Although lter models have been extensively discussed in the literature, see
e.g. [
In [