-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathRank2IntersectionTypes.hs
More file actions
122 lines (96 loc) · 6.1 KB
/
Rank2IntersectionTypes.hs
File metadata and controls
122 lines (96 loc) · 6.1 KB
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
module Rank2IntersectionTypes where
import LambdaCalculus
import SimpleTypes
data Type1 = T1_0 Type0 | Inters Type1 Type1
deriving Eq
data Type2 = T2_0 Type0 | T2Ap Type1 Type2
deriving Eq
type Ineq = (Type2, Type1)
type SatProblem = [Ineq]
-- Environments.
type Env = [(TeVar, Type1)]
instance Show Type1 where
show (T1_0 t) = show t
show (Inters t1 t2) = ('(':show t1) ++ ('/':'\\':show t2) ++ [')']
instance Show Type2 where
show (T2_0 t) = show t
show (T2Ap t1 t2) = ('(':show t1) ++ (' ':'-':'>':' ':show t2) ++ [')']
-------Transformation of <=2,1-satisfaction problems into unification problems (based on Corollary 33 (Cap.3.1), Rank 2 type systems and recursive definitions)-------
transformSat :: (SatProblem, EqSet, Int) -> (SatProblem, EqSet, Int)
transformSat ([], eqs, n0) = ([], eqs, n0)
transformSat ((T2Ap t1 t2, T1_0 (TVar a)):ts, eqs, n0) = transformSat ((T2_0 t0, t1):(t2, T1_0 t0'):ts, (TVar a, TAp t0 t0'):eqs, n0+2)
where t0 = TVar (TyVar ('a':(show n0)))
t0' = TVar (TyVar ('a':(show (n0+1))))
transformSat ((T2_0 (TAp t1 t2), T1_0 (TVar a)):ts, eqs, n0) = transformSat ((T2_0 t0, T1_0 t1):(T2_0 t2, T1_0 t0'):ts, (TVar a, TAp t0 t0'):eqs, n0+2)
where t0 = TVar (TyVar ('a':(show n0)))
t0' = TVar (TyVar ('a':(show (n0+1))))
transformSat ((T2Ap t1 t2, T1_0 (TAp t0 t0')):ts, eqs, n0) = transformSat ((T2_0 t0, t1):(t2, T1_0 t0'):ts, eqs, n0)
transformSat ((T2_0 (TAp t1 t2), T1_0 (TAp t0 t0')):ts, eqs, n0) = transformSat ((T2_0 t0, T1_0 t1):(T2_0 t2, T1_0 t0'):ts, eqs, n0)
transformSat ((t2, Inters t1 t1'):ts, eqs, n0) = transformSat ((t2, t1):(t2, t1'):ts, eqs, n0)
transformSat ((T2_0 (TVar a), T1_0 t0):ts, eqs, n0) = transformSat (ts, (TVar a, t0):eqs, n0)
-------Trevor Jim's Type Inference Algorithm (based on Def.36 (Cap.3.2), Rank 2 type systems and recursive definitions)-------
listToInters :: [Type1] -> Type1
listToInters [t1] = t1
listToInters (t1:ts) = Inters (listToInters ts) t1
subst1 :: Sub -> Type1 -> Type1
subst1 s (T1_0 t0) = T1_0 (subst s t0)
subst1 s (Inters t1 t1') = Inters (subst1 s t1) (subst1 s t1')
subst2 :: Sub -> Type2 -> Type2
subst2 s (T2_0 t0) = T2_0 (subst s t0)
subst2 s (T2Ap t1 t2) = T2Ap (subst1 s t1) (subst2 s t2)
substty2 :: Subst -> Type2 -> Type2
substty2 [] t2 = t2
substty2 (s:ts) t2 = substty2 ts (subst2 s t2)
substEn :: Sub -> Env -> Env
substEn _ [] = []
substEn s ((x,t):es) = (x, subst1 s t):substEn s es
substEnv :: Subst -> Env -> Env
substEnv [] e = e
substEnv (s:ts) e = substEnv ts (substEn s e)
isInEnv :: TeVar -> Env -> Bool
isInEnv _ [] = False
isInEnv x1 ((x2, _):es) = x1 == x2 || isInEnv x1 es
findAllInEnv :: TeVar -> Env -> [Type1]
findAllInEnv _ [] = []
findAllInEnv x1 ((x2, t):es) | x1 == x2 = t:findAllInEnv x1 es
| otherwise = findAllInEnv x1 es
findInEnv :: TeVar -> Env -> Type1
findInEnv x1 ((x2, t):es) | x1 == x2 = t
| otherwise = findInEnv x1 es
rmFromEnv :: TeVar -> Env -> Env
rmFromEnv _ [] = []
rmFromEnv x1 ((x2, t):es) | x1 == x2 = rmFromEnv x1 es
| otherwise = (x2, t):rmFromEnv x1 es
mergeEnv :: Env -> Env
mergeEnv [] = []
mergeEnv ((x, t1):es) = (x, listToInters (findAllInEnv x ((x, t1):es))):mergeEnv (rmFromEnv x es)
genPPSat :: Type1 -> Term -> Int -> (Env, SatProblem, Int)
genPPSat (T1_0 t0) m n0 = (env, [(t, T1_0 t0)], n1)
where (env, t, n1) = r2typeInf m n0
genPPSat (Inters t1 t1') m n0 = (mergeEnv (envm1++envm2), sat1++sat2, n2)
where (envm1, sat1, n1) = genPPSat t1 m n0
(envm2, sat2, n2) = genPPSat t1' m n1
-- Type inference algorithm.
r2typeInf :: Term -> Int -> (Env, Type2, Int)
r2typeInf (Var x) n0 = let t0 = TVar (TyVar ('a':(show n0))) in ([(x, T1_0 t0)], T2_0 t0, n0+1)
r2typeInf (App m1 m2) n0 = let (env1, t, n1) = r2typeInf m1 n0 in
case t of
T2_0 (TVar t2_0) -> (substEnv s env, substty2 s (T2_0 t0'), n3)
where (env2, t2, n2) = r2typeInf m2 n1
env = mergeEnv (env1++env2)
t0 = TVar (TyVar ('a':(show n2)))
t0' = TVar (TyVar ('a':(show (n2+1))))
([], eqs, n3) = transformSat ([(t2, T1_0 t0)], [((TVar t2_0), TAp t0 t0')], n2+2)
([], Uni s) = unify (eqs, Uni [])
T2Ap t_1 t_2 -> (substEnv s (mergeEnv (env1++envs)), substty2 s t_2, n3)
where (envs, sat, n2) = genPPSat t_1 m2 n1
([], eqs, n3) = transformSat (sat, [], n2)
([], Uni s) = unify (eqs, Uni [])
T2_0 (TAp t_1 t_2) -> (substEnv s (mergeEnv (env1++envs)), substty2 s (T2_0 t_2), n3)
where (envs, sat, n2) = genPPSat (T1_0 t_1) m2 n1
([], eqs, n3) = transformSat (sat, [], n2)
([], Uni s) = unify (eqs, Uni [])
r2typeInf (Abs x m) n0
| isInEnv x env = (rmFromEnv x env, T2Ap (findInEnv x env) t2, n1)
| otherwise = (env, T2Ap (T1_0 (TVar (TyVar ('a':(show n1))))) t2, n1+1)
where (env, t2, n1) = r2typeInf m n0