0 | ||| Sum type for binary relations.
 1 | module TypeAligned.Sum
 2 |
 3 | import Control.Relation
 4 | import Data.Linear.Notation
 5 |
 6 | %default total
 7 |
 8 | ||| Sum / Either of relations (linear!)
 9 | public export
10 | data Sum : (p, q : Rel a) -> Rel a where
11 |   Left : {0 p : Rel a} -> p x y -@ Sum p q x y
12 |   Right : {0 q : Rel a} -> q x y -@ Sum p q x y
13 |
14 | ||| Equality testing based on underlying values.
15 | export
16 | {0 p, q : Rel a} -> (Eq (p x y), Eq (q x y)) => Eq (Sum p q x y) where
17 |   (Left l) == (Left r) = l == r
18 |   (Left _) == _ = False
19 |   (Right l) == (Right r) = l == r
20 |   (Right _) == _ = False
21 |
22 | ||| `Left x` or `Right x`, same as `Either`.
23 | export
24 | {0 p, q : Rel a} -> (Show (p x y), Show (q x y)) => Show (Sum p q x y) where
25 |   showPrec d (Left p) = showCon d "Left" (showArg p)
26 |   showPrec d (Right q) = showCon d "Right" (showArg q)
27 |
28 | parameters {0 p, q : Rel a} {0 r, s : Rel b} {0 f : a -> b}
29 |   ||| Linear 'bimap'
30 |   export
31 |   bimapOnce :
32 |     (mapP : p x y -@ r (f x) (f y)) -> (mapQ : q x y -@ s (f x) (f y)) ->
33 |     Sum p q x y -@ Sum r s (f x) (f y)
34 |   bimapOnce mapP _ (Left pxy) = Left (mapP pxy)
35 |   bimapOnce _ mapQ (Right qxy) = Right (mapQ qxy)
36 |
37 |   ||| Transform relationships
38 |   export
39 |   bimap : (mapP : p x y -> r (f x) (f y)) -> (mapQ : q x y -> s (f x) (f y)) -> Sum p q x y -> Sum r s (f x) (f y)
40 |   bimap mapP _ (Left pxy) = Left (mapP pxy)
41 |   bimap _ mapQ (Right qxy) = Right (mapQ qxy)
42 |