mopdf.com

T ( ) is the covariant powerset functor, i.e.T (A) P(A) and T (f )(X) is the image of X along f ηA is the singleton map a 7 {a} µA is the big union map X 7 XIt is easy to check the equalizing requirement, in factηT A : X 7 {X}T (ηA ): X 7 {{x} x X}therefore ηT A (X) T (ηA )(X) iff X is a singleton.Example 2.6 computations with side-effects: T ( ) is the functor (S ( S)), where S is a nonempty set of stores.Intuitively a computation takes a store and returns a value together with themodified store. ηA is the map a 7 (λs: S.ha, si) µA is the map f 7 (λs: S.eval(f s)), i.e. µA (f ) is the computation that givena store s, first computes the pair computation-store hf 0 , s0 i f s and thenreturns the pair value-store ha, s00 i f 0 s0 .One can verify for himself that other notions of computation (e.g. partial, probabilistic or non-deterministic with side-effects) fit in this general definition.2.1A simple language and its interpretationThe aim of this section is to focus on the crucial ideas of the interpretation, and thelanguage has been oversimplified (for instance terms have exactly one free variable)in order to define its interpretation in any computational model without requiringany additional structure on it. However, richer languages, e.g. with product andfunctional types, will be considered in Section 3. The term language we introduceis parametric in a signature (i.e. a set of base types and unary function symbols),therefore its interpretation in a computational model (T, η, µ) over a category C, isparametric in an interpretation of the symbols in the signature. Given an interpretation [[A]] for any base type A, i.e. an object of the Kleislicategory CT , then the interpretation of a type τ : : A T τ is an object [[τ ]]of CT defined in the obvious way, namely [[T τ ]] T [[τ ]]. Given an interpretation [[f ]] for any unary function symbol f of arity τ1 τ2 ,i.e. a morphism from [[τ1 ]] to [[τ2 ]] in CT , then the interpretation of a well-formedterm x: τ e: τ 0 is a morphism [[x: τ e: τ 0 ]] from [[τ ]] to [[τ 0 ]] in CT defined byinduction on the derivation of x: τ e: τ 0 (see Table 1). On top of the term language we consider two atomic predicates: equivalenceand existence (see Table 2).5

RULE SYNTAXvarx: τ x: τSEMANTICS η[[τ ]]letx: τ e1 : τ1 g1x1 : τ 1 e 2 : τ 2 g2x: τ (let x1 e1 in e2 ): τ2 g1 ; T g2 ; µ[[τ2 ]]i.e. g1 ; g2 in the Kleisli categoryf : τ1 τ2x: τ e1 : τ1x: τ f (e1 ): τ2 g1 g1 ; T [[f ]]; µ[[τ2 ]]x: τ e: τ 0x: τ [e]: T τ 0 g g; ηT [[τ 0 ]]x: τ e: T τ 0x: τ µ(e): τ 0 g g; µ[[τ 0 ]][]µTable 1: Terms and their interpretationRULE SYNTAXeqx: τ1 e1 : τ2 x: τ1 e2 : τ2 x: τ1 e1 e2 : τ2 SEMANTICSg1g2g 1 g2exx: τ1 e: τ2x: τ1 e τ2 g g factors through η[[τ2 ]]i.e. there exists (unique) h s.t. g h; η[[τ2 ]]Table 2: Atomic assertions and their interpretation6

Remark 2.7 The let-constructor is very important semantically, since it correspondsto composition in the Kleisli category CT . While substitution (of a variable with anexpression denoting a value) corresponds to composition in C.In the λ-calculus (let x e in e0 ) is usually treated as syntactic sugar for (λx.e0 )e,and this can be done also in the λc -calculus (because of (β) in Table 8). However, wethink that this is not the right way to proceed, because it amounts to understandingthe let-constructor, which makes sense in any computational model, in terms ofconstructors that make sense only in λc -models. On the other hand, (let x e in e0 )cannot be reduced to the more basic substitution (i.e. e0 [x: e]) without collapsingCT to C.Remark 2.8 The existence of e does not simply means that the computation denotedby e terminates (as, say, in the logic of partial terms), but something stronger,namely that e denotes a value. For instance: a non-deterministic computation exists iff it gives exactly one result; a computation with side-effects exists iff it does not change the store.According to the paradigm of Categorical Logic, formulas should be interpreted bysubobjects. This can be achieved by interpreting the binary predicate : τ , i.e.equality of computations of type τ , by the diagonal T [[τ ]] and the unary predicate τ , i.e. existence of computations of type τ , by η[[τ ]] , which is a mono because ofthe equalizing requirement.2.2Embedding of a computational model in a toposWe show that any computational model (T, η, µ) over a small category C can be liftedto a computational model (T̂ , η̂, µ̂) over the topos Cˆ of presheaves (i.e. the functoropcategory SetC ), and that such a lifting commutes with the Yoneda embedding Yˆ i.e.of C into C,T̂ (Y ) Y(T ) ,η̂Y Y(η ) ,µ̂Y Y(µ )As pointed out in [Sco80] such an embedding enable us to switch from the equational (and rather inexpressive) calculus of an arbitrary computational model to theintuitionistic higher-order logic of (a computational model over) a topos.The monad (T̂ , η̂, µ̂) is defined by using the Yoneda embedding Y: C Cˆ andˆLanY , i.e. the left adjoint to Y; : CˆC CˆC mapping any F : C Cˆ to its left Kanextension4 along Y (see [Mac71]), namely:T̂ Lan(T ; Y) ,η̂ Lan(η; Y) ,µ̂ Lan(µ; Y)The commutativity with the Yoneda embedding (stated above) and the fact that Yinduces a full and faithful embedding Y of CT into CˆT̂ follow from some well-knownproperties of Y and LanY , summarised in the following lemma:ˆLemma 2.9 If C is small category, then Y: C Cˆ and LanY : CˆC CˆC are full andˆfaithful. Moreover Y; LanY F F for every F : C C.4the left adjoint LanY exists because Set is small cocomplete7

3Extending the languageIn this section we discuss how to interpret terms with any finite number of variables(instead of exactly one as in Table 1) and how datatypes relate to computations. Wewill consider only product and functional types, because sum types are completelystraightforward5 . This will allow a comparison with cartesian closed categories (ccc)and partial cartesian closed categories (pccc).The standard requirement on a category for interpreting terms with any finitenumber of variables is that it must have finite products, so that the interpretation [[f ]]of a function symbol f of arity τ τ is a morphism from [[ (τ )]] (i.e. [[τ1 ]] . . . [[τn ]])to [[τ ]] and similarly the interpretation of a well-formed term x1 : τ1 , . . . , xn : τn e: τis a morphism from [[ (τ )]] to [[τ ]].According to the view of “programs as functions from values to computations”,products should be taken in C, since a value of type A B is a pair of values one oftype A and the other of type B, even though the natural category for interpretingprograms is CT . However, products are not enough to extend the interpretation toterms with more than one free variable, because we must be able to take a pairvalue-computation or computation-computation and turn it into a computation ofa pair.Example 3.1 Let g2 : τ1 T τ2 and and g: τ1 τ2 T τ be the interpretations ofx1 : τ1 e2 : τ2 and x1 : τ1 , x2 : τ2 e: τ respectivelly. The problem with terms havingmore than one free variable (and its solution) becomes apparent if we try to interpretx1 : τ1 (let x2 e2 in e): τ , when both x1 and x2 are free in e.If T were IdC , then [[x1 : τ1 (let x2 e2 in e): τ ]] would be hidτ1 , g2 i; g. In thegeneral case, Table 1 says that ; above is indeed composition in the Kleisli category,therefore hidτ1 , g2 i; g becomes hidτ1 , g2 i; T g; µτ . But in hidτ1 , g2 i; T g; µτ there is atype mismatch, since the codomain of hidτ1 , g2 i is τ1 T τ2 , while the domain ofT g is T (τ1 τ2 ). To get around this we require T to have a tensorial strengthtA,B : A T B T (A B) (see below), so that x1 : τ1 (let x2 e2 in e): τ will beinterpreted by hidτ1 , g2 i; tτ1 ,τ2 ; T g; µτ .Similarly for interpreting x: τ f (e1 , e2 ): τ 0 , we need a natural transformationψA,B : (T A T B) T (A B) (see Definition 3.4), which given a pair of programsreturns a program computing a pair. More precisely, let gi : τ T τi be the interpretation of x: τ ei : τi , then [[x: τ f (e1 , e2 ): τ 0 ]] is hg1 , g2 i; ψτ1 ,τ2 ; T [[f ]]; µ.Definition 3.2 Let C be a category with finite products, and rA , αA,B,C and cA,B bethe natural isomorphisms:r(1 A) A,α(A B) C A (B C),c(A B) (B A)A computational cartesian model over C is a computational model (T, η, µ) overC together with a tensorial strength tA,B : (A T B) T (A B) of T , i.e. a natural5coproducts are preserved by the inclusion of C into the Kleisli category CT8

transformation s.t.1 TAt1,A T (1 A)@@ r@ [email protected]@tA B,C(A B) T CT rA TA T ((A B) C)αA,B,T CT αA,B,C idA tB,CtA,B CA (B T C) A T (B C) T (A (B C))satisfying the following diagrams:A BidA BidA ηB A TB ηA BtA,BidA µBA T 2B A B T (A B) µA BtA,T BT tA,B 2 T (A T B) T (A B)Remark 3.3 In general the tensorial strength t has to be given as an extra parameterfor models. However, t is uniquely determined (but it may not exists) by T andthe cartesian structure on C, when C has enough points, i.e. if f, g: A B, thenf g ( h: 1 A.h; f h; g).The diagrams above are not new, they are all in [Koc70b], where a one-one correspondence is established between functorial and tensorial strengths 6 : the first two diagrams, saying that t is a tensorial strength of T , are (1.7) and(1.8) in [Koc70b]. By Theorem 1.3 in [Koc70b] t induces a functorial strengthof T making T a C-enriched (also called strong) functor. the last two diagrams say that η and µ are natural transformations between.suitable C-enriched functors, namely η: IdC T and µ: T 2 T (see Remark 1.5 in [Koc70b]).6If V is a monoidal closed category, then a functorial strength of an endofunctor T on Vis a natural transformation stA,B : B A T B T A making T a V -enriched functor. Intuitively stinternalizes the action of T on morphisms.9

Definition 3.4 The tensorial strength t induces a monoidal structure, i.e. anatural transformation ψA,B : (T A T B) T (A B) and a map ψ1 : 1 T 1ψA,B cT A,T B ; tT B,A ; T (cT B,A ; tA,B ); µA B,ψ1 η 1satisfying certain diagrams (see [EK66]).The morphism ψA,B : (T A T B) T (A B) has the correct domain and codomainto interpret the pairing of a computation of type A with one of type B (obtainedby first evaluating the first argument and then the second), while the morphismψ1 interprets the computation of hi (the empty tuple). There is also a dual notionof pairing, namely ψ̃A,B cA,B ; ψB,A ; T cB,A , which amounts to first evaluating thesecond argument and then the first (see (2.1) and (2.2) at page 14 in [Koc70b]).The categorical interpretation of functional types in a computational model resembles that of partial function spaces in a pccc (see [Ros86, Mog86]):Definition 3.5 Let C be a category with finite products. A λc -model over C is acomputational cartesian model (T, η, µ, t) over C together with a family of universalarrows evalTA,B : (BTA A) T B (in C) s.t. for any f : (C A) T B there exists aunique h: C BTA (denoted by ΛTA,B,C (f )) making the following diagram commuteBTAevalTA,B A TB h idAfC AA more suggestive way of saying the same thing is that there is a natural isomorphismCT (C A, B) C(C, BTA ), where A, B and C vary over C op , CT and C respectively.The simple language introduced in Section 2.1 and its interpretation can beextended according to the additional structure available in a cartesian computationalmodel (T, η, µ, t) on a category C with finite products: there is a new type 1, interpreted by the terminal object of C, and a new typeconstructor τ1 τ2 interpreted by the product of [[τ1 ]] and [[τ2 ]] in C the interpretation of a well-formed term Γ e: τ , where Γ is a sequencex1 : τ1 , . . . , xn : τn , is a morphism from [[Γ]] (i.e. [[τ1 ]] . . . [[τn ]]) to [[τ ]] in CT(see Table 3)7 .In a λc -model the interpretation can be extended to functional types and λ-terms,1 ]]namely: the type τ1 * τ2 is interpreted by [[τ2 ]][[τT , while abstraction and applicationare interpreted as in Table 4.7We do not have to consider nonunary functions explicitly, because in a language with productsthey can be treated as unary functions from a product type.10

RULE SYNTAXSEMANTICSvarx1 : τ1 , . . . , xn : τn xi : τi πin ; η[[τi ]]letΓ e 1 : τ1Γ, x1 : τ1 e2 : τ2Γ (let x1 e1 in e2 ): τ2 g1 g2 hid[[Γ]] , g1 i; t[[Γ]],[[τ1]] ; T g2 ; µ[[τ2 ]]Γ : 1 ![[Γ]] ; η1 where !A is the only morphism from A to 1hiΓ e 1 : τ1Γ e 2 : τ2Γ he1 , e2 i: τ1 τ2 g1 g2 hg1 , g2 i; ψ[[τ1 ]],[[τ2 ]]Γ e: τ1 τ2Γ πi (e): τ1 g g; T (πi )πiTable 3: Terms and their interpretationRULE SYNTAXSEMANTICSλΓ, x1 : τ1 e2 : τ2 gΓ (λx1 : τ1 .e2 ): τ1 * τ2 ΛT[[τ1 ]],[[τ2 ]],[[Γ]](g); η[[τ1 *τ2 ]]appΓ e 1 : τ1Γ e: τ1 * τ2Γ e(e1 ): τ2 g1 g hg, g1 i; app[[τ1 ]],[[τ2 ]]where appA,B : T (BTA ) T A T B is ψBTA ,A ; T (evalTA,B ); µBTable 4: λ-terms and their interpretation11

3.1ExamplesIn this section we show few general ways of constructing computational models fromsimpler ones. Each of them amounts to adding a new feature to computations.Example 3.6 Let (T, η, µ, t) be a cartesian computational model on a topos (forsimplicity Set), then the following are cartesian computational models: Let S be inhabited (i.e. 1 S), then the model (TS , η S , µS , tS ) of T -computationswith side-effects in S isTS ( ) ( S)STηAS ΛTS,(A S),A (ηA S )µSA ΛTS,(A S),(T 2 A) (evalTS,(TS A S) ; T (evalTS,(A S) ); µA S )S 1tSA,B ΛTS,(A S),(A TS B) (αA,TS B,S ; (idA evalTS,(B S) ); tA,B S ; T (αA,B,S)) the model (TE , η E , µE , tE ) of T -computations with exceptions in E isTE ( ) T ( E)ηAE in1 ; ηA EµEA T ([idT (A E) , in2 ; ηA E ]); µA EtEA,B tA,B E ; T (dA,B,E ; [idA B , π2 ])ininwhere A 1 A B 2 B is a coproduct diagram,[f, g]: A B C is the mediating morphism of f : A C and g: B C, i.e.the unique h: A B C s.t. f in1 ; h and g in2 ; h,ddA,B,C is the natural isomorphism A (B C) (A B) (A C) expressingcommutativity of coproducts w.r.t. products8These constructions provide basic building blocks, that can be combined togetherfor instance: TE S ( ) T (( S) E)S and TS E ( ) T (( E) S)S combine side-effectsand exceptions. In the former the store is lost, when an exception is raised,while in the latter it is retained.( ) If T is the monad of R-continuations9 , i.e. T ( ) RR , then the monadA STS (A) RS (R ) combines continuation and side-effects as done when givingthe denotational semantics of imperative languages with goto.Monad-morphisms provide a simple tool for relating two computational models:Definition 3.7Given two cartesian computational models (T, η T , µT , tT ) and (S, η S , µS , tS ) over the8which holds in cartesian closed categories, but not in general9It is not clear what properties R must have in order for the monad T to satisfy the equalizingrequirement. Intuitively one expects that the category C must have enough R-observations, i.e.f g ( h: B R.f ; h g; h) for any f, g: A B12

same category, a monad-morphism from the first to the second model is a natural.transformation σ: T S s.t. :ηATAidA TA µTAηAS TA T AσA2σA A2µSA T 2AtTA,B T (A B)A TBA σB A SBσA B S(A B)tSA,Bwhere σ 2 is the horizontal composition, i.e. σA2 T (σA ); σSA σT A ; S(σA ).Example 3.8 For each of the computational model constructions defined above thereis a monad morphism from T to it, namely:. σ S : T TS is the natural transformation s.t. σAS is ΛTS,A S,T (A) (tA,S ). σ E : T TE is the natural transformation s.t. σAE is T (inA,E1 )Monad-morphisms are not adequate for relating λc -models, because the naturaltransformation σ cannot be extended to functional types. Instead, one can usea notion of logical relation between λc -models (see [Mog88] for various notions oflogical relation between λp -models).4The λc-calculusIn this section we present a formal system, the λc -calculus, based on many sortedintuitionistic logic with two atomic predicates, existence and equivalence.We claim that the formal system is sound and complete w.r.t. λc -models (overtoposes). Soundness amounts to showing that the inference rules are admissible inany λc -model, while completeness amounts to showing that any λc -theory has aninitial model (given by a term-model construction).The inference rules of the λc -calculus are for deriving sequents Γ. A, where Γis a sequence of type assignments x: τ , is a set of formulas and A is a formula s.t.the free variables FV( , A) of and A are included in the declared variables DV(Γ)of Γ. The intuitive meaning of Γ. A is: “for all variables in Γ, if all formulas in are true, then A is true”. We have intentionally left the set of formulas unspecified,since it depends on what class of models one is interested in. There is a minimaland maximal choice for the set of formulas: if the language has to be interpreted in any λc -model, then only atomic formulas (including e e0 : τ and e τ ) are allowed if the language has to be interpreted only in λc -model over a topos, then allhigher order formulas are allowed.13

The inference rules are partitioned as follows: general rules for (higher order) intuitionistic logic, where variables range overvalues, while terms denotes computations (see Table 5 for the most relevantrules)10 the basic inference rules for computational models (see Table 6) the inference rules for product types (see Table 7) the inference rules for functional types (see Table 8)Remark 4.1 A comparison among λc -, λv - and λp -calculus shows that: the λv -calculus proves less equivalences between λ-terms, e.g. (λx.x)(yz) (yz) is provable in the λc - but not in the λv -calculus the λp -calculus proves more equivalences between λ-terms, e.g. (λx.yz)(yz) (yz) is provable in the λp - but not in the λc -calculus, because y can be aprocedure, which modifies the store (e.g. by increasing the value contained ina local static variable) each time it is executed. a λ-term e has a value in the λc -calculus, i.e. e is provably equivalent to somevalue (either a variable or a λ-abstraction), iff e has a value in the λv -calculus(λp -calculus)5Untyped λc-modelsIt is well-known that a categorical model for the untyped λ-calculus is a reflexiveobject D D D in a cartesian closed category (see [Sco80, Bar82]). In a λc -modelthere are two analogs for a reflexive object: VTV N (see [Ong88] V and NTT N for similar definitions in the context of partial cartesian closed categories).In the first case we have a model of call-by-value. In fact the elements of Vcorrespond to functions from values to computations (as VTV stands for V T V ), andtherefore an element can be applied to a computation e only after e has been evaluated . In the second case we have a model of call-by-name, since the elements of Ncorrespond to functions from computations to computations.The call-by-value and call-by-name interpretations are defined by induction onthe derivation of the untyped λ-term x1 , . . . , xn e (with let): Let G: VTV V be an isomorphism with inverse F , then the call-by-valueinterpretation of x1 , . . . , xn e is a morphism from V n to T V (see Table 9),because free variables range over values.10The general rules of sequent calculus (in [Sza69]), more precisely those for substitution andquantifiers, have to be modified slightly, because variables range over values. These modificationsare similar to those introduced in the logic of partial terms (see Section 2.4 in [Mog88]).14

We write [x: e] for the substitution of x with e in .E.xsubstΓ. x τΓ. e τΓ, x: τ. AΓ. A[x: e] is an equivalence relationcongrΓ. e1 e2 : τΓ. A[x: e1 ]Γ. A[x: e2 ]Table 5: General rulesWe write (let x e in e) for (let x1 e1 in (. . . (let xn en in e) . . .)), where n is the lenghtof the sequence x (and e). In particular, (let in e) stands for e.idcomplet.ξlet.βlet.fE.[ ]Γ. (let x e in x) e: τΓ. (let x2 (let x1 e1 in e2 ) in e) (let x1 e1 in (let x2 e2 in e)): τΓ. e1 e01 : τΓ, x: τ. e2 e02 : τ 0Γ. (let x e1 in e2 ) (let x e01 in e02 ): τ 0Γ. (let x1 x2 in e) e[x1 : x2 ]: τΓ. f (e) (let x e in f (x)): τΓ. [e] T τΓ. e e0 : τT.ξΓ. [e] [e0 ]: T τlet.µT.βT.ηΓ. µ(e) (let x e in µ(x)): τΓ. µ([e]) e: τΓ. [µ(x)] x: T τΓ. e τ and Γ. [e] (let x e in [x]): τ are interderivableTable 6: rules for let and computational types15x1 6 FV(e)

E. 1.ηE.h ilet.h iE.πilet.πi .β .ηΓ. 1Γ. x: 1Γ. hx1 , x2 i τ1 τ2Γ. he1 , e2 i (let x1 , x2 e1 , e2 in hx1 , x2 i): τ1 τ2Γ. πi (x) τiΓ. πi (e1 , e2 ) (let x1 , x2 e1 , e2 in πi (x1 , x2 )): τiΓ. πi (hx1 , x2 i) xi : τiΓ. hπ1 (x), π2 (x)i x: τ1 τ

Computational lambda-calculus and monads Eugenio Moggi LFCS Dept. of Comp. Sci. University of Edinburgh EH9 3JZ Edinburgh, UK [email protected] October 1988 Abstract The -calculus is considered an useful mathematical tool in the study of programmin