git.iko.soy/Idris-dev
on master help sign in
Rename Either.swap to Either.mirror and extract Pairs.swap
dce49c0David Raymond Christiansen
libs/base/Control/Arrow.idr+2−4
compare with master
unifiedsplit
@@ -16,9 +16,7 @@ class Category arr => Arrow (arr : Type -> Type -> Type) where
16 first : arr a b -> arr (a, c) (b, c)
16 first : arr a b -> arr (a, c) (b, c)
17
17
18 second : arr a b -> arr (c, a) (c, b)
18 second : arr a b -> arr (c, a) (c, b)
19− second f = arrow swap >>> first f >>> arrow swap where
19+ second f = arrow swap >>> first f >>> arrow swap
20− swap : (x,y) -> (y,x)
21− swap (x,y) = (y,x)
22
20
23 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
21 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
24 f *** g = first f >>> second g
22 f *** g = first f >>> second g
@@ -61,7 +59,7 @@ class Arrow arr => ArrowChoice (arr : Type -> Type -> Type) where
61 left : arr a b -> arr (Either a c) (Either b c)
59 left : arr a b -> arr (Either a c) (Either b c)
62
60
63 right : arr a b -> arr (Either c a) (Either c b)
61 right : arr a b -> arr (Either c a) (Either c b)
64− right f = arrow swap >>> left f >>> arrow swap
62+ right f = arrow mirror >>> left f >>> arrow mirror
65
63
66 (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)
64 (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)
67 f +++ g = left f >>> right g
65 f +++ g = left f >>> right g
libs/base/Control/Isomorphism.idr+5−8
@@ -39,10 +39,10 @@ isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
39
39
40||| Disjunction is commutative
40||| Disjunction is commutative
41eitherComm : Iso (Either a b) (Either b a)
41eitherComm : Iso (Either a b) (Either b a)
42−eitherComm = MkIso swap swap swapSwap swapSwap
42+eitherComm = MkIso mirror mirror mirrorMirror mirrorMirror
43− where swapSwap : (e : Either a' b') -> swap (swap e) = e
43+ where mirrorMirror : (e : Either a' b') -> mirror (mirror e) = e
44− swapSwap (Left x) = Refl
44+ mirrorMirror (Left x) = Refl
45− swapSwap (Right x) = Refl
45+ mirrorMirror (Right x) = Refl
46
46
47||| Disjunction is associative
47||| Disjunction is associative
48eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))
48eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))
@@ -113,10 +113,7 @@ eitherCongRight i = eitherCong isoRefl i
113||| Conjunction is commutative
113||| Conjunction is commutative
114pairComm : Iso (a, b) (b, a)
114pairComm : Iso (a, b) (b, a)
115pairComm = MkIso swap swap swapSwap swapSwap
115pairComm = MkIso swap swap swapSwap swapSwap
116− where swap : (a', b') -> (b', a')
117− swap (x, y) = (y, x)
118−
119− swapSwap : (x : (a', b')) -> swap (swap x) = x
116+ where swapSwap : (x : (a', b')) -> swap (swap x) = x
120 swapSwap (x, y) = Refl
117 swapSwap (x, y) = Refl
121
118
122||| Conjunction is associative
119||| Conjunction is associative
libs/prelude/Prelude/Either.idr+4−4
@@ -66,10 +66,10 @@ fromEither : Either a a -> a
66fromEither (Left l) = l
66fromEither (Left l) = l
67fromEither (Right r) = r
67fromEither (Right r) = r
68
68
69−||| Either is commutative
69+||| Right becomes left and left becomes right
70−swap : Either a b -> Either b a
70+mirror : Either a b -> Either b a
71−swap (Left x) = Right x
71+mirror (Left x) = Right x
72−swap (Right x) = Left x
72+mirror (Right x) = Left x
73
73
74--------------------------------------------------------------------------------
74--------------------------------------------------------------------------------
75-- Conversions
75-- Conversions
libs/prelude/Prelude/Pairs.idr+3
@@ -5,6 +5,9 @@ import Builtins
5%access public
5%access public
6%default total
6%default total
7
7
8+swap : (a, b) -> (b, a)
9+swap (x, y) = (y, x)
10+
8using (a : Type, P : a -> Type)
11using (a : Type, P : a -> Type)
9
12
10 ||| Dependent pair where the first field is erased.
13 ||| Dependent pair where the first field is erased.