1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
; type checking for simply typed lambda calculus
(datatype Type
(TArr Type Type) ; t1 -> t2
)
(constructor TUnitConst () Type)
(let $TUnit (TUnitConst))
(datatype Expr
(Lam String Type Expr) ; lam x : t . e
(App Expr Expr)
(Var String)
)
(constructor MyUnitConst () Expr)
(let $MyUnit (MyUnitConst))
(datatype Ctx
(Cons String Type Ctx)
)
(constructor NilConst () Ctx)
(let $Nil (NilConst))
; ctx |- expr : type
(constructor typeof (Ctx Expr) Type)
; ctx |- () : unit
(rewrite (typeof ctx $MyUnit) $TUnit)
; ctx; x: t |- x : t
(rewrite (typeof (Cons x t ctx) (Var x)) t)
; ctx |- f :- t1 -> t2
; ctx |- e : t1
; -----------------
; ctx |- f e : t2
(rule (
(= (typeof ctx (App f e)) t2)
)(
(typeof ctx f)
(typeof ctx e)
))
(rule (
(= (typeof ctx (App f e)) t1)
(= (typeof ctx f) (TArr (typeof ctx e) t2))
)(
(union t1 t2)
))
; ctx |- x : t
; ------------------ y != x
; ctx; y: t |- x : t
(rewrite (typeof (Cons y ty ctx) (Var x))
(typeof ctx (Var x))
:when ((!= x y)))
; ctx; x: t1 |- e : t2
; ------------------------------
; ctx |- lam x: t1. e : t1 -> t2
; rhs of rewrite creates demand
(rewrite (typeof ctx (Lam x t1 e))
(TArr t1 (typeof (Cons x t1 ctx) e)))
; TEST
; ----
; lam x : unit, f : unit -> unit . f x
(let $e
(Lam "x" $TUnit
(Lam "f" (TArr $TUnit $TUnit)
(App (Var "f") (Var "x")))))
; lam x : unit . x
(let $id (Lam "x" $TUnit (Var "x")))
(let $t-id (typeof $Nil $id))
; ($e () $id) = ()
(let $app-unit-id (App (App $e $MyUnit) $id))
(let $t-app (typeof $Nil $app-unit-id))
(let $free (Lam "x" $TUnit (Var "y")))
(let $t-free-ill (typeof $Nil $free))
(let $t-free-1 (typeof (Cons "y" $TUnit $Nil) $free))
(let $t-free-2 (typeof (Cons "y" (TArr (TArr $TUnit $TUnit) $TUnit) $Nil) $free))
(run 15)
(extract $t-id)
(check (= $t-id (TArr $TUnit $TUnit)))
(extract $t-app)
(check (= $t-app $TUnit))
(extract $t-free-1)
(check (= $t-free-1 (TArr $TUnit $TUnit)))
(extract $t-free-2)
(check (= $t-free-2 (TArr $TUnit (TArr (TArr $TUnit $TUnit) $TUnit))))
; this will err
; (extract $t-free-ill)