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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
{-# LANGUAGE GADTs #-}
module Arith where
data E a b = E (a -> b) (b -> a)
eqRefl :: E a a
eqRefl = E id id
-- just to construct unique strings
data W
data M a
-- terms
data Var a where
VarW :: Var W
VarM :: Var (M a)
-- expose s in the type level making sure it is a string
data Abs s e1 where
Abs :: (Var s) -> e1 -> Abs (Var s) e1
data App e1 e2 = App e1 e2
data Lit = Lit
data TyBase = TyBase
data TyArr t1 t2 = TyArr t1 t2
-- (x:ty) in G
data IN g p where
INOne :: IN (g,(x,ty)) (x,ty)
INShift :: IN g0 (x,ty) -> IN (g0,a) (x,ty)
data INEX g x where
INEX :: IN g (x,v) -> INEX g x
-- G1 subseteq G2
type SUP g1 g2 = forall a. IN g1 a -> IN g2 a
-- typing derivations
data DER g a ty where
DVar :: IN (g,g0) ((Var a),ty) -> DER (g,g0) (Var a) ty -- the g,g0 makes sure that env is non-empty
DApp :: DER g a1 (TyArr ty1 ty2) ->
DER g a2 ty1 -> DER g (App a1 a2) ty2
DAbs :: DER (g,(Var a,ty1)) e ty2 ->
DER g (Abs (Var a) e) (TyArr ty1 ty2)
DLit :: DER g Lit TyBase
-- G |- \x.x : a -> a
test1 :: DER g (Abs (Var W) (Var W)) (TyArr ty ty)
test1 = DAbs (DVar INOne)
-- G |- (\x.x) Lit : Lit
test2 :: DER g (App (Abs (Var W) (Var W)) Lit) TyBase
test2 = DApp (DAbs (DVar INOne)) DLit
-- G |- \x.\y. x y : (C -> C) -> C -> C
test3 :: DER g (Abs (Var W) (Abs (Var (M W)) (App (Var W) (Var (M W))))) (TyArr (TyArr ty ty) (TyArr ty ty))
test3 = DAbs (DAbs (DApp (DVar (INShift INOne)) (DVar INOne)))
data ISVAL e where
ISVALAbs :: ISVAL (Abs (Var v) e)
ISVALLit :: ISVAL Lit
data React e1 e2 where
SUBSTReact :: React (Abs (Var y) e) v
-- evaluation
data EDER e1 e2 where
-- EVar :: IN (a,val) -> ISVAL val -> EDER c a val
EApp1 :: EDER e1 e1' -> EDER (App e1 e2) (App e1' e2)
EApp2 :: ISVAL v1 -> EDER e2 e2' -> EDER (App v1 e2) (App v1 e2')
EAppAbs :: ISVAL v2 -> React (Abs (Var v) e) v2 -> EDER (App (Abs (Var v) e) v2) e1
-- (\x.x) 3 -> 3
-- test4 :: EDER (App (Abs (Var W) (Var W)) Lit) Lit
-- test4 = EAppAbs ISVALLit SUBSTEqVar
-- existential
data REDUCES e1 where
REDUCES :: EDER e1 e2 -> REDUCES e1
-- data WFEnv x c g where
-- WFOne :: ISVAL v -> DER g v ty -> WFEnv (Var x) (c,(Var x,v)) (g,(Var x,ty))
-- WFShift :: WFEnv v c0 g0 -> WFEnv v (c0,(y,y1)) (g0,(z,z1))
-- data WFENVWRAP c g where
-- WFENVWRAP :: (forall v ty . IN g (v,ty) -> WFEnv v c g) -> WFENVWRAP c g
-- data INEXVAL c x where
-- INEXVAL :: IN c (x,v) -> ISVAL v -> INEXVAL c x
-- -- the first cool theorem!
-- fromTEnvToEnv :: IN g (x,ty) -> WFEnv x c g -> INEXVAL c x
-- fromTEnvToEnv INOne (WFOne isv _) = INEXVAL INOne isv
-- fromTEnvToEnv (INShift ind1) (WFShift ind2) =
-- case (fromTEnvToEnv ind1 ind2) of
-- INEXVAL i isv -> INEXVAL (INShift i) isv
data ISLAMBDA v where ISLAMBDA :: ISLAMBDA (Abs (Var x) e)
data ISLIT v where ISLIT :: ISLIT Lit
data EXISTAbs where
EXISTSAbs :: (Abs (Var x) e) -> EXISTAbs
bot = bot
canFormsLam :: ISVAL v -> DER g v (TyArr ty1 ty2) -> ISLAMBDA v
canFormsLam ISVALAbs _ = ISLAMBDA
-- canFormsLam ISVALLit _ = bot <== unfortunately I cannot catch this ... requires some exhaustiveness check :-(
canFormsLit :: ISVAL v -> DER g v TyBase -> ISLIT v
canFormsLit ISVALLit _ = ISLIT
data NULL
progress :: DER NULL e ty -> Either (ISVAL e) (REDUCES e)
progress (DAbs prem) = Left ISVALAbs
progress (DLit) = Left ISVALLit
-- progress (DVar iw) = bot <== here is the cool trick! I cannot even wite this down!
progress (DApp e1 e2) =
case (progress e1) of
Right (REDUCES r1) -> Right (REDUCES (EApp1 r1))
Left isv1 -> case (progress e2) of
Right (REDUCES r2) -> Right (REDUCES (EApp2 isv1 r2))
Left isv2 -> case (canFormsLam isv1 e1) of
ISLAMBDA -> Right (REDUCES (EAppAbs isv2 SUBSTReact))
-- case fromTEnvToEnv iw (f iw) of
-- INEXVAL i isv -> Right (REDUCES (EVar i isv))
-- progress (WFENVWRAP f) (DApp e1 e2) =
-- case (progress (WFENVWRAP f) e1) of
-- Right (REDUCES r1) -> Right (REDUCES (EApp1 r1))
-- Left isv1 -> case (progress (WFENVWRAP f) e2) of
-- Right (REDUCES r2) -> Right (REDUCES (EApp2 isv1 r2))
-- Left isv2 -> case (canFormsLam isv1 e1) of
-- ISLAMBDA -> EAppAbs isv2 e1
|
