Sterling Example: tutorial:typing

File: syntax.sos

[Reduce File] [Raw File]

Module tutorial:typing

Builds on tutorial:host

tm ::= ...
     | tyAbs(string, ty, tm)

------------------------------------ [Proj-TyAbs]
|{tm}- tyAbs(X, Ty, T) ~~> abs(X, T)


ty ::= baseTy /*because we don't have any particular types*/
     | arrowTy(ty, ty)

Projection ty :


X != Y
subst X R B S
----------------------------------------- [S-TyAbs-NEq]
subst X R tyAbs(Y, Ty, B) tyAbs(Y, Ty, S)


----------------------------------------- [S-TyAbs-Eq]
subst X R tyAbs(X, Ty, B) tyAbs(X, Ty, B)



--------------------- [V-TyAbs]
value tyAbs(X, Ty, T)



--------------------------- [AF-TyAbs]
absForm tyAbs(X, Ty, T) X T



closed X::Vars T
--------------------------- [C-TyAbs]
closed Vars tyAbs(X, Ty, T)

File: typing.sos

[Reduce File] [Raw File]

Module tutorial:typing

Judgment typeOf : [(string, ty)] tm* ty

lookup G X Ty
------------------ [T-Var]
typeOf G var(X) Ty


typeOf G T1 arrowTy(Ty1, Ty2)
typeOf G T2 Ty1
----------------------------- [T-App]
typeOf G app(T1, T2) Ty2


typeOf (X, Ty1)::G T Ty2
------------------------------------------- [T-TyAbs]
typeOf G tyAbs(X, Ty1, T) arrowTy(Ty1, Ty2)


typeOf (X, Ty1)::G T Ty2
------------------------------------ [T-Abs]
typeOf G abs(X, T) arrowTy(Ty1, Ty2)


|{tm}- T ~~> T_T
typeOf G T_T Ty
---------------- [T-D]*
typeOf G T Ty