-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathchris.hs
177 lines (152 loc) · 6.61 KB
/
chris.hs
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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
{-# LANGUAGE GADTs #-}
-- Define the language
data Exp where
Fun :: Var -> Exp -> Exp
App :: Exp -> Exp -> Exp
Constant :: Value -> Exp
Plus :: Exp -> Exp -> Exp
Minus :: Exp -> Exp -> Exp
Times :: Exp -> Exp -> Exp
Divide :: Exp -> Exp -> Exp
Variable :: Int -> Exp
Not :: Exp -> Exp
And :: Exp -> Exp -> Exp
Or :: Exp -> Exp -> Exp
Branch :: Exp -> Exp -> Exp -> Exp
data Value = VNat Nat | VInt Int | VBool Bool | VFunction (Value -> Value)
--Custom datatypes. These will support ad-hoc polymorphism alongside their usual counterparts below.
data Nat = Zero | Succ Nat
deriving (Show, Eq)
data Parity = P | S
instance Show Value where
show (VInt x) = show x
show (VNat x) = show x
show (VBool x) = show x
show _ = "<Function>"
data Var = Var Int Type
deriving (Eq, Show)
data Type = TInt | TBool | TNat | TFunction Type Type | TError
deriving (Eq, Show)
-- reducer, reduce, expand and simplify reduce any Nat to a canonical form. This solution only uses the List datatype provided by Haskell.
-- provide operations for Nats. Nats with these operations form a ring isomorphic to the integers. It might be fun to implement the field of fractions.
add' :: Nat -> Nat -> Nat
add' x Zero = x
add' x (Succ y) = (Succ (add' (x) (y)))
times' :: Nat -> Nat -> Nat
times' x Zero = Zero
times' x (Succ y) = (add' x (times' x y))
--Functions to extract Nats and Bool's from the Value wrapper. Along with translateint and translatebool below, this allows me to map customtypes to their usual counterparts, for the purposes of the talk.
unwrapint :: Value -> Nat
unwrapint x = case x of
(VNat Zero) -> Zero
(VNat (Succ x)) -> Succ (x)
translateint :: Nat -> Int
translateint Zero = 0
translateint (Succ x) = (translateint x) + 1
-- just as a comment, eval is a functor!
eval :: Exp -> Value
eval (Constant x) = x
eval (Plus x y) = case (eval x, eval y) of
(VInt x, VInt y) -> VInt (x+y)
(VNat x, VNat y) -> VNat (add' (x) (y))
(VInt _, VNat _) -> error "Incompatible argument types!"
(VNat _, VInt _) -> error "Incompatible argument types!"
_ -> error "Arguments must be Ints or Nats!"
eval (Minus x y) = case (eval x, eval y) of
(VInt x, VInt y) -> VInt (x-y)
(VNat x, VNat y) -> VInt ((translateint x) - (translateint y))
(VInt _, VNat _) -> error "Incompatible argument types!"
(VNat _, VInt _) -> error "Incompatible argument types!"
_ -> error "Arguments must be Ints!"
eval (Times x y) = case (eval x, eval y) of
(VInt x, VInt y) -> VInt (x*y)
(VNat x, VNat y) -> VNat (times' (x) (y))
(VInt _, VNat _) -> error "Incompatible argument types!"
(VNat _, VInt _) -> error "Incompatible argument types!"
_ -> error "Arguments must be Ints or Nats!"
eval (Divide x y) = case (eval x, eval y) of
(VInt x, VInt y) -> if (y/=0) then VInt (div x y) else error "Division by zero!"
(VNat x, VNat y) -> if (y/= Zero) then VInt (div (translateint x) (translateint y)) else error "Division by zero!"
(VInt _, VNat _) -> error "Incompatible argument types!"
(VNat _, VInt _) -> error "Incompatible argument types!"
_ -> error "Arguments must be integers!"
eval (Not x) = case (eval x) of
(VBool x) -> VBool (not x)
_ -> error "Not Boolean!"
eval (And x y) = case (eval x, eval y) of
(VBool x, VBool y) -> VBool(x && y)
_ -> error "Not Boolean!"
eval (Or x y) = case (eval x, eval y) of
(VBool x, VBool y) -> VBool(x || y)
_ -> error "Not Boolean!"
eval (Branch x y z) = case (eval x, eval y, eval z) of
(VBool x, this, that) -> if (x==True) then this else that
_ -> error "Condition must evaluate to Bool or Bool'!"
eval (App first second) = case (eval first) of
(VFunction f) -> f (eval second)
_ -> error "First argument is not a function!"
eval (Fun (Var v _) f) = VFunction (\x -> eval(subst f v x))
subst :: Exp -> Int -> Value -> Exp
subst c@(Constant _) _ _ = c
subst (Variable v ) (v' ) x = if (v==v') then (Constant x) else (Variable v )
subst (Plus m n) v x = Plus (subst m v x) (subst n v x)
subst (Minus m n) v x = Minus (subst m v x) (subst n v x)
subst (Times m n) v x = Times (subst m v x) (subst n v x)
subst (Divide m n) v x = Divide (subst m v x) (subst n v x)
subst (Not m) v x = Not (subst m v x)
subst (And m n) v x = And (subst m v x) (subst n v x)
subst (Or m n) v x = Or (subst m v x) (subst n v x)
subst (App m n) v x = App (subst m v x) (subst n v x)
subst (Fun (Var v' t') b) (v ) x = if (v==v') then (Fun (Var v' t') b) else (Fun (Var v' t') (subst b (v ) x))
evalT :: (Int -> Type) -> Exp -> Type
evalT _ (Constant (VInt _)) = TInt
evalT _ (Constant (VBool _)) = TBool
evalT _ (Constant (VNat _)) = TNat
evalT _ (Constant _) = TError
evalT tenv (Variable v) = tenv v
evalT tenv (Plus x y) = case (evalT tenv x, evalT tenv y) of
(TInt, TInt ) -> TInt
(TNat , TNat ) -> TNat
_ -> TError
evalT tenv (Minus x y) = case (evalT tenv x, evalT tenv y) of
(TInt , TInt ) -> TInt
(TNat , TNat ) -> TInt
_ -> TError
evalT tenv (Times x y) = case (evalT tenv x, evalT tenv y) of
(TInt , TInt ) -> TInt
(TNat , TNat ) -> TNat
_ -> TError
evalT tenv (Divide x y) = case (evalT tenv x, evalT tenv y) of
(TInt , TInt ) -> TInt
(TNat, TNat) -> TInt
_ -> TError
evalT tenv (Not x) = case (evalT tenv x) of
(TBool ) -> TBool
_ -> TError
evalT tenv (And x y) = case (evalT tenv x, evalT tenv y) of
(TBool , TBool ) -> TBool
_ -> TError
evalT tenv (Or x y) = case (evalT tenv x, evalT tenv y) of
(TBool , TBool ) -> TBool
_ -> TError
evalT tenv (Branch x y z) = case (evalT tenv x, evalT tenv y, evalT tenv z) of
(TBool , this, that) -> if (this==that) then this else TError
_ -> TError
evalT tenv (App f x) = case (evalT tenv f) of
(TFunction a b) -> if (a==(evalT tenv x)) then b else TError
_ -> TError
evalT tenv (Fun (Var v t) f) = TFunction t (evalT (extend tenv (v) t) f)
extend :: Eq a => (a -> b) -> a -> b -> (a -> b)
extend f x y = \w -> if (w==x) then y else (f w)
eval' :: Exp -> Value
eval' e = if (evalT initialenv e /= TError) then eval e else error "Type error!"
where
initialenv _ = TError
plusone = Fun (Var 1 TNat) (Plus (Variable 1 ) (Constant (VNat (Succ Zero))))
timesfour = Fun (Var 1 TNat) (Times (Variable 1 ) (Constant (VNat (Succ (Succ (Succ (Succ Zero)))))))
y=Fun (Var 1 TNat) (App ((Fun (Var 2 TNat) (App (Variable 1 ) (App (Variable 2 ) (Variable 2 ))))) (Fun (Var 3 TNat) (App (Variable 1 ) (App (Variable 3 ) (Variable 3 )))))
double = Fun (Var 1 (TFunction TNat TNat)) (
Fun (Var 2 TNat) (
App (Variable 1 ) (
App (Variable 1 ) (
(Variable 2 )))))