1

Semantic LegoDavid Espinosa
Department of Computer Science
Columbia University
New York, NY 10027
espinosa@cs.columbia.edu
March 31, 1995

2

Semantic Lego
SL builds interpreters from parts.
Based on denotational semantics
Covers all of Schmidt (1986)
Implemented in Scheme
Why? To study
Languages
Semantics
Modularity
Extensibility

3Contributions
Re-present programming languages as ADTs.
Re-present Moggi's theory of lifting.
Develop two styles of hand-written modular interpreters.
Develop theory of stratication (extends Mosses).
Implement theory of lifting.
Implement theory of stratication.

4Outline* Usual interpreters aren't modular
Modular interpreters by hand
Modular interpreters by machineTechnical aspects
Conclusion

5Languages as ADTs
compute: Exp! Ans%num%+: Num: Exp  Exp! Exp! Exp%abort: Exp! Exp%var%lambda%call: Name! Exp: Name  Exp ! Exp: Exp  Exp ! Exp(compute(%call (%lambda 'x (%+ (%var 'x) (%var 'x)))(%abort (%num 5))))=> 5

6An implementation
Den = Env -> Cont -> Ans
Proc = Val -> Cont -> Ans
Cont = Val -> Ans(define (compute den)((den (empty-env)) val->ans))(define (((%num n) env) k)(k n))(define (((%+ d1 d2) env) k)((d1 env)(lambda (v1)((d2 env)(lambda (v2) (k (+ v1 v2)))))))(define (((%var name) env) k)(k (env-lookup env name)))(define (((%lambda name den) env) k)(k (lambda (val) (den (env-extend env name val)))))(define (((%call d1 d2) env) k)((d1 env)(lambda (v1)((d2 env)(lambda (v2)((v1 v2) k))))))(define (((%abort den) env) k)((den env) val->ans))

7Problems
Not modular!
Each construct involves all modules.
Hard to understand and reason about.
Denitions are too specialized.

8Outline
Usual interpreters aren't modular* Modular interpreters by hand
Modular interpreters by machineTechnical aspects
Conclusion

9

Computation ADTs
Split language denitions into two parts:
Computation ADT denes the \basic semantics",
a type of denotations and operators on it.
Language ADT denes the actual constructs, as before.
Reference: Mosses

10Strati cation
Computation ADT is built from:a set of levels
a set of lifting operators relating levels

11Levels
Type constructors:
E (A) = Env ! (A ! Ans) ! Ans
C (A) = (A ! Ans) ! Ans
V (A) = A

12

Lifting operators 1
Monad = (T , unit, bind)Type constructor T
Families of maps:
unit : A ! T (A)bind : (A ! T (B )) ! (T (A) ! T (B ))bind(unit)= idbind(f) o unit
= fbind(g) o bind(f) = bind(bind(g) o f))

13Lifting operators 2
Monad = (T , unit, join)
Endofunctor T :map : (A ! B ) ! (T (A) ! T (B ))Natural transformations:
unit : A ! T (A)join : T (T (A)) ! T (A)join o unit= id
join o map(unit) = id
join o map(join) = join o join

14

Monad examples 1 T(A) = List(A)(define (unit a)(list a))(define ((map f) ta)(list-map f ta))(define ((bind f) ta)(append-map f ta))(define (join tta)
(reduce append '() tta))

15

Monad examples 2 T(A) = Env -> A(define ((unit a) env)a)(define (((map f) ta) env)
(f (ta env)))(define (((bind f) ta) env)((f (ta env)) env))(define ((join tta) env)((tta env) env))

16

Monads relate levels
A monad T relates L1 to L2 if

L2 = T  L1
V is related to C by the continuation monad.
C is related to E by the environment monad.
V is related to E by a combined monad.

17

Example monads
MonadAction T (A) =Identity
AListsList (A)
Lifting
1!AEnvironments Env ! AStoresSto ! A  Sto
Exceptions A + X
MonoidsAM
Continuations (A ! Ans ) ! Ans
Resumptions x (X ) (A + X )18Monads in use(define (%+ d1 d2)(bindVE d1(lambda (n1)(bindVE d2(lambda (n2)(unitVE (+ n1 n2)))))))

19

Computation ADT
E(A) = Env -> C(A)C(A) = (A -> Ans) -> Ans
V(A) = A
unitAB : A -> B
bindAB : B * (A -> B) -> B
(define ((unitVC v) k)(k v))(define ((unitCE c) env)c)(define (unitVE v)(unitCE (unitVC v)))(define ((bindVC c f) k)(c (lambda (v) ((f v) k))))(define ((bindCE e f) env)((f (e env)) env))(define ((bindVE e f) env)
(bindVC (e env)
(lambda (v) ((f v) env))))

20

Language ADT
Proc = V -> C(define (compute den)((den (empty-env)) val->ans))(define (%num n) (unitVE n))(define (%+ d1 d2)(bindVE d1(lambda (n1)(bindVE d2(lambda (n2)(unitVE (+ n1 n2)))))))(define ((%var name) env)
(unitVC (env-lookup env name)))(define ((%lambda var den) env)
(unitVC (lambda (val) (den (env-extend env var val)))))(define (%call d1 d2)(bindVE d1(lambda (p)(bindVE d2 (lambda (a) (unitCE (p a)))))))(define (%abort den)(bindCE den(lambda (c)(unitCE (lambda (k) (c val->ans))))))

21

Outline
Usual interpreters aren't modular
Modular interpreters by hand
* Modular interpreters by machineTechnical aspects
Conclusion

22

Kitchen sink language
compute%unit%true%false%num%+, %*%=?, %>?
%or, %and%not%number?
%boolean?
%callcc%amb%fail%while%if%begin%store%fetch%var%lambda%let%fix%rec%letrec%write%error%pair%left%right: Exp: 1: 1: 1: Num: Exp Exp
: Exp Exp
: Exp Exp
: Exp: Exp: Exp: Exp: Exp Exp
: 1: Exp Exp: Exp Exp Exp: Exp Exp
: Loc Exp
: Loc
: Name: Name Exp: Name Exp Exp
: Exp
: Exp
: Name Exp Exp: Exp: String: Exp Exp
: Exp
: Exp! Ans! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp! Exp23

Kitchen sink example program(compute(%begin(%store 'n (%amb (%num 4) (%num 5)))(%store 'r (%num 1))(%callcc(%lambda 'exit(%letrec 'loop(%lambda 'u(%begin(%if (%zero? (%fetch 'n))(%call (%var 'exit) (%fetch 'r))(%unit))(%write (%pair (%fetch 'n) (%fetch 'r)))(%store 'r (%* (%fetch 'r) (%fetch 'n)))(%store 'n (%- (%fetch 'n) (%num 1)))(%call (%var 'loop) (%unit))))(%call (%var 'loop) (%unit)))))))(value: (24 120)
output: ((pair 4 1) (pair 3 4) (pair 2 12) (pair 1 24)(pair 5 1) (pair 4 5) (pair 3 20)(pair 2 60) (pair 1 120)))

24

Language speci cations
Input:
A list of (predened) semantic modules
Output:An interpreter
Interpreter is used to
Execute programs
Produce semantics via program simplier25

Kitchen sink speci cation(define computations(construct-typecbn-environments
lifting1
storescontinuations1
listsoutputerrors))(show-computations)(-> Env(Lift (-> Sto(Let A0 (+ (* (List Ans) Out) Err)(-> (-> (* Val Sto) A0) A0)))))(load "error-exceptions" "numbers" "booleans" "products""procedures" "environments" "begin" "stores" "while""callcc" "amb" "output" "fix")26

Generic %amb
(define %amb
(let ((unit (get-unit 'lists 'top))(bind (get-bind 'lists 'top)))(lambda (x y)(bind x(lambda (x)(bind y(lambda (y)(unit (append x y)))))))))

27

Generic %callcc(define %callcc(let ((mapC (get-map 'conts 'top))(mapK (get-map 'conts 'env-results))(iunitK (get-iunit 'conts 'env-results))(unitE (get-unit 'env-values 'env-results))(unitP (get-value-unit 'procedures 'env-values))(unitR (get-unit 'cont-values 'env-results))(bindS (get-value-bind 'procedures 'env-results)))(define (tilt cv f)(iunitK (bindS (unitR cv) f)))(lambda (exp)(mapC exp
(lambda (cont)(lambda (k)(define (callcc-proc v)(mapK (unitE v)(lambda (cont)(lambda (k1) (cont k)))))(cont(lambda (cv)((tilt cv(lambda (p)(p (unitP callcc-proc))))k)))))))))

28

Simpli ed constructs
Den = Env ! (Val ! List (Ans )) ! List (Ans )(define (%amb x y)(lambda (env)(lambda (k)(reduce append ()(map k (append ((x env) list)((y env) list)))))))(define (%callcc den)(lambda (env)(lambda (k)(define (callcc-proc v)(lambda (k1) (k v)))((den env)
(lambda (cv)(if (is? 'procedures cv)(((value cv)(in 'procedures callcc-proc)) k)(k (in 'errors(type-error'procedures (type cv))))))))))

29

Resumption example
Den = x (X ) Sto ! List ((Val + X )  Sto )(define computations(make-computations resumptions stores lists))(compute(%par (%num 1) (%num 2) (%num 3)))
(3 3 2 2 1 1)(compute(%seq(%store 'x (%num 1))(%store 'go (%true))(%par(%store 'go (%false))(%while (%and (%fetch 'go)(%< (%fetch 'x) (%num 7)))(%pause (%store 'x (%1+ (%fetch 'x))))))(%fetch 'x)))(1 2 3 4 5 6 7 7)

30Outline
Usual interpreters aren't modular
Modular interpreters by hand
Modular interpreters by machine* Technical aspects
Conclusion

31

Monads don't compose
Suppose we have:unitS
unitT
joinS
joinT

: Id ! S: Id ! T: SS ! S: TT ! T

We want:
joinST

Can't dene it!

: STST ! ST

32

Monad transformers
Transformer Action F (T )(A) =Identity
T (A)
Lists
T (List (A))
Lifting 1
1 ! T (A)
Lifting 2
T (1 ! A)
Environments Env ! T (A)StoresSto ! T (A  Sto )Exceptions T (A + X )Monoids
T (A  M )Continuations (A ! T (Ans )) ! T (Ans )Resumptions x (X ) T (A + X )33Monad transformer types
Type Form
ExamplesTop
F (T ) = S  T
Environments
Bottom F (T ) = T  U
Lists, Monoids
Around F (T ) = S  T  U Stores

34

Strati ed example 1
Let's build:
Den = Env ! Sto ! List (Val  Sto )Start with:

L1(A) = A
T11(A) = A

35

Strati ed example 2
Apply F (T )(A) = T (List (A)):

L2(A) = List (A)L1(A) = A
T12(A) = List (A)36Strati ed example 3
Apply F (T )(A) = Sto ! T (A  Sto ):L4(A) = Sto ! List (Sto  A)
L3(A) = List (Sto  A)
L2(A) = Sto  A
L1(A) = A
T34(A) = Sto ! A
T23(A) = List (A)
T24(A) = Sto ! List (A)T14(A) = Sto ! List (Sto  A)

37

Strati ed example 4
Apply F (T )(A) = Env ! T (A):L5(A) = Env ! Sto ! List (Sto  A)
L4(A) = Sto ! List (Sto  A)
L3(A) = List (Sto  A)
L2(A) = Sto  A
L1(A) = A
T45(A) = Env ! A
T34(A) = Sto ! A
T23(A) = List (A)
T35(A) = Env ! Sto ! A
T24(A) = Sto ! List (A)
T25(A) = Env ! Sto ! List (A)T14(A) = Sto ! List (Sto  A)
T15(A) = Env ! Sto ! List (Sto  A)

38

Compatibility laws
ST = S o T
map = mapS o mapT
unitST = unitS o unitT= mapS(unitT) o unitS : Id -> ST
joinST o mapST(unitS) = mapS(joinT) : STT -> ST
joinST o mapS(unitT) = joinS: SST -> ST
joinS o mapS(joinS)= joinST o joinS: SSTST -> ST

joinST o mapST(mapS(joinT))= mapS(joinT) o joinST : STSTT -> ST

References: Beck, Barr

39

Strati ed monads
Categories in which:Objects = levels (type constructors)
Arrows = monads T with L2 = T  L1
Composition respects compatibility.
All diagrams commute.
Distinguished levels Top and Bot that are maximal andminimal.
Distinguished monad T from Bot to Top.

40

Outline
Usual interpreters aren't modular
Modular interpreters by hand
Modular interpreters by machineTechnical aspects* Conclusion

41Limitations
SL builds basic denotational models.
Doesn't do compilation or abstract interpretation.
Doesn't help with static aspects (types, syntax).
Doesn't help with non-semantic aspects(unication, constraint solving).

42

Future work
Extend to do compilation and abstract interpretation.
Develop modular systems for reasoning about programs.

43

Previous work 1
ADTs in semantics:
Goguen, Thatcher, Wagner, and Wright, \Initial algebra
semantics and continuous algebras", 1977.
Mosses, \Action Semantics", 1983 { 92.
Monadic interpreters:
Moggi, \Computational lambda calculus and monads",
1989.
Moggi, \Notions of computation and monads", 1991.
Wadler, \The essence of functional programming", 1992.
Composing monads:
Beck, \Distributive laws", 1969.
Barr and Wells, \Triples, Toposes, and Theories", 1985.
King and Wadler, \Combining monads", 1992.
Jones and Duponcheel, \Composing monads", 1993.

44

Previous work 2
Compound interpreters:
Moggi, \An abstract view of programming languages",
1989.
Moggi, \A modular approach to denotational semantics",
1991.
Moggi and Cenciarelli, \A syntactic approach to modularity in denotational semantics", 1993.
Cartwright and Felleisen, \Extensible Denotational Language Specications", 1994.
Steele, \Building interpreters by composing monads",
1994.
Espinosa, \Semantic Lego", 1994.
Espinosa, \Stratied Monads", 1994.
Liang, Hudak, and Jones, \Monad transformers and modular interpreters", 1995.
Espinosa, Ph.D. thesis, 1995.