commit 54e567bd598043672529bafca8d9d586e1e9d1e4
parent 762bfc7cb184e0ff4ca4c7ab41044d6fd303413b
Author: Robert Russell <robert@rr3.xyz>
Date: Wed, 7 Oct 2026 17:06:47 -0700
Algebra.Category, Function: add application operators (with good fixity)
Diffstat:
3 files changed, 52 insertions(+), 38 deletions(-)
diff --git a/src/Lude/Algebra/Category/Bifunctor.hs b/src/Lude/Algebra/Category/Bifunctor.hs
@@ -13,6 +13,7 @@ module Lude.Algebra.Category.Bifunctor (
rmap,
pattern Binaturally,
bicomp,
+ ($^^),
) where
import Lude.Algebra.Category.Core
@@ -26,6 +27,10 @@ import Lude.Pair
--------------------------------------------------------------------------------
+infixl 1 $^^
+
+--------------------------------------------------------------------------------
+
-- NOTE: We ought not need to assume that BidomR p and Bicod p are categorical,
-- because the Categorical (NT _ _) instance assumes it, but maybe there's
-- some reason the constraint solver can't safely deduce that.
@@ -111,6 +116,9 @@ bicomp
-> (forall (a :: i) (b :: j). (Obj p a, Obj q b) => f a b `r` g a b)
bicomp m = comp (comp m)
+($^^) :: forall {i} {j} (p :: Cat i) (q :: Cat j) (f :: i -> j -> Type) (g :: i -> j -> Type) (x :: i) (y :: j). (Obj p x, Obj q y) => NT p (q ==> Function) f g -> f x y -> g x y
+($^^) h = bicomp h
+
--------------------------------------------------------------------------------
-- | A semigroup structure on a category, represented as a bifunctor
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -25,13 +25,13 @@ module Lude.Algebra.Category.Core (
type (==>),
NTDom,
NTCod,
+ ($^),
) where
import Data.Coerce
import Prelude qualified as Base
import Lude.Constraint.Predicate
-import Lude.Function
import Lude.Haskell
import Lude.IO
import Lude.List
@@ -42,6 +42,7 @@ import Lude.List
infixr 9 .
infixr 1 ==>
+infixl 1 $^
--------------------------------------------------------------------------------
@@ -195,6 +196,9 @@ instance (Categorical p, Categorical q) => Functorial (NT p q) where
type Cod (NT p q) = NT p q ==> Function
map (MkDual f) = Naturally (. f)
+($^) :: forall {i} (p :: Cat i) (f :: i -> Type) (g :: i -> Type) (x :: i). (Obj p x) => NT p Function f g -> f x -> g x
+($^) h = comp h
+
--------------------------------------------------------------------------------
-- Haskell
@@ -242,46 +246,46 @@ 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 (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 (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 (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 (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 (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 (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)
+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
@@ -24,8 +24,6 @@ module Lude.Function (
(*.*),
) where
-import Data.Function (($))
-
import Lude.Haskell
-- TODO: Generalize some of this? E.g., for CCCs?
@@ -34,14 +32,18 @@ import Lude.Haskell
--------------------------------------------------------------------------------
+infixl 1 $
+infixl 0 &
infixr 9 .*, *., *.*
infixr 9 .#, .*#, *.#, *.*#
--------------------------------------------------------------------------------
-app :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s). (a -> b) -> (a -> b)
-app = ($)
+app, ($) :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s). (a -> b) -> (a -> b)
+app f = f
+($) = app
{-# INLINE app #-}
+{-# INLINE ($) #-}
rapp, (&) :: forall {r :: Repr} (a :: Type# r) {s :: Repr} (b :: Type# s). (Functional# r) => a -> (a -> b) -> b
rapp = lam# \x f -> app# f x
