lude

commit dfda2dd288c7d211f21a364e46ffd83023467fe3
parent 01daa79f631bc664ce0e98dbaf3f0bdc77d43da7
Author: Robert Russell <robert@rr3.xyz>
Date:   Sun,  4 Oct 2026 13:27:55 -0700

Haskell: make Function consistent with Type

Diffstat:
M
src/Lude/Algebra/Category/Core.hs
 | 
16
++++++++--------
M
src/Lude/Haskell/Category.hs
 | 
14
++++++++++----

2 files changed, 18 insertions(+), 12 deletions(-)
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -46,7 +46,7 @@ infixr 1 ==>
 
 type DefaultCat :: forall i -> Cat i
 type family DefaultCat i
-type instance DefaultCat Type = Function
+type instance DefaultCat (Type# r) = Function# r
 type instance DefaultCat (k -> l) = DefaultCat k ==> DefaultCat l
 
 -- NOTE: This is not allowed, because Type = Constraint :(
@@ -198,18 +198,18 @@ instance (Categorical p, Categorical q) => Functorial (NT p q) where
 --------------------------------------------------------------------------------
 -- Haskell
 
-instance forall (r :: Repr). (Functional# r) => Categorical (Function @r) where
+instance forall (r :: Repr). (Functional# r) => Categorical (Function# r) where
     identity = identityFunction
     compose = composeFunction
 
-instance forall (r :: Repr) (a :: Type# r). (Functional# r) => Functorial (Function @r a) where
-    type Dom (Function a) = Function
-    type Cod (Function a) = Function
+instance forall (r :: Repr) (a :: Type# r). (Functional# r) => Functorial (Function# r a) where
+    type Dom (Function# r a) = Function# r
+    type Cod (Function# r a) = Function
     map = compose
 
-instance forall (r :: Repr). (Functional# r) => Functorial (Function @r) where
-    type Dom Function = Dual Function
-    type Cod Function = Function ==> Function
+instance forall (r :: Repr). (Functional# r) => Functorial (Function# r) where
+    type Dom (Function# r) = Dual (Function# r)
+    type Cod (Function# r) = Function# r ==> Function
     map (MkDual f) = Naturally (. f)
 
 instance Categorical Entailment where
diff --git a/src/Lude/Haskell/Category.hs b/src/Lude/Haskell/Category.hs
@@ -1,5 +1,6 @@
 module Lude.Haskell.Category (
     Cat,
+    Function#,
     Function,
     type (~>),
     type (~~>),
@@ -55,6 +56,7 @@ import GHC.Exts qualified as GHC
 import Lude.Haskell.Constraint
 import Lude.Haskell.Core
 import Lude.Haskell.Functional
+import Lude.Haskell.Repr qualified as Repr
 import Lude.Haskell.Type
 
 -- NOTE: `Entailment`/`:-` is to `Constraint` what `Function`/`->` is to `Type`.
@@ -71,9 +73,13 @@ infixl 1 \\
 type Cat :: Kind -> Kind
 type Cat i = i -> i -> Type
 
--- | Functions between two types (which form a category)
-type Function :: forall (r :: Repr). Cat (Type# r)
-type Function @r = (->)
+-- | Functions between two types (of a given representation), which form a category
+type Function# :: forall (r :: Repr) -> Cat (Type# r)
+type Function# _ = (->)
+
+-- | Functions between two (lazy boxed) types, which form a category
+type Function :: Cat Type
+type Function = Function# Repr.BoxL
 
 -- | Natural transformations to `Function`/`->`
 type (~>) :: forall i (r :: Repr). Cat (i -> Type# r)
@@ -93,7 +99,7 @@ composeFunction
 composeFunction f g = lam# \x -> f `app#` (g `app#` x)
 {-# INLINE composeFunction #-}
 
--- | Entailments between two constraints (which form a category)
+-- | Entailments between two constraints, which form a category
 type Entailment :: Cat Constraint
 newtype Entailment a b = Entail {unEntail :: (a) => Evidence b}