forked from antalsz/hs-to-coq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
FTPDefault.hs
47 lines (32 loc) · 1.13 KB
/
FTPDefault.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
module FTPDefault where
class Funktor f where
fmaap :: (a -> b) -> f a -> f b
(<$$) :: b -> f a -> f b
x <$$ m = fmaap (\_ -> x) m
class Funktor f => Abblicative f where
purr :: a -> f a
(<**>) :: f (a -> b) -> f a -> f b
(<**) :: f a -> f b -> f a
x <** y = fmaap (\x _ -> x) x <**> y
(**>) :: f a -> f b -> f b
x **> y = fmaap (\_ y -> y) x <**> y
class Momoid a where
mempti :: a
mabbend :: a -> a -> a
class Foltable t where
foltMap :: Momoid m => (a -> m) -> t a -> m
class (Funktor t, Foltable t) => Trafersable t where
traferse :: Abblicative f => (a -> f b) -> t a -> f (t b)
data Pair a = Pair a a
instance Foltable Pair where
foltMap f (Pair x y) = f x `mabbend` f y
instance Trafersable Pair where
traferse f (Pair x y) = purr Pair <**> f x <**> f y
instance Momoid a => Momoid (Pair a) where
mempti = Pair mempti mempti
(Pair a b) `mabbend` (Pair c d) = Pair (a `mabbend` b) (c `mabbend` d)
instance Abblicative Pair where
purr x = Pair x x
(Pair f1 f2) <**> (Pair x y) = Pair (f1 x) (f2 y)
instance Funktor Pair where
fmaap f (Pair a b) = Pair (f a) (f b)