commit 5f4d78ab7400b020beea411d7d1cc3144a93c736
parent 5724351a8a85cd9d3e272642b2c37eeb096d6f83
Author: Robert Russell <robert@rr3.xyz>
Date: Mon, 5 Oct 2026 10:04:52 -0700
Pair: add tentative combinators for Repr-generic pair manipulations
Diffstat:
5 files changed, 202 insertions(+), 34 deletions(-)
diff --git a/src/Lude/Algebra/Category/Bifunctor.hs b/src/Lude/Algebra/Category/Bifunctor.hs
@@ -19,6 +19,7 @@ import Lude.Algebra.Category.Core
import Lude.Algebra.Category.Iso
import Lude.Algebra.Category.Terminal
import Lude.Haskell
+import Lude.Pair
-- TODO: Read Conor McBride's paper on bifunctors and decide what abstractions
-- are worth providing here.
@@ -162,12 +163,6 @@ class (MonoidalFunctorialOn p (Prod p), HasTerminalObject p, Terminal p ~ Monid
--------------------------------------------------------------------------------
-- TODO: Temp
-type Pair :: Type -> Type -> Type
-data Pair a b = MkPair a b
-
-instance Functorial (Pair a) where map f = \(MkPair x y) -> MkPair x (f y)
-instance Functorial Pair where map f = Naturally \(MkPair x y) -> MkPair (f x) y
-
instance SemigroupalFunctorial Pair where
assoc = MkIso to fro
where
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -31,6 +31,7 @@ import Data.Coerce
import Prelude qualified as Base
import Lude.Constraint.Predicate
+import Lude.Function
import Lude.Haskell
import Lude.IO
import Lude.List
@@ -235,6 +236,53 @@ instance Functorial Given where
type Cod Given = Entailment
map = mapGiven
+-- TODO: We'll need some map aliases for NT-valued functors to make these usable...
+instance Functorial (Tuple1) where map z = \(MkTuple1 a) -> MkTuple1 (z a)
+instance Functorial (Tuple2 a) where map z = \(a, b) -> (a, z b)
+instance Functorial (Tuple2) where map z = Naturally \(a, b) -> (z a, b)
+instance Functorial (Tuple3 a b) where map z = \(a, b, c) -> (a, b, z c)
+instance Functorial (Tuple3 a) where map z = Naturally \(a, b, c) -> (a, z b, c)
+instance Functorial (Tuple3) where map z = Naturally $ Naturally \(a, b, c) -> (z a, b, c)
+instance Functorial (Tuple4 a b c) where map z = \(a, b, c, d) -> (a, b, c, z d)
+instance Functorial (Tuple4 a b) where map z = Naturally \(a, b, c, d) -> (a, b, z c, d)
+instance Functorial (Tuple4 a) where map z = Naturally $ Naturally \(a, b, c, d) -> (a, z b, c, d)
+instance Functorial (Tuple4) where map z = Naturally $ Naturally $ Naturally \(a, b, c, d) -> (z a, b, c, d)
+instance Functorial (Tuple5 a b c d) where map z = \(a, b, c, d, e) -> (a, b, c, d, z e)
+instance Functorial (Tuple5 a b c) where map z = Naturally $ \(a, b, c, d, e) -> (a, b, c, z d, e)
+instance Functorial (Tuple5 a b) where map z = Naturally $ Naturally \(a, b, c, d, e) -> (a, b, z c, d, e)
+instance Functorial (Tuple5 a) where map z = Naturally $ Naturally $ Naturally \(a, b, c, d, e) -> (a, z b, c, d, e)
+instance Functorial (Tuple5) where map z = Naturally $ Naturally $ Naturally $ Naturally \(a, b, c, d, e) -> (z a, b, c, d, e)
+instance Functorial (Tuple6 a b c d e) where map z = \(a, b, c, d, e, f) -> (a, b, c, d, e, z f)
+instance Functorial (Tuple6 a b c d) where map z = Naturally $ \(a, b, c, d, e, f) -> (a, b, c, d, z e, f)
+instance Functorial (Tuple6 a b c) where map z = Naturally $ Naturally $ \(a, b, c, d, e, f) -> (a, b, c, z d, e, f)
+instance Functorial (Tuple6 a b) where map z = Naturally $ Naturally $ Naturally \(a, b, c, d, e, f) -> (a, b, z c, d, e, f)
+instance Functorial (Tuple6 a) where map z = Naturally $ Naturally $ Naturally $ Naturally \(a, b, c, d, e, f) -> (a, z b, c, d, e, f)
+instance Functorial (Tuple6) where map z = Naturally $ Naturally $ Naturally $ Naturally $ Naturally \(a, b, c, d, e, f) -> (z a, b, c, d, e, f)
+instance Functorial (Tuple7 a b c d e f) where map z = \(a, b, c, d, e, f, g) -> (a, b, c, d, e, f, z g)
+instance Functorial (Tuple7 a b c d e) where map z = Naturally $ \(a, b, c, d, e, f, g) -> (a, b, c, d, e, z f, g)
+instance Functorial (Tuple7 a b c d) where map z = Naturally $ Naturally $ \(a, b, c, d, e, f, g) -> (a, b, c, d, z e, f, g)
+instance Functorial (Tuple7 a b c) where map z = Naturally $ Naturally $ Naturally $ \(a, b, c, d, e, f, g) -> (a, b, c, z d, e, f, g)
+instance Functorial (Tuple7 a b) where map z = Naturally $ Naturally $ Naturally $ Naturally \(a, b, c, d, e, f, g) -> (a, b, z c, d, e, f, g)
+instance Functorial (Tuple7 a) where map z = Naturally $ Naturally $ Naturally $ Naturally $ Naturally \(a, b, c, d, e, f, g) -> (a, z b, c, d, e, f, g)
+instance Functorial (Tuple7) where map z = Naturally $ Naturally $ Naturally $ Naturally $ Naturally $ Naturally \(a, b, c, d, e, f, g) -> (z a, b, c, d, e, f, g)
+instance Functorial (Tuple8 a b c d e f g) where map z = \(a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, z h)
+instance Functorial (Tuple8 a b c d e f) where map z = Naturally $ \(a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, z g, h)
+instance Functorial (Tuple8 a b c d e) where map z = Naturally $ Naturally $ \(a, b, c, d, e, f, g, h) -> (a, b, c, d, e, z f, g, h)
+instance Functorial (Tuple8 a b c d) where map z = Naturally $ Naturally $ Naturally $ \(a, b, c, d, e, f, g, h) -> (a, b, c, d, z e, f, g, h)
+instance Functorial (Tuple8 a b c) where map z = Naturally $ Naturally $ Naturally $ Naturally $ \(a, b, c, d, e, f, g, h) -> (a, b, c, z d, e, f, g, h)
+instance Functorial (Tuple8 a b) where map z = Naturally $ Naturally $ Naturally $ Naturally $ Naturally \(a, b, c, d, e, f, g, h) -> (a, b, z c, d, e, f, g, h)
+instance Functorial (Tuple8 a) where map z = Naturally $ Naturally $ Naturally $ Naturally $ Naturally $ Naturally \(a, b, c, d, e, f, g, h) -> (a, z b, c, d, e, f, g, h)
+instance Functorial (Tuple8) where map z = Naturally $ Naturally $ Naturally $ Naturally $ Naturally $ Naturally $ Naturally \(a, b, c, d, e, f, g, h) -> (z a, b, c, d, e, f, g, h)
+instance Functorial (Tuple9 a b c d e f g h) where map z = \(a, b, c, d, e, f, g, h, i) -> (a, b, c, d, e, f, g, h, z i)
+instance Functorial (Tuple9 a b c d e f g) where map z = Naturally $ \(a, b, c, d, e, f, g, h, i) -> (a, b, c, d, e, f, g, z h, i)
+instance Functorial (Tuple9 a b c d e f) where map z = Naturally $ Naturally $ \(a, b, c, d, e, f, g, h, i) -> (a, b, c, d, e, f, z g, h, i)
+instance Functorial (Tuple9 a b c d e) where map z = Naturally $ Naturally $ Naturally $ \(a, b, c, d, e, f, g, h, i) -> (a, b, c, d, e, z f, g, h, i)
+instance Functorial (Tuple9 a b c d) where map z = Naturally $ Naturally $ Naturally $ Naturally $ \(a, b, c, d, e, f, g, h, i) -> (a, b, c, d, z e, f, g, h, i)
+instance Functorial (Tuple9 a b c) where map z = Naturally $ Naturally $ Naturally $ Naturally $ Naturally $ \(a, b, c, d, e, f, g, h, i) -> (a, b, c, z d, e, f, g, h, i)
+instance Functorial (Tuple9 a b) where map z = Naturally $ Naturally $ Naturally $ Naturally $ Naturally $ Naturally \(a, b, c, d, e, f, g, h, i) -> (a, b, z c, d, e, f, g, h, i)
+instance Functorial (Tuple9 a) where map z = Naturally $ Naturally $ Naturally $ Naturally $ Naturally $ Naturally $ Naturally \(a, b, c, d, e, f, g, h, i) -> (a, z b, c, d, e, f, g, h, i)
+instance Functorial (Tuple9) where map z = Naturally $ Naturally $ Naturally $ Naturally $ Naturally $ Naturally $ Naturally $ Naturally \(a, b, c, d, e, f, g, h, i) -> (z a, b, c, d, e, f, g, h, i)
+
--------------------------------------------------------------------------------
-- Interop
diff --git a/src/Lude/Function.hs b/src/Lude/Function.hs
@@ -6,7 +6,6 @@ module Lude.Function (
const,
flip,
on,
- fork,
compose00#,
(.#),
compose00,
@@ -68,12 +67,6 @@ on
on f g = lam2# \x y -> app2# f (app# g x) (app# g y)
{-# INLINE on #-}
-fork
- :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s) {t :: Repr} (c :: Type# t) {u :: Repr} (d :: Type# u)
- . (Functional# r, Functional# s, Functional# t) => (b -> c -> d) -> (a -> b) -> (a -> c) -> (a -> d)
-fork f g h = lam# \x -> app2# f (app# g x) (app# h x)
-{-# INLINE fork #-}
-
--------------------------------------------------------------------------------
-- Composition
diff --git a/src/Lude/Haskell/Category.hs b/src/Lude/Haskell/Category.hs
@@ -82,11 +82,11 @@ type Function :: Cat Type
type Function = Function# Repr.BoxL
-- | Natural transformations to `Function`/`->`
-type (~>) :: forall i (r :: Repr). Cat (i -> Type# r)
+type (~>) :: forall i (r :: Repr) (s :: Repr). (i -> Type# r) -> (i -> Type# s) -> Type
type f ~> g = forall x. f x -> g x
-- | Binatural transformations to `Function`/`->`
-type (~~>) :: forall i j (r :: Repr). Cat (i -> j -> Type# r)
+type (~~>) :: forall i j (r :: Repr) (s :: Repr). (i -> j -> Type# r) -> (i -> j -> Type# s) -> Type
type f ~~> g = forall x y. f x y -> g x y
identityFunction :: forall {r :: Repr} (a :: Type# r). (Functional# r) => a -> a
diff --git a/src/Lude/Pair.hs b/src/Lude/Pair.hs
@@ -1,42 +1,174 @@
module Lude.Pair (
Pair,
+ MkPair,
pattern MkPair,
type (*),
- fst,
- snd,
- Fst,
- Snd,
+ outl,
+ outr,
+ dup,
+ swap,
+ curry,
+ uncurry,
+ Outl,
+ Outr,
+ --
+ fbimap,
+ flmap,
+ frmap,
+ fbmap,
+ fbmap1,
+ foutl,
+ foutr,
+ fdup,
+ fswap,
) where
+import Data.Tuple qualified as Base
+
import Lude.Haskell
-import Prelude.Experimental qualified as GHC
--- TODO: Generalize fst and snd (and fst1 and snd1?) with Cartesian class.
--- Probably name them outl and outr for symmetry with inl and inr.
+-- TODO: Generalize with Cartesian class.
+
+--------------------------------------------------------------------------------
+
+infixl 7 *
--------------------------------------------------------------------------------
type Pair :: Type -> Type -> Type
-type Pair = GHC.Tuple2
+type Pair = Tuple2
-- For consistency
+type MkPair :: a -> b -> Pair a b
+type MkPair = (,)
pattern MkPair :: a -> b -> Pair a b
pattern MkPair a b = (a, b)
{-# COMPLETE MkPair #-}
type (*) = Pair
-infixl 7 *
-fst :: Pair a b -> a
-fst (MkPair x _) = x
+outl :: forall a b. Pair a b -> a
+outl = Base.fst
+
+outr :: forall a b. Pair a b -> b
+outr = Base.snd
+
+dup :: forall a. a -> Pair a a
+dup x = (x, x)
+
+swap :: forall a b. Pair a b -> Pair b a
+swap = Base.swap
+
+curry :: forall a b c. (Pair a b -> c) -> (a -> b -> c)
+curry = Base.curry
+
+uncurry :: forall a b c. (a -> b -> c) -> (Pair a b -> c)
+uncurry = Base.uncurry
+
+type Outl :: forall {a} {b}. Pair a b -> a
+type family Outl _ where
+ Outl (a, b) = a
+
+type Outr :: forall {a} {b}. Pair a b -> b
+type family Outr _ where
+ Outr (a, b) = b
+
+--------------------------------------------------------------------------------
+-- CPS/Yoneda Pair Operations
+
+-- TODO: Figure-out the best way to generalize this idea.
+
+type CoTuple :: forall {k} {r :: Repr}. k -> Type# r -> Type
+type family CoTuple _ _ where
+ CoTuple () z = z -- TODO: must lift somehow
+ CoTuple (a) z = a -> z
+ CoTuple (a, b) z = a -> b -> z
+ CoTuple (a, b, c) z = a -> b -> c -> z
+ CoTuple (a, b, c, d) z = a -> b -> c -> d -> z
+ CoTuple (a, b, c, d, e) z = a -> b -> c -> d -> e -> z
+ CoTuple (a, b, c, d, e, f) z = a -> b -> c -> d -> e -> f -> z
+ CoTuple (a, b, c, d, e, f, g) z = a -> b -> c -> d -> e -> f -> g -> z
+ CoTuple (a, b, c, d, e, f, g, h) z = a -> b -> c -> d -> e -> f -> g -> h -> z
+ CoTuple (a, b, c, d, e, f, g, h, i) z = a -> b -> c -> d -> e -> f -> g -> h -> i -> z
+ CoTuple (MkTuple1 a) z = a -> z
+
+-- | A morphism @Tuple a -> Tuple b@ for tuples of types @a@ and @b@ with
+-- arbitrary representations, without requiring `Functional#` tuples
+type HomTuple :: forall {k} {l}. k -> l -> Type
+type HomTuple a b = forall {r :: Repr} (z :: Type# r). CoTuple b z -> CoTuple a z
+
+-- | A morphism @a * b -> a' * b'@ for types @a@, @b@, @a'@, and @b'@ with
+-- arbitrary representations, without requiring `Functional#` tuples
+type HomPair
+ :: forall {r :: Repr} {s :: Repr} {r' :: Repr} {s' :: Repr}
+ . Type# r -> Type# s -> Type# r' -> Type# s' -> Type
+type HomPair a b a' b' = HomTuple (a, b) (a', b')
+
+-- type HomPair a b a' b' = forall {t :: Repr} (c :: Type# t). (a' -> b' -> c) -> (a -> b -> c)
+
+-- | A binatural transformation @f * g ~~> f' * g'@ for type-valued functors
+-- @f@, @g@, @f'@, and @g'@ with arbitrary representations, without requiring
+-- `Functional#` tuples
+type HomPair1
+ :: forall {i} {j} {r :: Repr} {s :: Repr} {r' :: Repr} {s' :: Repr}
+ . (i -> Type# r) -> (j -> Type# s) -> (i -> Type# r') -> (j -> Type# s') -> Type
+type HomPair1 f g f' g' = forall x y. HomPair (f x) (g y) (f' x) (g' y)
+
+fbimap
+ :: forall {r :: Repr} (a :: Type# r) {r' :: Repr} (a' :: Type# r') {s :: Repr} (b :: Type# s) {s' :: Repr} (b' :: Type# s')
+ . (Functional# r, Functional# r', Functional# s, Functional# s')
+ => (a -> a') -> (b -> b') -> HomPair a b a' b'
+fbimap f g k = lam2# \x y -> app2# k (app# f x) (app# g y) -- flmap f . frmap g
+{-# INLINE fbimap #-}
+
+flmap
+ :: forall {r :: Repr} (a :: Type# r) {r' :: Repr} (a' :: Type# r') {s :: Repr} (b :: Type# s)
+ . (Functional# r, Functional# r', Functional# s)
+ => (a -> a') -> HomPair a b a' b
+flmap f k = lam2# \x y -> app2# k (app# f x) y -- flip (.#)
+{-# INLINE flmap #-}
+
+frmap
+ :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s) {s' :: Repr} (b' :: Type# s')
+ . (Functional# r, Functional# s, Functional# s')
+ => (b -> b') -> HomPair a b a b'
+frmap g k = lam2# \x y -> app2# k x (app# g y) -- flip (*.#)
+{-# INLINE frmap #-}
+
+fbmap
+ :: forall {r :: Repr} (a :: Type# r) {r' :: Repr} (a' :: Type# r')
+ . (Functional# r, Functional# r')
+ => (a -> a') -> HomPair a a a' a'
+fbmap h = fbimap h h
+{-# INLINE fbmap #-}
+
+fbmap1
+ :: forall {i} {r :: Repr} (f :: i -> Type# r) {r' :: Repr} (f' :: i -> Type# r')
+ . (Functional# r, Functional# r')
+ => (f ~> f') -> HomPair1 f f f' f'
+fbmap1 h = fbimap h h
+{-# INLINE fbmap1 #-}
+
+foutl
+ :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s)
+ . (Functional# r, Functional# s) => HomTuple (a, b) (a)
+foutl k = lam2# \x _ -> app# k x
+{-# INLINE foutl #-}
-snd :: Pair a b -> b
-snd (MkPair _ y) = y
+foutr
+ :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s)
+ . (Functional# r, Functional# s) => HomTuple (a, b) (b)
+foutr k = lam2# \_ y -> app# k y
+{-# INLINE foutr #-}
-type Fst :: forall {a} {b}. Pair a b -> a
-type family Fst _ where
- Fst (a, b) = a
+fdup
+ :: forall {r :: Repr} (a :: Type# r)
+ . (Functional# r) => HomTuple (a) (a, a)
+fdup k = lam# \x -> app2# k x x
+{-# INLINE fdup #-}
-type Snd :: forall {a} {b}. Pair a b -> b
-type family Snd _ where
- Snd (a, b) = b
+fswap
+ :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s)
+ . (Functional# r, Functional# s) => HomPair b a a b
+fswap k = lam2# \x y -> app2# k y x
+{-# INLINE fswap #-}
