Type Systems: Simply Typed ?-calculus
Realistic core language suitable for type-checking
M ::= c | x | (M M … M) | (? x:?… x:? . M) | if M then M else M
? ::= b | ? ? ... ? ? ? ?
b ? B (a set of base types including bool)
c ? C (a set of constants including true, false), c ? C has a given type ?(c)
x ? V (a set of variables), variables in (x:?… x:?) must be distinct
Typing rules:
- ?, x:? |- x: ?
- ? |- c: ?(c) [ ?(true) = bool, ?(false) = bool ]
- ? |- M:?1 ? ... ? ?k ? ?, ? |? N1:?1,…, ? |- Nk:?k (app rule)
? |- (M N1 … Nk): ?.
- ?, x1:?1, …, xk:?k |? M: ?. (abs rule)
? |- (? x1:?1 …xk:?k . M): ?1 ? ... ? ?k ? ?
- ? |- M1:bool, ? |? M2:?, ? |? M3:? (if rule)
? |- if M1 then M2 else M3 : ?