Sterling Example: soundX:pair

File: def.sos

[Reduce File] [Raw File]

Module soundX:pair

Builds on soundX:host

tm ::= ...
     | pair(tm, tm)
     | fst(tm)
     | snd(tm)


ty ::= ...
     | pairTy(ty)


typeOf Ctx T1 Ty
----------------------------------------------------------- [Proj-Pair]
Ctx |{tm}- pair(T1, T2) ~~>
     app(
       app(
         abs("A", Ty, abs("B", Ty,
             abs("S", arrowTy(Ty, arrowTy(Ty, Ty)),
                 app(app(var("S"), var("A")), var("B"))))),
         T1),
       T2)


typeOf Ctx T pairTy(Ty)
------------------------------------------------- [Proj-Fst]
Ctx |{tm}- fst(T) ~~>
     app(T, abs("A", Ty, abs("B", Ty, var("A"))))


typeOf Ctx T pairTy(Ty)
------------------------------------------------- [Proj-Snd]
Ctx |{tm}- snd(T) ~~>
     app(T, abs("A", Ty, abs("B", Ty, var("B"))))


------------------------------------------------ [Proj-PairTy]
|{ty}- pairTy(Ty) ~~>
       arrowTy(arrowTy(Ty, arrowTy(Ty, Ty)), Ty)



typeOf Ctx T1 Ty
typeOf Ctx T2 Ty
---------------------------------- [T-Pair]
typeOf Ctx pair(T1, T2) pairTy(Ty)


typeOf Ctx T pairTy(Ty)
----------------------- [T-Fst]
typeOf Ctx fst(T) Ty


typeOf Ctx T pairTy(Ty)
----------------------- [T-Snd]
typeOf Ctx snd(T) Ty