Sterling Example: stlc:pair

File: pair.sos

[Reduce File] [Raw File]

Module stlc:pair

Builds on stlc:host


/*New syntax*/
term ::= ...
       | pair(term, term)
       | fst(term)
       | snd(term)

type ::= ...
       | pairTy(type)


/*Typing Rules*/
typeOf G T1 Ty
typeOf G T2 Ty
------------------------------------ [T-Pair]
typeOf G pair(T1, T2) pairTy(Ty)


typeOf G P pairTy(Ty)
--------------------- [T-Fst]
typeOf G fst(P) Ty


typeOf G P pairTy(Ty)
--------------------- [T-Snd]
typeOf G snd(P) Ty


/*Projection Rules*/
----------------------------------------------------------- [Proj-PairTy]
|{type}- pairTy(Ty) ~~> arrow(arrow(Ty, arrow(Ty, Ty)), Ty)


typeOf G pair(T1, T2) pairTy(Ty)
------------------------------------------------ [Proj-Pair]
/*G |- (T1, T2) ~~> (\ a. \ b. \ s. s a b) T1 T2*/
G |{term}- pair(T1, T2) ~~>
           app(app(abs("a", Ty, abs("b", Ty,
                      abs("s", arrow(Ty, arrow(Ty, Ty)),
                           app(app(var("s"), var("a")), var("b"))))),
                   T2), T1)


typeOf G P pairTy(Ty)
------------------------------------------------- [Proj-Fst]
G |{stlc:host:term}- fst(P) ~~>
                     app(P, abs("a", Ty, abs("b", Ty, var("a"))))


typeOf G P pairTy(Ty)
------------------------------------------------- [Proj-Snd]
G |{term}- snd(P) ~~>
           app(P, abs("a", Ty, abs("b", Ty, var("a"))))