-
Notifications
You must be signed in to change notification settings - Fork 0
/
Ip.hs
105 lines (74 loc) · 2.25 KB
/
Ip.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
-- Intuitionistic propositional logic, PHOAS approach, initial encoding
{-# LANGUAGE DataKinds, GADTs, KindSignatures, Rank2Types, Safe, TypeOperators #-}
module Pi.Ip where
-- Types
infixl 2 :&&
infixl 1 :||
infixr 0 :=>
data Ty :: * where
UNIT :: Ty
(:=>) :: Ty -> Ty -> Ty
(:&&) :: Ty -> Ty -> Ty
(:||) :: Ty -> Ty -> Ty
FALSE :: Ty
infixr 0 :<=>
type a :<=> b = (a :=> b) :&& (b :=> a)
type NOT a = a :=> FALSE
type TRUE = FALSE :=> FALSE
-- Context and truth judgement
-- NOTE: Haskell does not support kind synonyms
-- type Cx = Ty -> *
type IsTrue (a :: Ty) (tc :: Ty -> *) = tc a
-- Terms
infixl 1 :$
data Tm :: (Ty -> *) -> Ty -> * where
Var :: IsTrue a tc -> Tm tc a
Lam :: (IsTrue a tc -> Tm tc b) -> Tm tc (a :=> b)
(:$) :: Tm tc (a :=> b) -> Tm tc a -> Tm tc b
Pair :: Tm tc a -> Tm tc b -> Tm tc (a :&& b)
Fst :: Tm tc (a :&& b) -> Tm tc a
Snd :: Tm tc (a :&& b) -> Tm tc b
Left' :: Tm tc a -> Tm tc (a :|| b)
Right' :: Tm tc b -> Tm tc (a :|| b)
Match :: Tm tc (a :|| b) -> (IsTrue a tc -> Tm tc c) -> (IsTrue b tc -> Tm tc c) -> Tm tc c
Abort :: Tm tc FALSE -> Tm tc a
var :: IsTrue a tc -> Tm tc a
var = Var
lam :: (Tm tc a -> Tm tc b) -> Tm tc (a :=> b)
lam f = Lam $ \x -> f (var x)
pair :: (Tm tc a, Tm tc b) -> Tm tc (a :&& b)
pair (a, b) = Pair a b
fst' :: Tm tc (a :&& b) -> Tm tc a
fst' = Fst
snd' :: Tm tc (a :&& b) -> Tm tc b
snd' = Snd
left :: Tm tc a -> Tm tc (a :|| b)
left = Left'
right :: Tm tc b -> Tm tc (a :|| b)
right = Right'
case' :: Tm tc (a :|| b) -> (Tm tc a -> Tm tc c) -> (Tm tc b -> Tm tc c) -> Tm tc c
case' xy f g = Match xy (\x -> f (var x)) (\y -> g (var y))
abort :: Tm tc FALSE -> Tm tc a
abort = Abort
type Thm a = forall tc. Tm tc a
-- Example theorems
t1 :: Thm (a :=> NOT a :=> b)
t1 =
lam $ \x ->
lam $ \f -> abort (f :$ x)
t2 :: Thm (NOT a :=> a :=> b)
t2 =
lam $ \f ->
lam $ \x -> abort (f :$ x)
t3 :: Thm (a :=> NOT (NOT a))
t3 =
lam $ \x ->
lam $ \f -> f :$ x
t4 :: Thm (NOT a :<=> NOT (NOT (NOT a)))
t4 =
pair
( lam $ \f ->
lam $ \g -> g :$ f
, lam $ \g ->
lam $ \x -> g :$ (lam $ \f -> f :$ x)
)