liboleg 2009.9.1 → 2010.1.1
raw patch · 3 files changed
+745/−1 lines, 3 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
+ Control.ExtensibleDS: (:@) :: e1 -> e2 -> App e1 e2
+ Control.ExtensibleDS: Add1 :: Add1
+ Control.ExtensibleDS: BE_err :: BE_err
+ Control.ExtensibleDS: BE_omega :: BE_omega
+ Control.ExtensibleDS: Control :: e -> Control e
+ Control.ExtensibleDS: ControlAdmin :: e -> ControlAdmin e
+ Control.ExtensibleDS: Deref :: e -> Deref e
+ Control.ExtensibleDS: InFX :: (Value -> Comp) -> Action -> Comp
+ Control.ExtensibleDS: InV :: !Value -> Comp
+ Control.ExtensibleDS: IntC :: Int -> IntC
+ Control.ExtensibleDS: Lam :: V -> e -> Lam e
+ Control.ExtensibleDS: Loc :: Int -> Loc
+ Control.ExtensibleDS: Ref :: e -> Ref e
+ Control.ExtensibleDS: Set :: e1 -> e2 -> Set e1 e2
+ Control.ExtensibleDS: StoAdmin :: Sto -> e -> StoAdmin e
+ Control.ExtensibleDS: V :: String -> V
+ Control.ExtensibleDS: VF :: (Value -> Value) -> Value
+ Control.ExtensibleDS: VI :: Int -> Value
+ Control.ExtensibleDS: VP :: Value -> Value -> Value
+ Control.ExtensibleDS: VS :: String -> Value
+ Control.ExtensibleDS: VT :: Tag -> Value -> Value
+ Control.ExtensibleDS: class Interpretor exp
+ Control.ExtensibleDS: class PL u
+ Control.ExtensibleDS: class PN u
+ Control.ExtensibleDS: class PV u
+ Control.ExtensibleDS: data Add1
+ Control.ExtensibleDS: data App e1 e2
+ Control.ExtensibleDS: data BE_err
+ Control.ExtensibleDS: data BE_omega
+ Control.ExtensibleDS: data Comp
+ Control.ExtensibleDS: data Control e
+ Control.ExtensibleDS: data ControlAdmin e
+ Control.ExtensibleDS: data Deref e
+ Control.ExtensibleDS: data IntC
+ Control.ExtensibleDS: data Lam e
+ Control.ExtensibleDS: data Ref e
+ Control.ExtensibleDS: data Set e1 e2
+ Control.ExtensibleDS: data StoAdmin e
+ Control.ExtensibleDS: data Value
+ Control.ExtensibleDS: inComp :: Comp -> Value
+ Control.ExtensibleDS: inControl :: (Value -> Comp) -> Value
+ Control.ExtensibleDS: inL :: (PL u) => Loc -> u
+ Control.ExtensibleDS: inN :: (PN u) => Int -> u
+ Control.ExtensibleDS: inP :: (PV u) => Proc -> u
+ Control.ExtensibleDS: inSto :: Sto -> Value
+ Control.ExtensibleDS: init_sto :: Sto
+ Control.ExtensibleDS: instance (Interpretor e) => Interpretor (Control e)
+ Control.ExtensibleDS: instance (Interpretor e) => Interpretor (ControlAdmin e)
+ Control.ExtensibleDS: instance (Interpretor e) => Interpretor (Deref e)
+ Control.ExtensibleDS: instance (Interpretor e) => Interpretor (Lam e)
+ Control.ExtensibleDS: instance (Interpretor e) => Interpretor (Ref e)
+ Control.ExtensibleDS: instance (Interpretor e) => Interpretor (StoAdmin e)
+ Control.ExtensibleDS: instance (Interpretor e1, Interpretor e2) => Interpretor (App e1 e2)
+ Control.ExtensibleDS: instance (Interpretor e1, Interpretor e2) => Interpretor (Set e1 e2)
+ Control.ExtensibleDS: instance Eq Loc
+ Control.ExtensibleDS: instance Eq V
+ Control.ExtensibleDS: instance Interpretor Add1
+ Control.ExtensibleDS: instance Interpretor BE_err
+ Control.ExtensibleDS: instance Interpretor BE_omega
+ Control.ExtensibleDS: instance Interpretor IntC
+ Control.ExtensibleDS: instance Interpretor V
+ Control.ExtensibleDS: instance PL Value
+ Control.ExtensibleDS: instance PN Value
+ Control.ExtensibleDS: instance PV Value
+ Control.ExtensibleDS: instance Show Comp
+ Control.ExtensibleDS: instance Show Loc
+ Control.ExtensibleDS: instance Show V
+ Control.ExtensibleDS: instance Show Value
+ Control.ExtensibleDS: interpret :: (Interpretor exp) => exp -> Env Value -> Comp
+ Control.ExtensibleDS: newtype Loc
+ Control.ExtensibleDS: newtype V
+ Control.ExtensibleDS: prComp :: Value -> Maybe Comp
+ Control.ExtensibleDS: prControl :: Value -> Maybe (Value -> Comp)
+ Control.ExtensibleDS: prL :: (PL u) => u -> Maybe Loc
+ Control.ExtensibleDS: prN :: (PN u) => u -> Maybe Int
+ Control.ExtensibleDS: prP :: (PV u) => u -> Maybe (Proc)
+ Control.ExtensibleDS: prSto :: Value -> Maybe Sto
+ Control.ExtensibleDS: type Action = Value
+ Control.ExtensibleDS: type Env v = V -> v
+ Control.ExtensibleDS: type Proc = Value -> Comp
+ Control.ExtensibleDS: type Sto = (Int, Loc -> Value)
+ Control.ExtensibleDS: type Tag = String
+ Control.ExtensibleDS: type Var = V
+ Control.ExtensibleDS: vf :: Var
+ Control.ExtensibleDS: vr :: Var
+ Control.ExtensibleDS: vx :: Var
+ Control.ExtensibleDS: vy :: Var
Files
- Control/ExtensibleDS.hs +527/−0
- Language/Symantics1.hs +216/−0
- liboleg.cabal +2/−1
+ Control/ExtensibleDS.hs view
@@ -0,0 +1,527 @@+{-# LANGUAGE PatternGuards #-}+-- |+-- Extensible Denotational Semantics+--+--+-- This work is a generalization of +-- /Extensible Denotational Language Specifications+-- Robert Cartwright, Matthias Felleisen+-- Theor. Aspects of Computer Software, 1994/+-- <http://citeseer.ist.psu.edu/69837.html>+--+-- to be referred to as EDLS.+--+-- We implement the enhanced EDLS in Haskell and add delimited control.+-- To be precise, we implement the Base interpreter (whose sole+-- operations are Loop and Error) and the following extensions: CBV+-- lambda-calculus, Arithmetic, Storage, Control. The extensions can be+-- added to the Base interpreter in any order and in any combination.+-- +-- Our implementation has the following advantages over EDLS:+--+-- * support for delimited control+-- * support for a local storage (including `thread-local' storage and+-- general delimited dynamic binding)+-- * extensions do not have to be composed explicitly, and so the+-- composition order truly does not matter. In the+-- original EDLS, one+-- had to write interpreter composition explicitly. In our approach, an+-- extension is pulled in automatically if the program includes the+-- corresponding syntactic forms. For example, if a program contains+-- storage cell creation and dereference operations, the Storage extension+-- will automatically be used to interpret the program.+--+-- Our main departure from EDLS is is the removal of the `central+-- authority'. There is no semantic `admin' function. Rather, admin is+-- part of the source language and can be used at any place in the+-- code. The `central authority' of EDLS must be an extensible function,+-- requiring meta-language facilities to implement (such as quite+-- non-standard Scheme modules). We do not have central+-- authority. Rather, we have bureaucracy: each specific effect handler+-- interprets its own effects as it can, throwing the rest `upstairs' for+-- higher-level bureaucrats to deal with. Extensibility arises+-- automatically.+-- +-- We take the meaning of a program to be the union of Values and+-- (unfulfilled) Actions. If the meaning of the program is a (non-bottom)+-- value, the program is terminating. If the meaning of the program is an+-- Action -- the program finished with an error, such as an action to+-- access a non-existing storage cell, or shift without reset, or a+-- user-raised error.+-- +-- Incidentally, EDLS stresses on p. 2 (the last full paragraph) that+-- their schema critically relies on the distinction between a complete+-- program and a nested program phrase. Our contribution (which is the+-- consequence of removing the central admin, making it first-class) is+-- eliminating such a distinction! EDLS says, at the very top of p. 3,+-- that the handle in the effect message ``is roughly a conventional+-- continuation.'' Because the admin of EDLS is `outside' of the program+-- (at the point of infinity, so to speak), its continuation indeed+-- appears undelimited. By making our `admin' a part of the source+-- language, we recognize the handle in the effect message for what it+-- is: a _delimited_ continuation.+-- +-- As we see below, the Control aspect is orthogonal to the CBV+-- aspect. So, we can just as easily replace the CBV extension with the+-- CBN extension, which will give us the denotation of delimited control+-- in CBN.+-- +-- +-- We shall be using Haskell to express denotations, taking advantage of+-- the fact that Haskell values are `lifted'. See also the remark on p21+-- of EDLS: someone (ref. [4]) showed that sets and partial functions can+-- suffice...+-- +-- +-- Our program denotations are stable: they have the same form regardless+-- of a particular composition of modular interpreters. See Section 3.5+-- of EDLS for precise formulation (and the last paragraph of Section 3.4+-- for concise informal statement of stability). Also see the comparison+-- with the monads on p. 20: different monads assign numeral radically+-- different meanings, depending on the monad. But in EDLS, a numeral has+-- exactly the same denotation.+-- +-- The meaning of an expression is also the same and stable, no matter+-- what the interpreter is: it is a function from Env to Computations+-- (the latter being the union of values and unfulfilled effects -- the+-- same union mentioned above).+-- +-- However, by using handlers, some effect messages can be subtracted:+-- so, strictly speaking, the denotation of a fragment is V ++-- effect-message-issued - effect-messages handled. There seem to be a+-- connection with effect systems.+-- +-- +-- Additional notes on EDLS:+-- +-- The abstract and p. 2 (especially the last full paragraph) are+-- so well-written!+-- +-- p. 5, bottom: ``It [ref \x.x, where ref means what it does in ML] +-- is a closed expression that does not diverge, is not a value, and+-- cannot be reduced to a value without affecting the context. We refer+-- to such results as _effects_.''+-- +-- Beginning of Section 3 and App A give a very good introduction+-- to the denotational semantics.+-- +-- p. 6: ``Algebraically speaking, the interpreter is (roughly) a+-- homomorphism from syntax to semantics''+-- +-- ``A straightforward representation of an evaluation context is a+-- function from values to computations, which directly corresponds to+-- its operational usage as a function from syntactic values to+-- expressions.'' (p. 8). EDLS then notices that the `handle' has+-- the same type as the denotation of a context. Footnote 6 notes that+-- handler is roughly the composition combinator for functions from values+-- to computations [contexts!] and it superficially relates to [bind]+-- but does not satisfy all monad laws.+-- +-- The last of EDLS Sec 3.5, p. 15: ``Informally speaking, this property+-- [stable denotations] asserts that in the framework of extensible+-- semantics, the addition of a programming construct corresponds to the+-- addition of a new ``dimension'' to the space of meaning. [The+-- equations, featuring injection and projection functions, make that+-- precise and clear.] The reader may want to contrast this general+-- statement with the numerous papers on the relationship between direct+-- and continuation semantics.''+-- +-- The practical consequence of the lack of stability of denotations for+-- monads is that monadic transformers put layers upon layers of thunks,+-- which have to be carried over _in full_ from one sub-expression into+-- the other, even if no single subexpression uses all of the features.+-- +-- The present code is not written in idiomatic Haskell and does not take+-- advantage of types at all. The ubiquitous projections from the+-- universal domain tantamount to ``dynamic typing.'' The code is+-- intentionally written to be close to the EDLS paper, emphasizing+-- denotational semantics (whose domains are untyped). One can certainly+-- do better, for example, employ user-defined datatypes for tagged+-- values, avoiding the ugly string-tagged VT.+--++module Control.ExtensibleDS where++import Data.Maybe++------------------------------------------------------------------------+-- The base interpreter+++-- | The universal domain+-- Yes, it is untyped... But Denot semantics is like this anyway...+-- Bottom is the implicit member of this domain.+data Value = VI Int -- integers+ | VS String -- strings+ | VP Value Value -- pairs+ | VF (Value -> Value) -- functions+ | VT Tag Value -- tagged value++type Tag = String++type Action = Value -- only differently tagged++instance Show Value where+ show (VI x) = show x+ show (VS x) = show x+ show (VT tag v) = "{"++show tag++" "++show v++"}"+ show (VP x1 x2) = show (x1,x2)+ show (VF _) = "<procedure>"++++-- | Computations: just like in EDLS+-- The strictness of inV guarantees that inV bottom = bottom, as+-- on Fig. 3 of EDLS+-- Error is always a part of the computation+--+data Comp = InV !Value | InFX (Value -> Comp) Action++instance Show Comp where+ show (InV v) = show v+ show (InFX _ a) = "Effect: " ++ show a+++-- | Auxiliary functions+newtype V = V String deriving (Eq, Show) -- Variables+type Env v = V -> v+empty_env x = error $ "impossible: an open program? var " ++ show x+ext_env env x v y | x == y = v+ext_env env x v y = env y+++-- | Note that inV is essentially the identity `partial' continuation+inAC action = InFX InV action++-- | The error `raise' action and its tag+tagErr = "Err"+raise err = inAC $ VT tagErr (VS err)++-- | The universal handler of actions+-- It propagates the action request InFX up.+-- Since we do case-analysis on the first argument, v, the handler+-- is strict in that argument. That is, handler bottom ==> bottom,+-- as required by Fig. 3 of EDLS.+-- The last clause is essentially the denotation of a `control channel'+handler (InV v) k = k v+handler (InFX ka a) k = InFX (\v -> handler (ka v) k) a+++-- | Expressions and their interpretations+-- This is an open data type and an open function. Haskell typeclasses+-- are ideal for that.+--+-- This is the function \curlyM of EDLS+class Interpretor exp where+ interpret :: exp -> Env Value -> Comp++-- | The base language has only two expressions: omega and error+-- See Fig. 3 (p. 7) of EDLS+--+data BE_err = BE_err+data BE_omega = BE_omega++instance Interpretor BE_omega where+ interpret _ _ = InV undefined++instance Interpretor BE_err where+ interpret _ _ = raise "error action"++-- | The meaning of a program+prog p = interpret p empty_env+++-- ----------------------------------------------------------------------+-- | Extension: Call-by-Value: see a part Fig. 4 of EDLS (or, Fig. 8)+--+-- We add closures (procedures) to the Base+type Proc = Value -> Comp++class PV u where -- and the corresponding injection/+ inP :: Proc -> u -- projection functions+ prP :: u -> Maybe (Proc)+++type Var = V+data Lam e = Lam V e+data App e1 e2 = e1 :@ e2+infixl 1 :@++instance Interpretor V where+ interpret v env = InV (env v)++instance Interpretor e => Interpretor (Lam e) where+ interpret (Lam x e) env = InV (inP (\d -> interpret e (ext_env env x d)))++instance (Interpretor e1, Interpretor e2) => Interpretor (App e1 e2) where+ interpret (e1 :@ e2) env =+ handler (interpret e1 env) $+ \f -> handler (interpret e2 env) $+ \a -> maybe (raise "InP expected") (\g -> g a)+ (prP f)+++-- | Create a few variables for use in examples+vx, vy, vr, vf :: Var+(vx,vy,vr,vf) = (V "x", V "y", V "r", V "f")++-- Test of the extension+-- Instantiate this extension on the top of the base language+--+-- | Denotations of the new actions (inj/proj to/from the Universal Domain)+tagProc = "Proc"+tagCompV = "CompV"+tagCompE = "CompE"++-- | inject and project computations+inComp :: Comp -> Value+inComp (InV v) = VT tagCompV v+inComp (InFX k a) = VT tagCompE (VP (VF (inComp . k)) a)++prComp :: Value -> Maybe Comp+prComp (VT tag v) | tag == tagCompV = Just (InV v)+prComp (VT tag v) | tag == tagCompE = pr v+ where pr (VP (VF k) a) = Just $ InFX (fromJust . prComp . k) a+ pr _ = Nothing+prComp _ = Nothing+++instance PV Value where+ inP f = VT tagProc (VF (inComp . f))+ prP (VT tag (VF k)) | tag == tagProc = Just $ fromJust . prComp . k+ prP _ = Nothing++test1 = Lam vx (vx :@ BE_err)++test1e = prog test1+-- {"Proc" <procedure>}+++------------------------------------------------------------------------+-- | Extension: Arithmetic: see a part Fig. 4 of EDLS +--+class PN u where -- inj/proj for numbers+ inN :: Int -> u+ prN :: u -> Maybe Int++data IntC = IntC Int -- an integer constant+data Add1 = Add1++instance Interpretor IntC where+ interpret (IntC v) _ = InV (inN v)++instance Interpretor Add1 where+ interpret Add1 _ = InV (inP $+ \v -> maybe (raise "InN expected")+ (InV . inN . succ)+ (prN v))+++add1 x = Add1 :@ x++-- | Test of the extension+-- Instantiate this extension on the top of the CBV evaluator+--+instance PN Value where+ inN n = VI n+ prN (VI n) = Just n+ prN _ = Nothing+++test2 = (Lam vx $ add1 vx) :@ (IntC 1)+test2e = prog test2+-- 2++------------------------------------------------------------------------+-- | Extension: State: see Fig. 5 of EDLS +--+newtype Loc = Loc Int deriving (Eq, Show) -- locations++class PL u where+ inL :: Loc -> u+ prL :: u -> Maybe Loc++-- | a better idea is Loc -> Maybe Value, so that when lookup fails,+-- we can re-throw that Deref or Set message. That would make the+-- storage extensible...+-- The first component of the pair is the allocation counter+type Sto = (Int, Loc -> Value) ++tagSto = "Storage"++inSto :: Sto -> Value+inSto (cnt, st) = VT tagSto (VP (VI cnt) (VF (st . fromJust . prL)))+prSto :: Value -> Maybe Sto+prSto (VT tag (VP (VI cnt) (VF k))) | tag == tagSto = Just (cnt, k . inL)+prSto _ = Nothing++init_sto :: Sto+init_sto = (0,\l->undefined)+++-- data StoAct v = InRef v | InDer Loc | InSet Loc v++-- | new expressions+data Ref e = Ref e+data Deref e = Deref e+data Set e1 e2 = Set e1 e2++-- | Denotations of the new actions (inj/proj to/from the Universal Domain)+tagInRef = "Ref"+tagInDer = "Deref"+tagInSet = "Set"++inRef v = VT tagInRef v+prRef (VT tag v) | tag == tagInRef = Just v+prRef _ = Nothing++inDer v = VT tagInDer (inL v)+prDer (VT tag v) | tag == tagInDer = prL v+prDer _ = Nothing++inSet l v = VT tagInSet (VP (inL l) v)+prSet (VT tag (VP l v)) | tag == tagInSet = fmap (\l -> (l,v)) (prL l)+prSet _ = Nothing++++instance Interpretor e => Interpretor (Ref e) where+ interpret (Ref e) env = handler (interpret e env) $+ \v -> inAC(inRef v)+++instance Interpretor e => Interpretor (Deref e) where+ interpret (Deref e) env = handler (interpret e env) $+ \v -> maybe (raise "InL expected")+ (inAC . inDer)+ (prL v)++instance (Interpretor e1, Interpretor e2) => Interpretor (Set e1 e2) where+ interpret (Set e1 e2) env = handler (interpret e1 env) $+ \l -> handler (interpret e2 env) $+ \v -> maybe (raise "InL expected")+ (\l -> inAC (inSet l v))+ (prL l)+++-- | Now we need a storage admin+-- It is treated as an expression in the source language!+--+data StoAdmin e = StoAdmin Sto e++instance Interpretor e => Interpretor (StoAdmin e) where+ interpret (StoAdmin sto e) env = sto_handler sto (interpret e env) InV+++sto_handler (cnt,st) (InFX k a) f | Just v <- prRef a = + let l = Loc cnt+ sto = (cnt+1, \l' -> if l' == l then v else st l')+ in sto_handler sto (k (inL l)) f+sto_handler sto@(cnt,st) (InFX k a) f | Just l <- prDer a = + sto_handler sto (k (st l)) f+sto_handler (cnt,st) (InFX k a) f | Just (l,v) <- prSet a = + sto_handler (cnt, \l' -> if l' == l then v else st l') (k (inL l)) f++sto_handler sto (InV v) f = f (VP v (inSto sto)) -- normal return+-- Propagate everything else+sto_handler sto (InFX k a) f = InFX (\v -> sto_handler sto (k v) f) a++ +tagLoc = "Loc"++instance PL Value where+ inL (Loc l) = VT tagLoc (VI l)+ prL (VT tag (VI l)) | tag == tagLoc = Just (Loc l)+ prL _ = Nothing+++-- Test of the extension+-- Note that we can use several local storages!+++test3 = (Lam vr $ Lam vf $ vf :@ (Deref vr)) :@+ (Ref (IntC 1)) :@ (Lam vx $ add1 vx)++-- we forgot the Admin..., so the program terminates with an effect+test31 = prog test3 +-- Effect: {"Ref" 1}++test32 = prog (StoAdmin init_sto test3)+-- (2,{"Storage" (1,<procedure>)})++test33 = prog (StoAdmin init_sto + ((Lam vr $ (Lam (V "_") (Deref vr)) :@ (Deref (Set vr (IntC 2))))+ :@ (Ref (IntC 1))))+-- (2,{"Storage" (1,<procedure>)})++------------------------------------------------------------------------+-- Extension: Delimited continuation+-- That is new compared to EDLS++-- new effect message: Control ((Value->Comp)->Comp)+tagControl = "Control"++inControl :: (Value->Comp) -> Value+inControl f = VT tagControl (VF (inComp . f))+prControl :: Value -> Maybe (Value->Comp)+prControl (VT tag (VF f)) | tag == tagControl = Just (fromJust . prComp . f)+prControl _ = Nothing+++data Control e = Control e++instance Interpretor e => Interpretor (Control e) where+ interpret (Control e) env = handler (interpret e env) $+ \a -> maybe (raise "InP expected")+ (\f -> inAC(inControl f))+ (prP a)++-- The administrator here is prompt, quite unsurprisingly++data ControlAdmin e = ControlAdmin e++instance Interpretor e => Interpretor (ControlAdmin e) where+ interpret (ControlAdmin e) env = ctl_handler (interpret e env) InV+++ctl_handler (InFX k a) f | Just e <- prControl a = + ctl_handler (e (inP k)) f++ctl_handler (InV v) f = f v -- normal return+-- Propagate everything else+ctl_handler (InFX k a) f = InFX (\v -> ctl_handler (k v) f) a++-- Ken's tests++control v e = Control (Lam (V v) e)+prompt e = ControlAdmin e+succ0 = (add1 (IntC 0))++-- if we forget Reset...+test41 = prog $ add1 (Control (Lam vf succ0))+-- Effect: {"Control" <procedure>}++test42 = prog $ prompt (add1 (control "f" succ0))+-- 1++test43 = prog $ prompt (add1 (control "f" (vf :@ succ0)))+--2++test44 = prog $ prompt (add1 (add1 (control "f" (vf :@ succ0))))+-- 3++test45 = prog $ prompt (add1 (add1 (control "f" + (vf :@ (vf :@ succ0)))))+-- 5++test46 = prog $ prompt (add1 ((Lam vx (add1 vx)) :@+ (control "f" (vf :@ (vf :@ succ0)))))++-- 5+test47 = prog $ prompt (add1 ((Lam vx (control "f" (IntC 0))) :@+ (control "f" (vf :@ (vf :@ succ0)))))+-- 0++test48 = prog $ add1 (prompt ((Lam vx (control "f" (IntC 0))) :@+ (control "f" (vf :@ (vf :@ succ0)))))+-- 1
+ Language/Symantics1.hs view
@@ -0,0 +1,216 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE Rank2Types, GeneralizedNewtypeDeriving #-}+{-# LANGUAGE NoMonomorphismRestriction, EmptyDataDecls #-}++-- This is the Haskell version of symantics1.ml, for comparison+-- ACG with a more expressive semantic lexicon that includes+-- multi-prompt delimited continuations and the notion of evaluation.+-- Types are considered as a mere approximation rather than+-- the complete specification of grammatical composition.+--+-- * <http://okmij.org/ftp/gengo/index.html#CAG>+--++module Language.Symantics1 where++-- Part of the Dybvig, Sabry, Peyton-Jones' library+-- for multi-prompt delimited control+import CC_Frame -- ed. I don't know where this is.+import Control.Monad.Reader++-- The abstract form, to be interpreted in several ways.++-- | Abstract signature, which defines base types, constants and their types+--+data N -- Base types+data NP+data S+data SM++-- | An interpretation of the base type btyp in the signature+-- labeled by lab+type family I lab btyp ++class Abstract c where+ john :: c (I c NP) -- constants+ bill :: c (I c NP)++ man :: c (I c N)+ woman :: c (I c N)+ see :: c (I c NP) -> c (I c NP) -> c (I c S)+ love :: c (I c NP) -> c (I c NP) -> c (I c S)++ every :: c (I c N) -> c (I c NP)+ some :: c (I c N) -> c (I c NP)++ dot :: c (I c S) -> c (I c SM) -- Terminating dot++{-+ everyone :: c (I c NP)+ someone :: c (I c NP)++-}+++-- Sample phrases in the abstract language++-- term1 = see someone everyone++-- | Example from Sec 4.3 of the ESSLLI Advanced ACG course.+term43 = dot (love (some woman) (every man))+++-- | An interpretation of the abstract signature as the surface form: strings+--+newtype LString a = LString a deriving Show++-- All base type are interpreted as strings+type instance I LString N = String+type instance I LString NP = String+type instance I LString S = String+type instance I LString SM = String++ccat :: LString String -> LString String -> LString String+ccat (LString a) (LString b) = LString (a ++ b)++instance Abstract LString where+ john = LString "John"+ bill = LString "Bill"+ man = LString "man"+ woman = LString "woman"++ every = \x -> LString "every " `ccat` x+ some = \x -> LString "some " `ccat` x+ see = \o s -> s `ccat` LString " saw " `ccat` o+ love = \o s -> s `ccat` LString " loves " `ccat` o++ dot = \s -> s `ccat` LString "."+++-- Surface forms of sample terms+term43S = case term43 of LString x -> x++-- ------------------------------------------------------------------------+-- | Semantic forms+--+data E = Ind String deriving Show+data T = Man E+ | Woman E+ | See E E+ | Love E E+ | And T T+ | Imply T T+ | Exists Varname T+ | Forall Varname T+ deriving Show+type Varname = String+++-- We now build the semantic signature and the lexicon -- stepwise++-- | The order of quantification+data QuantOrder = Uni_over_Exi | Exi_over_Uni++data SemEnv r = + SemEnv{puni :: Prompt r T,+ pexi :: Prompt r T,+ quant_order :: QuantOrder,+ pcnt :: Prompt r (Int -> CC r T) -- to generate variable names+ }++-- | The Semantic monad+newtype SemM r a = SemM (ReaderT (SemEnv r) (CC r) a)+ deriving Monad++unSem :: SemM r a -> SemEnv r -> CC r a+unSem (SemM m) env = runReaderT m env++-- | Interpretation of Basic types+type instance I (SemM r) NP = E+type instance I (SemM r) N = E -> T+type instance I (SemM r) S = T+type instance I (SemM r) SM = T++instance Abstract (SemM r) where+ john = return $ Ind "John'"+ bill = return $ Ind "Bill'"+ man = return Man+ woman= return Woman+ love = \o s -> (return Love) `ap` o `ap` s+ see = \o s -> (return See) `ap` o `ap` s++ every pred = pred >>= \pr -> + make_ind_quant puni (\vn x -> + return $ Forall vn $ Imply (pr (Ind vn)) x)+ some pred = pred >>= \pr -> + make_ind_quant pexi (\vn x -> + return $ Exists vn $ And (pr (Ind vn)) x)++ dot m = SemM $ do+ env <- ask+ lift $ do+ case quant_order env of+ Uni_over_Exi -> + pushPrompt (puni env) $+ pushPrompt (pexi env) (unSem m env)+ Exi_over_Uni -> + pushPrompt (pexi env) $+ pushPrompt (puni env) (unSem m env)++runSem :: QuantOrder -> (forall r. SemM r T) -> T+runSem qorder m = runCC init+ where+ init = do+ uni <- newPrompt+ exi <- newPrompt+ cnt <- newPrompt+ -- initialize to 0 the counter to create variable names+ pushPrompt cnt (do+ v <- unSem m (SemEnv{puni=uni, pexi=exi, quant_order=qorder, pcnt=cnt})+ return $ const (return v)) `app` (return 0)++-- | /Movement/ into the position of the prompt selected by psel+make_ind_quant psel body = do+ vn <- genvar+ let v = Ind vn+ SemM $ do+ env <- ask+ lift $ shiftP (psel env) $ \sk -> + body vn =<< sk (Ind vn)++-- | Logical forms of sample terms in different semantic environment+term43L1 = runSem Uni_over_Exi term43+{-+ Forall "v1" (Imply (Man (Ind "v1")) + (Exists "v0" (And (Woman (Ind "v0")) + (Love (Ind "v0") (Ind "v1")))))+-}++term43L2 = runSem Exi_over_Uni term43+{-+ Exists "v0" (And (Woman (Ind "v0")) + (Forall "v1" (Imply (Man (Ind "v1")) + (Love (Ind "v0") (Ind "v1")))))+-}+++-- | Auxiliary functions+--+app :: Monad m => m (a -> m b) -> m a -> m b+app m1 m2 = (m1 `ap` m2) >>= id++-- | Generate a new variable name+genvar :: SemM r Varname+genvar = SemM $ do+ env <- ask+ cnt <- lift $ shiftP (pcnt env) $ \sk ->+ return $ \cnt -> sk cnt `app` (return (succ cnt))+ return $ "v" ++ show cnt+++shiftP :: Prompt r b -> ((a -> CC r b) -> CC r b) -> CC r a+shiftP p f = letSubCont p $ \sk -> + pushPrompt p (f (\v -> + pushPrompt p (pushSubCont sk (return v))))++
liboleg.cabal view
@@ -1,5 +1,5 @@ name: liboleg-version: 2009.9.1+version: 2010.1.1 license: BSD3 license-file: LICENSE author: Oleg Kiselyov@@ -28,6 +28,7 @@ Control.CaughtMonadIO Control.ShiftResetGenuine Control.VarStateM+ Control.ExtensibleDS Codec.Image.Tiff