Pair.hs (5269B)
1 module Lude.Pair ( 2 Pair, 3 type (*), 4 type (×), 5 MkPair, 6 pattern MkPair, 7 outl, 8 outr, 9 dup, 10 swap, 11 curry, 12 uncurry, 13 Outl, 14 Outr, 15 -- 16 fbimap, 17 flmap, 18 frmap, 19 fbmap, 20 fbmap1, 21 foutl, 22 foutr, 23 fdup, 24 fswap, 25 ) where 26 27 import Data.Tuple qualified as Base 28 29 import Lude.Haskell 30 31 -- TODO: Generalize with Cartesian class. 32 33 -------------------------------------------------------------------------------- 34 35 type Pair = Tuple2 36 type (*) = Tuple2 37 type (×) = Tuple2 38 infixl 7 *, × 39 40 -- For consistency 41 type MkPair :: a -> b -> a × b 42 type MkPair = (,) 43 pattern MkPair :: a -> b -> a × b 44 pattern MkPair a b = (a, b) 45 {-# COMPLETE MkPair #-} 46 47 outl :: forall a b. a × b -> a 48 outl = Base.fst 49 50 outr :: forall a b. a × b -> b 51 outr = Base.snd 52 53 dup :: forall a. a -> a × a 54 dup x = (x, x) 55 56 swap :: forall a b. a × b -> b × a 57 swap = Base.swap 58 59 curry :: forall a b c. (a × b -> c) -> (a -> b -> c) 60 curry = Base.curry 61 62 uncurry :: forall a b c. (a -> b -> c) -> (a × b -> c) 63 uncurry = Base.uncurry 64 65 type Outl :: forall {a} {b}. a × b -> a 66 type family Outl _ where 67 Outl (a, b) = a 68 69 type Outr :: forall {a} {b}. a × b -> b 70 type family Outr _ where 71 Outr (a, b) = b 72 73 -------------------------------------------------------------------------------- 74 -- CPS/Yoneda Pair Operations 75 76 -- TODO: Figure-out the best way to generalize this idea. 77 78 type CoTuple :: forall {k} {r :: Repr}. k -> Type# r -> Type 79 type family CoTuple _ _ where 80 CoTuple () z = z -- TODO: must lift somehow 81 CoTuple (a) z = a -> z 82 CoTuple (a, b) z = a -> b -> z 83 CoTuple (a, b, c) z = a -> b -> c -> z 84 CoTuple (a, b, c, d) z = a -> b -> c -> d -> z 85 CoTuple (a, b, c, d, e) z = a -> b -> c -> d -> e -> z 86 CoTuple (a, b, c, d, e, f) z = a -> b -> c -> d -> e -> f -> z 87 CoTuple (a, b, c, d, e, f, g) z = a -> b -> c -> d -> e -> f -> g -> z 88 CoTuple (a, b, c, d, e, f, g, h) z = a -> b -> c -> d -> e -> f -> g -> h -> z 89 CoTuple (a, b, c, d, e, f, g, h, i) z = a -> b -> c -> d -> e -> f -> g -> h -> i -> z 90 CoTuple (MkTuple1 a) z = a -> z 91 92 -- | A morphism @Tuple a -> Tuple b@ for tuples of types @a@ and @b@ with 93 -- arbitrary representations, without requiring `Functional#` tuples 94 type HomTuple :: forall {k} {l}. k -> l -> Type 95 type HomTuple a b = forall {r :: Repr} (z :: Type# r). CoTuple b z -> CoTuple a z 96 97 -- | A morphism @a * b -> a' * b'@ for types @a@, @b@, @a'@, and @b'@ with 98 -- arbitrary representations, without requiring `Functional#` tuples 99 type HomPair 100 :: forall {r :: Repr} {s :: Repr} {r' :: Repr} {s' :: Repr} 101 . Type# r -> Type# s -> Type# r' -> Type# s' -> Type 102 type HomPair a b a' b' = HomTuple (a, b) (a', b') 103 104 -- type HomPair a b a' b' = forall {t :: Repr} (c :: Type# t). (a' -> b' -> c) -> (a -> b -> c) 105 106 -- | A binatural transformation @f * g ~~> f' * g'@ for type-valued functors 107 -- @f@, @g@, @f'@, and @g'@ with arbitrary representations, without requiring 108 -- `Functional#` tuples 109 type HomPair1 110 :: forall {i} {j} {r :: Repr} {s :: Repr} {r' :: Repr} {s' :: Repr} 111 . (i -> Type# r) -> (j -> Type# s) -> (i -> Type# r') -> (j -> Type# s') -> Type 112 type HomPair1 f g f' g' = forall x y. HomPair (f x) (g y) (f' x) (g' y) 113 114 fbimap 115 :: forall {r :: Repr} (a :: Type# r) {r' :: Repr} (a' :: Type# r') {s :: Repr} (b :: Type# s) {s' :: Repr} (b' :: Type# s') 116 . (Functional# r, Functional# r', Functional# s, Functional# s') 117 => (a -> a') -> (b -> b') -> HomPair a b a' b' 118 fbimap f g k = lam2# \x y -> app2# k (app# f x) (app# g y) -- flmap f . frmap g 119 {-# INLINE fbimap #-} 120 121 flmap 122 :: forall {r :: Repr} (a :: Type# r) {r' :: Repr} (a' :: Type# r') {s :: Repr} (b :: Type# s) 123 . (Functional# r, Functional# r', Functional# s) 124 => (a -> a') -> HomPair a b a' b 125 flmap f k = lam2# \x y -> app2# k (app# f x) y -- flip (.#) 126 {-# INLINE flmap #-} 127 128 frmap 129 :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s) {s' :: Repr} (b' :: Type# s') 130 . (Functional# r, Functional# s, Functional# s') 131 => (b -> b') -> HomPair a b a b' 132 frmap g k = lam2# \x y -> app2# k x (app# g y) -- flip (*.#) 133 {-# INLINE frmap #-} 134 135 fbmap 136 :: forall {r :: Repr} (a :: Type# r) {r' :: Repr} (a' :: Type# r') 137 . (Functional# r, Functional# r') 138 => (a -> a') -> HomPair a a a' a' 139 fbmap h = fbimap h h 140 {-# INLINE fbmap #-} 141 142 fbmap1 143 :: forall {i} {r :: Repr} (f :: i -> Type# r) {r' :: Repr} (f' :: i -> Type# r') 144 . (Functional# r, Functional# r') 145 => (f ~> f') -> HomPair1 f f f' f' 146 fbmap1 h = fbimap h h 147 {-# INLINE fbmap1 #-} 148 149 foutl 150 :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s) 151 . (Functional# r, Functional# s) => HomTuple (a, b) (a) 152 foutl k = lam2# \x _ -> app# k x 153 {-# INLINE foutl #-} 154 155 foutr 156 :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s) 157 . (Functional# r, Functional# s) => HomTuple (a, b) (b) 158 foutr k = lam2# \_ y -> app# k y 159 {-# INLINE foutr #-} 160 161 fdup 162 :: forall {r :: Repr} (a :: Type# r) 163 . (Functional# r) => HomTuple (a) (a, a) 164 fdup k = lam# \x -> app2# k x x 165 {-# INLINE fdup #-} 166 167 fswap 168 :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s) 169 . (Functional# r, Functional# s) => HomPair b a a b 170 fswap k = lam2# \x y -> app2# k y x 171 {-# INLINE fswap #-}