blob: 247b9eb6154e0e709c7dc91d1cf595187fae1d65 (
plain)
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
|
{-# LANGUAGE GADTs, ExistentialQuantification #-}
-- This typechecker, written by Stephanie Weirich at Dagstuhl (Sept 04)
-- demonstrates that it's possible to write functions of type
-- tc :: String -> Term a
-- where Term a is our strongly-typed GADT.
-- That is, generate a typed term from an untyped source; Lennart
-- Augustsson set this as a challenge.
--
-- In fact the main function goes
-- tc :: UTerm -> exists ty. (Ty ty, Term ty)
-- so the type checker returns a pair of an expression and its type,
-- wrapped, of course, in an existential.
module Main where
-- Untyped world --------------------------------------------
data UTerm = UVar String
| ULam String UType UTerm
| UApp UTerm UTerm
| UConBool Bool
| UIf UTerm UTerm UTerm
data UType = UBool | UArr UType UType
-- Typed world -----------------------------------------------
data Ty t where
Bool :: Ty Bool
Arr :: Ty a -> Ty b -> Ty (a -> b)
data Term g t where
Var :: Var g t -> Term g t
Lam :: Ty a -> Term (g,a) b -> Term g (a->b)
App :: Term g (s -> t) -> Term g s -> Term g t
ConBool :: Bool -> Term g Bool
If :: Term g Bool -> Term g a -> Term g a -> Term g a
data Var g t where
ZVar :: Var (h,t) t
SVar :: Var h t -> Var (h,s) t
data Typed thing = forall ty. Typed (Ty ty) (thing ty)
-- Typechecking types
data ExType = forall t. ExType (Ty t)
tcType :: UType -> ExType
tcType UBool = ExType Bool
tcType (UArr t1 t2) = case tcType t1 of { ExType t1' ->
case tcType t2 of { ExType t2' ->
ExType (Arr t1' t2') }}
-- The type environment and lookup
data TyEnv g where
Nil :: TyEnv g
Cons :: String -> Ty t -> TyEnv h -> TyEnv (h,t)
lookupVar :: String -> TyEnv g -> Typed (Var g)
lookupVar _ Nil = error "Variable not found"
lookupVar v (Cons s ty e)
| v==s = Typed ty ZVar
| otherwise = case lookupVar v e of
Typed ty v -> Typed ty (SVar v)
-- Comparing types
newtype C1 c a2 d = C1 { unC1 :: c (d -> a2) }
newtype C2 c b1 d = C2 { unC2 :: c (b1 -> d) }
cast2 :: Ty a -> Ty b -> (c a -> c b)
cast2 Bool Bool x = x
cast2 (Arr a1 a2) (Arr b1 b2) f
= let C1 x = cast2 a1 b1 (C1 f)
C2 y = cast2 a2 b2 (C2 x)
in y
data Equal a b where
Equal :: Equal c c
cmpTy :: Ty a -> Ty b -> Maybe (Equal a b)
cmpTy Bool Bool = Just Equal
cmpTy (Arr a1 a2) (Arr b1 b2)
= do { Equal <- cmpTy a1 b1
; Equal <- cmpTy a2 b2
; return Equal }
-- Typechecking terms
tc :: UTerm -> TyEnv g -> Typed (Term g)
tc (UVar v) env = case lookupVar v env of
Typed ty v -> Typed ty (Var v)
tc (UConBool b) env
= Typed Bool (ConBool b)
tc (ULam s ty body) env
= case tcType ty of { ExType bndr_ty' ->
case tc body (Cons s bndr_ty' env) of { Typed body_ty' body' ->
Typed (Arr bndr_ty' body_ty')
(Lam bndr_ty' body') }}
tc (UApp e1 e2) env
= case tc e1 env of { Typed (Arr bndr_ty body_ty) e1' ->
case tc e2 env of { Typed arg_ty e2' ->
case cmpTy arg_ty bndr_ty of
Nothing -> error "Type error"
Just Equal -> Typed body_ty (App e1' e2') }}
tc (UIf e1 e2 e3) env
= case tc e1 env of { Typed Bool e1' ->
case tc e2 env of { Typed t2 e2' ->
case tc e3 env of { Typed t3 e3' ->
case cmpTy t2 t3 of
Nothing -> error "Type error"
Just Equal -> Typed t2 (If e1' e2' e3') }}}
showType :: Ty a -> String
showType Bool = "Bool"
showType (Arr t1 t2) = "(" ++ showType t1 ++ ") -> (" ++ showType t2 ++ ")"
uNot = ULam "x" UBool (UIf (UVar "x") (UConBool False) (UConBool True))
test :: UTerm
test = UApp uNot (UConBool True)
main = putStrLn (case tc test Nil of
Typed ty _ -> showType ty
)
|
