commit bc2229ec25c50ef3c3a4d73dbd3c301e6eca4b60
parent 9400c550dc27c17893c1e454cef9c1d7b7089e61
Author: Robert Russell <robert@rr3.xyz>
Date: Wed, 16 Sep 2026 16:44:01 -0700
Function: add Repr-polymorphic combinators
Diffstat:
6 files changed, 154 insertions(+), 58 deletions(-)
diff --git a/Todo/Lude.hs b/Todo/Lude.hs
@@ -108,44 +108,6 @@ class Unlift a where
--------------------------------------------------------------------------------
-type SKI :: Rep -> Constraint
-class SKI r where
- _S :: forall (a :: Type r). a -> GHC.Int
-
---------------------------------------------------------------------------------
-
--- TODO: Don't require the objects to be Type r. E.g., functor categories don't
--- fit this shape.
-type Mor obj r = obj -> obj -> Type r
-type Category :: forall obj r. Mor obj r -> Constraint
-class Category @obj mor where
- identity :: forall (a :: obj). Lev (mor a a)
- compose :: forall (a :: obj) (b :: obj) (c :: obj). mor b c -> mor a b -> mor a c
-
-type CatFunctor :: forall obj0 obj1 r0 r1. (obj0 -> obj1) -> Mor obj0 r0 -> Mor obj1 r1 -> Constraint
-class (Category @obj0 mor0, Category @obj1 mor1) => CatFunctor @obj0 @obj1 f mor0 mor1 where
- map :: forall (a :: obj0) (b :: obj0). mor0 a b -> mor1 (f a) (f b)
-
---------------------------------------------------------------------------------
-
--- type Hask r = Hask0 r
--- type Hask0 r = Mor (Type r) LRep
--- type Hask1 k0 r = Mor (k0 -> Type r) LRep
--- type Hask2 k0 k1 r = Mor (k0 -> k1 -> Type r) LRep
--- type Hask3 k0 k1 k2 r = Mor (k0 -> k1 -> k2 -> Type r) LRep
-
-newtype Whoa a b = Whoa (forall i j. a i j -> b i j)
-instance Category @(k0 -> k1 -> LType) @LRep Whoa where
- identity = Whoa \a -> a
- compose (Whoa f) (Whoa g) = Whoa \ @i @j a -> f @i @j (g @i @j a)
-
-newtype Fix2 f i j = Fix2 (f (Fix2 f i j) i j)
-
--- type
--- type Functor f = CatFunctor f (Hask r) (Hask s)
-
---------------------------------------------------------------------------------
-
-- type Functor :: forall r s. (Type r -> Type s) -> Constraint
-- class Functor @r f where
-- map :: forall (a :: Type r) (b :: Type r). (a -> b) -> f a -> f b
@@ -366,8 +328,6 @@ newtype Fix2 f i j = Fix2 (f (Fix2 f i j) i j)
{-
-type Iso (mor :: obj -> obj -> TypeL) a b = (mor a b, mor b a) -- TODO: use strict pair
-
class (Bifunctor f, LDomOf f ~ Hask ρ, RDomOf f ~ Hask ρ) => Monoidal (f :: Type ρ -> Type ρ -> Type ρ) where
type UnitOf f :: Type ρ
unitl :: Iso (Hask ρ) (f (UnitOf f) a) a
diff --git a/src/Lude.hs b/src/Lude.hs
@@ -5,7 +5,8 @@ module Lude (
import Lude.Algebra as X
import Lude.Bool as X
import Lude.Constraint as X
-import Lude.Function as X
+import Lude.Equivalence as X
+import Lude.Function as X hiding ((.))
import Lude.Haskell as X
import Lude.IO as X
import Lude.List as X
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -199,16 +199,16 @@ instance (Categorical p, Categorical q) => Functorial (NT p q) where
--------------------------------------------------------------------------------
-- Haskell
-instance Categorical Function where
+instance forall (r :: Repr). (Functional# r) => Categorical (Function @r) where
identity = identityFunction
compose = composeFunction
-instance Functorial (Function a) where
+instance forall (r :: Repr) (a :: Type @r). (Functional# r) => Functorial (Function @r a) where
type Dom (Function a) = Function
type Cod (Function a) = Function
map = compose
-instance Functorial Function where
+instance forall (r :: Repr). (Functional# r) => Functorial (Function @r) where
type Dom Function = Dual Function
type Cod Function = Function ==> Function
map (MkDual f) = Naturally (. f)
diff --git a/src/Lude/Function.hs b/src/Lude/Function.hs
@@ -1,13 +1,143 @@
module Lude.Function (
+ identity,
+ app,
+ ($),
+ rapp,
+ (&),
const,
flip,
on,
- ($),
- (&),
+ compose00,
+ (.),
+ compose01,
+ (.*),
+ compose10,
+ (*.),
+ compose11,
+ (*.*),
) where
-import Data.Function (const, flip, on, ($), (&))
+import Data.Function (($))
+
+import Lude.Algebra.Category.Core (identity)
+import Lude.Haskell
-- TODO: Generalize some of this? E.g., for CCCs?
+-- TODO: How should we deal with the (.) naming conflict with category?
+
+-- TODO: Repr-generic S and Phi combinators?
+
--------------------------------------------------------------------------------
+
+app :: forall {r :: Repr} (a :: Type @r) {s :: Repr} (b :: Type @s). (a -> b) -> (a -> b)
+app = ($)
+{-# INLINE app #-}
+
+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
+(&) = rapp
+{-# INLINE rapp #-}
+{-# INLINE (&) #-}
+
+const
+ :: forall {r :: Repr} (a :: Type @r) {s :: Repr} (b :: Type @s)
+ . (Functional# r, Functional# s) => a -> (b -> a)
+const = lam2# \x _ -> x
+{-# INLINE const #-}
+
+flip
+ :: forall {r :: Repr} (a :: Type @r) {s :: Repr} (b :: Type @s) {t :: Repr} (c :: Type @t)
+ . (Functional# r, Functional# s) => (a -> b -> c) -> (b -> a -> c)
+flip f = lam2# \y x -> app2# f x y
+{-# INLINE flip #-}
+
+on
+ :: forall {r :: Repr} (a :: Type @r) {s :: Repr} (b :: Type @s) {t :: Repr} (c :: Type @t)
+ . (Functional# r, Functional# s) => (b -> b -> c) -> (a -> b) -> (a -> a -> c)
+on f g = lam2# \x y -> app2# f (app# g x) (app# g y)
+{-# INLINE on #-}
+
+--------------------------------------------------------------------------------
+-- Composition
+
+compose00,
+ (.)
+ :: forall {r0 :: Repr} (a0 :: Type @r0) {s :: Repr} (b :: Type @s) {t :: Repr} (c :: Type @t)
+ . (Functional# r0, Functional# s) => (b -> c) -> (a0 -> b) -> (a0 -> c)
+compose00 = composeFunction
+(.) = compose00
+{-# INLINE compose00 #-}
+{-# INLINE (.) #-}
+
+compose01,
+ (.*)
+ :: forall {r0 :: Repr} (a0 :: Type @r0) {r1 :: Repr} (a1 :: Type @r1) {s :: Repr} (b :: Type @s) {t :: Repr} (c :: Type @t)
+ . (Functional# r0, Functional# r1, Functional# s) => (b -> c) -> (a0 -> a1 -> b) -> (a0 -> a1 -> c)
+compose01 g f = lam# \x0 -> compose00 g (f `app#` x0)
+(.*) = compose01
+{-# INLINE compose01 #-}
+{-# INLINE (.*) #-}
+
+compose10,
+ (*.)
+ :: forall {r0 :: Repr} (a0 :: Type @r0) {s0 :: Repr} (b0 :: Type @s0) {s :: Repr} (b :: Type @s) {t :: Repr} (c :: Type @t)
+ . (Functional# r0, Functional# s0, Functional# s) => (b0 -> b -> c) -> (a0 -> b) -> (b0 -> a0 -> c)
+compose10 g f = lam# \y -> compose00 (g `app#` y) f
+(*.) = compose10
+{-# INLINE compose10 #-}
+{-# INLINE (*.) #-}
+
+compose11,
+ (*.*)
+ :: forall {r0 :: Repr} (a0 :: Type @r0) {r1 :: Repr} (a1 :: Type @r1) {s0 :: Repr} (b0 :: Type @s0) {s :: Repr} (b :: Type @s) {t :: Repr} (c :: Type @t)
+ . (Functional# r0, Functional# r1, Functional# s0, Functional# s) => (b0 -> b -> c) -> (a0 -> a1 -> b) -> (b0 -> a0 -> a1 -> c)
+compose11 g f = lam# \y -> compose01 (g `app#` y) f
+(*.*) = compose11
+{-# INLINE compose11 #-}
+{-# INLINE (*.*) #-}
+
+-- compose02,
+-- (.**)
+-- :: forall {r0 :: Repr} (a0 :: Type @r0) {r1 :: Repr} (a1 :: Type @r1) {r2 :: Repr} (a2 :: Type @r2) {s :: Repr} (b :: Type @s) {t :: Repr} (c :: Type @t)
+-- . (Functional# r0, Functional# r1, Functional# r2, Functional# s) => (b -> c) -> (a0 -> a1 -> a2 -> b) -> (a0 -> a1 -> a2 -> c)
+-- compose02 g f = lam# \x -> compose01 g (f `app#` x)
+-- (.**) = compose02
+-- {-# INLINE compose02 #-}
+-- {-# INLINE (.**) #-}
+
+-- compose12,
+-- (*.**)
+-- :: forall {r0 :: Repr} (a0 :: Type @r0) {r1 :: Repr} (a1 :: Type @r1) {r2 :: Repr} (a2 :: Type @r2) {s0 :: Repr} (b0 :: Type @s0) {s :: Repr} (b :: Type @s) {t :: Repr} (c :: Type @t)
+-- . (Functional# r0, Functional# r1, Functional# r2, Functional# s0, Functional# s) => (b0 -> b -> c) -> (a0 -> a1 -> a2 -> b) -> (b0 -> a0 -> a1 -> a2 -> c)
+-- compose12 g f = lam# \y -> compose02 (g `app#` y) f
+-- (*.**) = compose12
+-- {-# INLINE compose12 #-}
+-- {-# INLINE (*.**) #-}
+
+-- compose20,
+-- (**.)
+-- :: forall {r0 :: Repr} (a0 :: Type @r0) {s0 :: Repr} (b0 :: Type @s0) {s1 :: Repr} (b1 :: Type @s1) {s :: Repr} (b :: Type @s) {t :: Repr} (c :: Type @t)
+-- . (Functional# r0, Functional# s0, Functional# s1, Functional# s) => (b0 -> b1 -> b -> c) -> (a0 -> b) -> (b0 -> b1 -> a0 -> c)
+-- compose20 g f = lam# \y -> compose10 (g `app#` y) f
+-- (**.) = compose20
+-- {-# INLINE compose20 #-}
+-- {-# INLINE (**.) #-}
+
+-- compose21,
+-- (**.*)
+-- :: forall {r0 :: Repr} (a0 :: Type @r0) {r1 :: Repr} (a1 :: Type @r1) {s0 :: Repr} (b0 :: Type @s0) {s1 :: Repr} (b1 :: Type @s1) {s :: Repr} (b :: Type @s) {t :: Repr} (c :: Type @t)
+-- . (Functional# r0, Functional# r1, Functional# s0, Functional# s1, Functional# s) => (b0 -> b1 -> b -> c) -> (a0 -> a1 -> b) -> (b0 -> b1 -> a0 -> a1 -> c)
+-- compose21 g f = lam# \y -> compose11 (g `app#` y) f
+-- (**.*) = compose21
+-- {-# INLINE compose21 #-}
+-- {-# INLINE (**.*) #-}
+
+-- compose22,
+-- (**.**)
+-- :: forall {r0 :: Repr} (a0 :: Type @r0) {r1 :: Repr} (a1 :: Type @r1) {r2 :: Repr} (a2 :: Type @r2) {s0 :: Repr} (b0 :: Type @s0) {s1 :: Repr} (b1 :: Type @s1) {s :: Repr} (b :: Type @s) {t :: Repr} (c :: Type @t)
+-- . (Functional# r0, Functional# r1, Functional# r2, Functional# s0, Functional# s1, Functional# s) => (b0 -> b1 -> b -> c) -> (a0 -> a1 -> a2 -> b) -> (b0 -> b1 -> a0 -> a1 -> a2 -> c)
+-- compose22 g f = lam# \y -> compose12 (g `app#` y) f
+-- (**.**) = compose22
+-- {-# INLINE compose22 #-}
+-- {-# INLINE (**.**) #-}
diff --git a/src/Lude/Haskell/Category.hs b/src/Lude/Haskell/Category.hs
@@ -51,10 +51,11 @@ module Lude.Haskell.Category (
) where
import GHC.Exts qualified as GHC
-import Prelude qualified as Base
import Lude.Haskell.Constraint
+import Lude.Haskell.Functional
import Lude.Haskell.Kind
+import Lude.Haskell.Repr
import Lude.Haskell.Type
-- NOTE: `Entailment`/`:-` is to `Constraint` what `Function`/`->` is to `Type`.
@@ -72,8 +73,8 @@ type Cat :: Kind -> Kind
type Cat i = i -> i -> Type
-- | Functions between two types (which form a category)
-type Function :: Cat Type
-type Function = (->)
+type Function :: forall (r :: Repr). Cat (Type @r)
+type Function @r = (->)
-- | Natural transformations to `Function`/`->`
type (~>) :: forall i r. Cat (i -> Type @r)
@@ -83,11 +84,15 @@ type f ~> g = forall x. f x -> g x
type (~~>) :: forall i j r. Cat (i -> j -> Type @r)
type f ~~> g = forall x y. f x y -> g x y
-identityFunction :: forall a. a -> a
-identityFunction = Base.id
+identityFunction :: forall {r :: Repr} (a :: Type @r). (Functional# r) => a -> a
+identityFunction = lam# \x -> x
+{-# INLINE identityFunction #-}
-composeFunction :: forall a b c. (b -> c) -> (a -> b) -> (a -> c)
-composeFunction = (Base..)
+composeFunction
+ :: forall {r :: Repr} (a :: Type @r) {s :: Repr} (b :: Type @s) {t :: Repr} (c :: Type @t)
+ . (Functional# r, Functional# s) => (b -> c) -> (a -> b) -> (a -> c)
+composeFunction f g = lam# \x -> f `app#` (g `app#` x)
+{-# INLINE composeFunction #-}
-- | Entailments between two constraints (which form a category)
type Entailment :: Cat Constraint
diff --git a/src/Lude/Haskell/Functional.hs b/src/Lude/Haskell/Functional.hs
@@ -31,13 +31,13 @@ class Functional# r where
app# :: forall (a :: Type @r) {s} (b :: Type @s). (a -> b) -> (Lev a -> b)
lam2#
- :: forall {r :: Repr} (a :: Type @r) (b :: Type @r) {s} (c :: Type @s)
- . (Functional# r) => (Lev a -> Lev b -> c) -> (a -> b -> c)
+ :: forall {r0 :: Repr} (a0 :: Type @r0) {r1 :: Repr} (a1 :: Type @r1) {s} (b :: Type @s)
+ . (Functional# r0, Functional# r1) => (Lev a0 -> Lev a1 -> b) -> (a0 -> a1 -> b)
lam2# f = lam# \x -> lam# (f x)
app2#
- :: forall {r :: Repr} (a :: Type @r) (b :: Type @r) {s} (c :: Type @s)
- . (Functional# r) => (a -> b -> c) -> (Lev a -> Lev b -> c)
+ :: forall {r0 :: Repr} (a0 :: Type @r0) {r1 :: Repr} (a1 :: Type @r1) {s} (b :: Type @s)
+ . (Functional# r0, Functional# r1) => (a0 -> a1 -> b) -> (Lev a0 -> Lev a1 -> b)
app2# f x y = f `app#` x `app#` y
--------------------------------------------------------------------------------
