git.iko.soy/Idris-dev
on master help sign in
Rename Either.swap to Either.mirror and extract Pairs.swap
commitdce49c0b901031af71a1e059830ef973ba222da0 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 20 Apr 2015, 14:06 (12 years ago) parentc18f17b
4 files changed+14−16
compare with master
unifiedsplit
libs/base/Control/Arrow.idr+2−4 libs/base/Control/Isomorphism.idr+5−8 libs/prelude/Prelude/Either.idr+4−4 libs/prelude/Prelude/Pairs.idr+3
libs/base/Control/Arrow.idr+2−4
@@ -16,9 +16,7 @@ class Category arr => Arrow (arr : Type -> Type -> Type) where
1616 first : arr a b -> arr (a, c) (b, c)
1717
1818 second : arr a b -> arr (c, a) (c, b)
19− second f = arrow swap >>> first f >>> arrow swap where
20− swap : (x,y) -> (y,x)
21− swap (x,y) = (y,x)
19+ second f = arrow swap >>> first f >>> arrow swap
2220
2321 (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
2422 f *** g = first f >>> second g
@@ -61,7 +59,7 @@ class Arrow arr => ArrowChoice (arr : Type -> Type -> Type) where
6159 left : arr a b -> arr (Either a c) (Either b c)
6260
6361 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
6563
6664 (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)
6765 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
3939
4040||| Disjunction is commutative
4141eitherComm : Iso (Either a b) (Either b a)
42−eitherComm = MkIso swap swap swapSwap swapSwap
43− where swapSwap : (e : Either a' b') -> swap (swap e) = e
44− swapSwap (Left x) = Refl
45− swapSwap (Right x) = Refl
42+eitherComm = MkIso mirror mirror mirrorMirror mirrorMirror
43+ where mirrorMirror : (e : Either a' b') -> mirror (mirror e) = e
44+ mirrorMirror (Left x) = Refl
45+ mirrorMirror (Right x) = Refl
4646
4747||| Disjunction is associative
4848eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))
@@ -113,10 +113,7 @@ eitherCongRight i = eitherCong isoRefl i
113113||| Conjunction is commutative
114114pairComm : Iso (a, b) (b, a)
115115pairComm = 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
120117 swapSwap (x, y) = Refl
121118
122119||| Conjunction is associative
libs/prelude/Prelude/Either.idr+4−4
@@ -66,10 +66,10 @@ fromEither : Either a a -> a
6666fromEither (Left l) = l
6767fromEither (Right r) = r
6868
69−||| Either is commutative
70−swap : Either a b -> Either b a
71−swap (Left x) = Right x
72−swap (Right x) = Left x
69+||| Right becomes left and left becomes right
70+mirror : Either a b -> Either b a
71+mirror (Left x) = Right x
72+mirror (Right x) = Left x
7373
7474--------------------------------------------------------------------------------
7575-- Conversions
libs/prelude/Prelude/Pairs.idr+3
@@ -5,6 +5,9 @@ import Builtins
55%access public
66%default total
77
8+swap : (a, b) -> (b, a)
9+swap (x, y) = (y, x)
10+
811using (a : Type, P : a -> Type)
912
1013 ||| Dependent pair where the first field is erased.