/
Cooper.hs
143 lines (123 loc) · 5.75 KB
/
Cooper.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
module Cooper
( ComposeWith(..)
, HasTrace(..)
, Simple
, Val(Val)
, ($$)
, compose
, lift
, retrieve
, retrieve2
, retrieve3
, retrieve4
, unlift
, store
) where
import HList (HList(HCons, HNil), HListConcat, HListSplit, List(Cons, Nil), hListConcat, hListFirst, hListRest, hListSplit)
class HasTrace a where
type TraceOf a :: *
class TraceList (a :: List *) where
type TracesOf a :: List *
instance TraceList 'Nil where
type TracesOf 'Nil = 'Nil
instance HasTrace x => TraceList ('Cons x xs) where
type TracesOf ('Cons x xs) = ('Cons (TraceOf x) (TracesOf xs))
-- a means of composing values of types a and b (in that order) to obtain a
-- value of type c; c uniqely determined by a and b
class ComposeWith a b c | a b -> c where
composeWith :: a -> b -> c
-- composition by function application
instance ComposeWith (a -> b) a b where
composeWith = id
instance ComposeWith a (a -> b) b where
composeWith = flip id
-- composition by predicate modification
instance ComposeWith (a -> Bool) (a -> Bool) (a -> Bool) where
composeWith p1 p2 x = p1 x && p2 x
data Val s a where
Val :: TraceList s => HList s -> (HList (TracesOf s) -> b) -> Val (HList s) ((HList (TracesOf s)) -> b)
-- a simple value with an empty store (and hence no parameters)
type Simple a = Val (HList 'Nil) (HList 'Nil -> a)
lift :: a -> Val (HList 'Nil) (HList 'Nil -> a)
lift v = Val HNil (\_ -> v)
store
:: HasTrace a
=> Val (HList 'Nil) (HList 'Nil -> a)
-> Val (HList ('Cons a 'Nil)) (HList ('Cons (TraceOf a) 'Nil) -> TraceOf a)
store (Val store a) =
Val (HCons (a HNil) HNil) (\(HCons x _) -> x)
-- retrieves and applies the first value in the store
retrieve
:: (TraceList store, ComposeWith s (p -> t) r)
=> Val (HList ('Cons s store)) (HList ('Cons p (TracesOf store)) -> t)
-> Val (HList store) (HList (TracesOf store) -> r)
retrieve (Val store v) =
Val (hListRest store)
(\ps -> composeWith stored (\x -> (v (HCons x ps))))
where
stored = hListFirst store
compose
:: ( ComposeWith f a r
, HListSplit store1 store2
, HListSplit (TracesOf store1) (TracesOf store2)
, TraceList store1, TraceList store2
, TraceList (HListConcat store1 store2)
, HListConcat (TracesOf store1) (TracesOf store2) ~ TracesOf (HListConcat store1 store2)
)
=> Val (HList store1) (HList (TracesOf store1) -> f)
-> Val (HList store2) (HList (TracesOf store2) -> a)
-> Val (HList (HListConcat store1 store2)) (HList (HListConcat (TracesOf store1) (TracesOf store2)) -> r)
compose (Val store1 f1) (Val store2 f2) =
Val (hListConcat store1 store2)
(\ps ->
let
(p1, p2) = hListSplit ps
in
composeWith (f1 p1) (f2 p2)
)
-- operator synonym for 'compose'
($$)
:: ( ComposeWith f a r
, HListSplit store1 store2
, HListSplit (TracesOf store1) (TracesOf store2)
, TraceList store1, TraceList store2
, TraceList (HListConcat store1 store2)
, HListConcat (TracesOf store1) (TracesOf store2) ~ TracesOf (HListConcat store1 store2)
)
=> Val (HList store1) (HList (TracesOf store1) -> f)
-> Val (HList store2) (HList (TracesOf store2) -> a)
-> Val (HList (HListConcat store1 store2)) (HList (HListConcat (TracesOf store1) (TracesOf store2)) -> r)
($$) = compose
infixr 1 $$
unlift :: Val (HList 'Nil) (HList 'Nil -> a) -> a
unlift (Val _ f) = f HNil
-- retrieves and applies the second value in the store
retrieve2
:: (HasTrace sfst, TraceList store, ComposeWith s (p -> t) r)
=> Val (HList ('Cons sfst ('Cons s store))) (HList ('Cons (TraceOf sfst) ('Cons p (TracesOf store))) -> t)
-> Val (HList ('Cons sfst store)) (HList ('Cons (TraceOf sfst) (TracesOf store)) -> r)
retrieve2 (Val store v) =
Val (HCons (hListFirst store) (hListRest (hListRest store)))
(\ps -> composeWith stored (\x -> (v (HCons (hListFirst ps) (HCons x (hListRest ps))))))
where
stored = hListFirst (hListRest store)
-- retrieves and applies the third value in the store
retrieve3
:: (HasTrace sfst, HasTrace ssnd, TraceList store, ComposeWith s (p -> t) r)
=> Val (HList ('Cons sfst ('Cons ssnd ('Cons s store)))) (HList ('Cons (TraceOf sfst) ('Cons (TraceOf ssnd) ('Cons p (TracesOf store)))) -> t)
-> Val (HList ('Cons sfst ('Cons ssnd store))) (HList ('Cons (TraceOf sfst) ('Cons (TraceOf ssnd) (TracesOf store))) -> r)
retrieve3 (Val store v) =
Val (HCons (hListFirst store) (HCons (hListFirst (hListRest store)) (hListRest (hListRest (hListRest store)))))
(\ps -> composeWith stored (\x -> (v (HCons (hListFirst ps) (HCons (hListFirst (hListRest ps)) (HCons x (hListRest (hListRest ps))))))))
where
stored = hListFirst (hListRest (hListRest store))
-- retrieves and applies the fourth value in the store
retrieve4
:: (HasTrace sfst, HasTrace ssnd, HasTrace strd, TraceList store, ComposeWith s (p -> t) r)
=> Val (HList ('Cons sfst ('Cons ssnd ('Cons strd ('Cons s store))))) (HList ('Cons (TraceOf sfst) ('Cons (TraceOf ssnd) ('Cons (TraceOf strd) ('Cons p (TracesOf store))))) -> t)
-> Val (HList ('Cons sfst ('Cons ssnd ('Cons strd store)))) (HList ('Cons (TraceOf sfst) ('Cons (TraceOf ssnd) ('Cons (TraceOf strd) (TracesOf store)))) -> r)
retrieve4 (Val store v) =
Val (HCons (hListFirst store) (HCons (hListFirst (hListRest store)) (HCons (hListFirst (hListRest (hListRest store))) (hListRest (hListRest (hListRest (hListRest store)))))))
(\ps -> composeWith stored (\x -> (v (HCons (hListFirst ps) (HCons (hListFirst (hListRest ps)) (HCons (hListFirst (hListRest (hListRest ps))) (HCons x (hListRest (hListRest (hListRest ps))))))))))
where
stored = hListFirst (hListRest (hListRest (hListRest store)))