lude

commit e579946c86f2f743147fb0de191edde012c66511
parent 28d9bc9550ad835f3cea14d54c6226c6e4915580
Author: Robert Russell <robert@rr3.xyz>
Date:   Tue, 10 Mar 2026 13:51:11 -0700

Improve Kind

Diffstat:
M
src/Lude/Algebra.hs
 | 
11
++++++-----
M
src/Lude/Kind.hs
 | 
37
++++++++++++++++++++++++++-----------

2 files changed, 32 insertions(+), 16 deletions(-)
diff --git a/src/Lude/Algebra.hs b/src/Lude/Algebra.hs
@@ -1,6 +1,7 @@
 {-# OPTIONS_GHC -Wno-unused-top-binds #-}
 
 module Lude.Algebra (
+    Cat,
     Category (..),
     Functor (..),
     Bifunctor (..),
@@ -19,7 +20,7 @@ import Lude.Repr qualified as Repr
 --------------------------------------------------------------------------------
 -- Category
 
-type Cat k r = k -> k -> Type r
+type Cat k r = k -> k -> Type @r
 
 type Category :: forall k r. Cat k r -> Constraint
 class Category (cat :: Cat k r) where
@@ -126,7 +127,7 @@ class (Hypoplexal cat f) => Plexal @k cat f where
 
 --------------------------------------------------------------------------------
 
-type Hask :: forall r. Cat (Type r) Repr.BoxL
+type Hask :: forall r. Cat (Type @r) Repr.BoxL
 type Hask @r = (->)
 
 instance Category (Hask @Repr.BoxL) where
@@ -162,7 +163,7 @@ instance (Category cat) => Category (Op cat) where
 --------------------------------------------------------------------------------
 
 -- | Natural transformations to Hask
-type (~>) :: forall k (r :: Repr). Cat (k -> Type r) Repr.BoxL
+type (~>) :: forall k (r :: Repr). Cat (k -> Type @r) Repr.BoxL
 type f ~> g = forall a. f a -> g a
 
 {-
@@ -196,9 +197,9 @@ instance RFunctor (Endofunct Hask) (Endofunct Hask) Compose where
 
 --------------------------------------------------------------------------------
 
--- type HypoMonoid :: forall r. Type r -> Constraint
+-- type HypoMonoid :: forall r. Type @r -> Constraint
 -- class HypoMonoid a where
 --     combine :: a -> a -> a
--- type Monoid :: forall r. Type r -> Constraint
+-- type Monoid :: forall r. Type @r -> Constraint
 -- class (HypoMonoid a) => Monoid a where
 --     unit :: a
diff --git a/src/Lude/Kind.hs b/src/Lude/Kind.hs
@@ -1,27 +1,42 @@
+{-# OPTIONS_GHC -Wno-unused-foralls #-}
+
 module Lude.Kind (
-    Constraint,
+    Kind,
     Type,
     TypeL,
     TypeU,
-    Kind,
+    Constraint,
+    ConstraintL,
+    ConstraintU,
     Lev,
 ) where
 
-import GHC.Exts (Constraint)
 import GHC.Exts qualified as GHC
 
+import Lude.Repr (Repr)
 import Lude.Repr qualified as Repr
 
--- TODO: CONSTRAINT (Repr-indexed)
+--------------------------------------------------------------------------------
+
+type Kind = GHC.TYPE Repr.BoxL
 
 --------------------------------------------------------------------------------
 
-type Type = GHC.TYPE
-type TypeL = Type Repr.BoxL
-type TypeU = Type Repr.BoxU
+type Type :: forall (r :: Repr). Kind
+type Type @r = GHC.TYPE r
 
--- | An alias for `TypeL`.
-type Kind = TypeL
+type TypeL = Type @Repr.BoxL
+type TypeU = Type @Repr.BoxU
+
+--------------------------------------------------------------------------------
+
+type Constraint :: forall (r :: Repr). Kind
+type Constraint @r = GHC.CONSTRAINT r
+
+type ConstraintL = Constraint @Repr.BoxL
+type ConstraintU = Constraint @Repr.BoxU
+
+--------------------------------------------------------------------------------
 
 -- | Used to declare unlifted values at the top-level. For example, for any @r@,
 -- @A :: Type r@, and @bar :: A@:
@@ -29,5 +44,5 @@ type Kind = TypeL
 -- foo :: Lev A
 -- foo = bar
 -- @
-type Lev :: forall r. Type r -> TypeL
-type Lev (a :: Type r) = (() :: Constraint) => a
+type Lev :: forall r. Type @r -> Type
+type Lev a = (() :: ConstraintL) => a