commit 1e3c6d28859992b3781cd8f69c261269871a00b6
parent 05d8beadfe3a415754aad808574bf9dd89f776c1
Author: Robert Russell <robert@rr3.xyz>
Date: Sun, 15 Mar 2026 14:19:14 -0700
Clean up
Diffstat:
6 files changed, 196 insertions(+), 102 deletions(-)
diff --git a/src/Lude/Algebra/Category.hs b/src/Lude/Algebra/Category.hs
@@ -8,54 +8,32 @@ module Lude.Algebra.Category (
Functor (..),
) where
+import Lude.Constraint
import Lude.Either
import Lude.Kind
import Lude.Pair
-- TODO: Semicategory
-- TODO: Allow non-BoxL morphism Repr?
+-- TODO: Filterable is functor from Kleisli Option to Hask
-type Type1 i = i -> Type
-type Type2 i = i -> i -> Type
+-- type Type2 i = i -> i -> Type
+-- type Constraint2 i = i -> i -> Constraint
-type Constraint1 i = i -> Constraint
-type Constraint2 i = i -> i -> Constraint
+-- type Pair2 :: forall i j. Type2 i -> Type2 j -> Type2 (i × j)
+-- data Pair2 p q a b where
+-- Pair2 :: p a0 b0 -> q a1 b1 -> Pair2 p q '(a0, a1) '(b0, b1)
-type Pair1 :: forall i j. Type1 i -> Type1 j -> Type1 (i × j)
-data Pair1 p q a where
- Pair1 :: p a0 -> q a1 -> Pair1 p q '(a0, a1)
+-- type (×^^) = Pair2
+-- infixl 7 ×^^
-fst1 :: Pair1 p q '(i, j) -> p i
-fst1 (Pair1 x _) = x
+-- type Either2 :: forall i j. Type2 i -> Type2 j -> Type2 (i + j)
+-- data Either2 p q a b where
+-- L2 :: p a b -> Either2 p q (L a) (L b)
+-- R2 :: q a b -> Either2 p q (R a) (R b)
-snd1 :: Pair1 p q '(i, j) -> q j
-snd1 (Pair1 _ y) = y
-
-type (×^) = Pair1
-infixl 7 ×^
-
-type Pair2 :: forall i j. Type2 i -> Type2 j -> Type2 (i × j)
-data Pair2 p q a b where
- Pair2 :: p a0 b0 -> q a1 b1 -> Pair2 p q '(a0, a1) '(b0, b1)
-
-type (×^^) = Pair2
-infixl 7 ×^^
-
-type Either1 :: forall i j. Type1 i -> Type1 j -> Type1 (i + j)
-data Either1 p q a where
- L1 :: p a -> Either1 p q (L a)
- R1 :: q a -> Either1 p q (R a)
-
-type (+^) = Either1
-infixl 6 +^
-
-type Either2 :: forall i j. Type2 i -> Type2 j -> Type2 (i + j)
-data Either2 p q a b where
- L2 :: p a b -> Either2 p q (L a) (L b)
- R2 :: q a b -> Either2 p q (R a) (R b)
-
-type (+^^) = Either2
-infixl 6 +^^
+-- type (+^^) = Either2
+-- infixl 6 +^^
--------------------------------------------------------------------------------
@@ -63,8 +41,8 @@ type Cat i = i -> i -> Type
type Category :: forall i. Cat i -> Constraint
class Category (p :: Cat i) where
- type Ob p :: i -> Constraint
- type Ob p = Always
+ type Ob p :: Constraint1 i
+ type Ob p = Always1
identity :: (Ob p a) => p a a
compose :: p b c -> p a b -> p a c
@@ -85,66 +63,42 @@ instance Category Hask where
-- instance (Ob p i, Ob q j) => ProdOb p q '(i, j) where
-- prodOb = Pair1 Evidence1 Evidence1
-instance (Category p, Category q) => Category (p ×^^ q) where
- -- type Ob (p ×^^ q) = ProdOb p q
- type Ob (p ×^^ q) = HasPairEvidence1 (Ob p) (Ob q)
- identity @a = case pairEvidence @_ @_ @(Ob p) @(Ob q) @a of
- Pair1 Evidence1 Evidence1 -> Pair2 identity identity
- compose (Pair2 f0 f1) (Pair2 g0 g1) = Pair2 (compose f0 g0) (compose f1 g1)
+-- instance (Category p, Category q) => Category (p ×^^ q) where
+-- -- type Ob (p ×^^ q) = ProdOb p q
+-- type Ob (p ×^^ q) = HasPairEvidence1 (Ob p) (Ob q)
+-- identity @a = case pairEvidence @_ @_ @(Ob p) @(Ob q) @a of
+-- Pair1 Evidence1 Evidence1 -> Pair2 identity identity
+-- compose (Pair2 f0 f1) (Pair2 g0 g1) = Pair2 (compose f0 g0) (compose f1 g1)
--------------------------------------------------------------------------------
-type SumOb :: Cat i -> Cat j -> i + j -> Constraint
-class SumOb p q a where
- sumOb :: EitherEvidence1 (Ob p) (Ob q) a
-instance (Category p, Ob p a) => SumOb p q (L a) where
- sumOb = L1 Evidence1
-instance (Category q, Ob q a) => SumOb p q (R a) where
- sumOb = R1 Evidence1
-
-instance (Category p, Category q) => Category (p +^^ q) where
- type Ob (p +^^ q) = SumOb p q
- identity @a = case sumOb @_ @_ @p @q @a of
- L1 Evidence1 -> L2 identity
- R1 Evidence1 -> R2 identity
- compose (L2 f) (L2 g) = L2 (compose f g)
- compose (R2 f) (R2 g) = R2 (compose f g)
+-- type SumOb :: Cat i -> Cat j -> i + j -> Constraint
+-- class SumOb p q a where
+-- sumOb :: EitherEvidence1 (Ob p) (Ob q) a
+-- instance (Category p, Ob p a) => SumOb p q (L a) where
+-- sumOb = L1 Evidence1
+-- instance (Category q, Ob q a) => SumOb p q (R a) where
+-- sumOb = R1 Evidence1
+
+-- instance (Category p, Category q) => Category (p +^^ q) where
+-- type Ob (p +^^ q) = SumOb p q
+-- identity @a = case sumOb @_ @_ @p @q @a of
+-- L1 Evidence1 -> L2 identity
+-- R1 Evidence1 -> R2 identity
+-- compose (L2 f) (L2 g) = L2 (compose f g)
+-- compose (R2 f) (R2 g) = R2 (compose f g)
--------------------------------------------------------------------------------
-type Always :: forall i. i -> Constraint
-class Always i
-instance Always i
-
-type Evidence :: Constraint -> Type
-data Evidence a = (a) => Evidence
-
-type Evidence1 :: forall i. Constraint1 i -> Type1 i
-data Evidence1 p a = (p a) => Evidence1
-
-type PairEvidence1 :: forall i j. Constraint1 i -> Constraint1 j -> Type1 (i × j)
-type PairEvidence1 p q = Pair1 (Evidence1 p) (Evidence1 q)
-
-type HasPairEvidence1 :: forall i j. Constraint1 i -> Constraint1 j -> Constraint1 (i × j)
-class HasPairEvidence1 p q a where
- pairEvidence :: PairEvidence1 p q a
-
--- TODO: pattern
-
-type EitherEvidence1 :: forall i j. Constraint1 i -> Constraint1 j -> Type1 (i + j)
-type EitherEvidence1 p q = Either1 (Evidence1 p) (Evidence1 q)
-
-type Entailment :: Constraint -> Constraint -> Type
-newtype Entailment a b = Entailment ((a) => Evidence b)
-
-type (:-) = Entailment
-infixr 9 :-
+-- type PairEvidence1 :: forall i j. Constraint1 i -> Constraint1 j -> Type1 (i × j)
+-- type PairEvidence1 p q = Pair1 (Evidence1 p) (Evidence1 q)
-always :: a :- Always b
-always = Entailment Evidence
+-- type HasPairEvidence1 :: forall i j. Constraint1 i -> Constraint1 j -> Constraint1 (i × j)
+-- class HasPairEvidence1 p q a where
+-- pairEvidence :: PairEvidence1 p q a
-(\\) :: (a) => ((b) => c) -> (a :- b) -> c
-c \\ Entailment Evidence = c
+-- type EitherEvidence1 :: forall i j. Constraint1 i -> Constraint1 j -> Type1 (i + j)
+-- type EitherEvidence1 p q = Either1 (Evidence1 p) (Evidence1 q)
--------------------------------------------------------------------------------
@@ -157,7 +111,7 @@ instance (Functor f, Dom f ~ p, Cod f ~ q) => NtOb p q f
instance (Category p, Category q) => Category (Nt p q) where
type Ob (Nt p q) = NtOb p q
- identity @f = Nt \ @a -> identity \\ (preserveOb :: Ob p a :- Ob q (f a))
+ identity @f = Nt \ @a -> identity `because` (preserveOb :: Ob p a :- Ob q (f a))
compose (Nt a) (Nt b) = Nt (compose a b)
--------------------------------------------------------------------------------
@@ -174,8 +128,8 @@ class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
type Cod f = DefaultCat
preserveOb :: Ob (Dom f) a :- Ob (Cod f) (f a)
- default preserveOb :: (Ob (Cod f) ~ Always) => Ob (Dom f) a :- Ob (Cod f) (f a)
- preserveOb = always
+ default preserveOb :: (Ob (Cod f) ~ Always1) => Ob (Dom f) a :- Ob (Cod f) (f a)
+ preserveOb = always1
map :: Dom f a b -> Cod f (f a) (f b)
@@ -188,10 +142,10 @@ instance Functor (Either b) where
--------------------------------------------------------------------------------
-type Bifunctor :: forall i j k. (i -> j -> k) -> Constraint
-class (Category (Bildom f), Category (Birdom f), Category (Bicod f)) => Bifunctor (f :: i -> j -> k) where
- type Bildom f :: Cat i
- type Birdom f :: Cat j
- type Bicod f :: Cat k
+-- type Bifunctor :: forall i j k. (i -> j -> k) -> Constraint
+-- class (Category (Bildom f), Category (Birdom f), Category (Bicod f)) => Bifunctor (f :: i -> j -> k) where
+-- type Bildom f :: Cat i
+-- type Birdom f :: Cat j
+-- type Bicod f :: Cat k
-- lmap :: Bildom f a b ->
diff --git a/src/Lude/Constraint.hs b/src/Lude/Constraint.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module Lude.Constraint (
+ Evidence (..),
+ Evidence1 (..),
+ --
+ Entailment (..),
+ (:-),
+ because,
+ --
+ Always,
+ always,
+ --
+ Always1,
+ always1,
+ --
+ Never (..),
+ never,
+ --
+ Never1 (..),
+ never1,
+) where
+
+import Lude.Kind
+import Lude.Proxy
+
+--------------------------------------------------------------------------------
+
+type Evidence :: Constraint -> Type
+data Evidence a = (a) => Evidence
+
+-- TODO: Delete?
+type Evidence1 :: forall i. Constraint1 i -> Type1 i
+data Evidence1 p a = (p a) => Evidence1
+
+--------------------------------------------------------------------------------
+
+type Entailment :: Constraint -> Constraint -> Type
+newtype Entailment a b = Entailment ((a) => Evidence b)
+
+type (:-) = Entailment
+infixr 9 :-
+
+because :: (a) => ((b) => c) -> (a :- b) -> c
+c `because` Entailment Evidence = c
+
+--------------------------------------------------------------------------------
+
+type Always :: Constraint
+class Always
+instance Always
+
+always :: a :- Always
+always = Entailment Evidence
+
+--------------------------------------------------------------------------------
+
+type Always1 :: forall i. Constraint1 i
+class Always1 a
+instance Always1 a
+
+always1 :: a :- Always1 b
+always1 = Entailment Evidence
+
+--------------------------------------------------------------------------------
+
+type Never :: Constraint
+class Never where contradiction :: b
+
+never :: Never :- b
+never = Entailment contradiction
+
+--------------------------------------------------------------------------------
+
+type Never1 :: forall i. Constraint1 i
+class Never1 a where contradiction1 :: Proxy a -> b
+
+never1 :: forall a b. Never1 a :- b
+never1 @a = Entailment (contradiction1 (Proxy :: Proxy a))
diff --git a/src/Lude/Either.hs b/src/Lude/Either.hs
@@ -1,9 +1,12 @@
module Lude.Either (
Either (..),
type (+),
+ --
+ Either1 (..),
+ type (+^),
) where
-import Data.Kind
+import Lude.Kind
-- TODO: It's probably not worth defining our own type here.
@@ -14,3 +17,13 @@ data Either a b = L a | R b
type (+) = Either
infixl 6 +
+
+--------------------------------------------------------------------------------
+
+type Either1 :: forall i j. Type1 i -> Type1 j -> Type1 (i + j)
+data Either1 f g a where
+ L1 :: f a -> Either1 f g (L a)
+ R1 :: g a -> Either1 f g (R a)
+
+type (+^) = Either1
+infixl 6 +^
diff --git a/src/Lude/Kind.hs b/src/Lude/Kind.hs
@@ -4,12 +4,17 @@ module Lude.Kind (
(:~~:) (..),
type (~),
type (~~),
+ --
Type,
TypeL,
TypeU,
+ Type1,
+ --
Constraint,
ConstraintL,
ConstraintU,
+ Constraint1,
+ --
Lev,
) where
@@ -31,6 +36,9 @@ type Type @r = GHC.TYPE r
type TypeL = Type @Repr.BoxL
type TypeU = Type @Repr.BoxU
+type Type1 :: forall (r :: Repr). Kind -> Kind
+type Type1 @r i = i -> Type @r
+
--------------------------------------------------------------------------------
type Constraint :: forall (r :: Repr). Kind
@@ -39,6 +47,9 @@ type Constraint @r = GHC.CONSTRAINT r
type ConstraintL = Constraint @Repr.BoxL
type ConstraintU = Constraint @Repr.BoxU
+type Constraint1 :: forall (r :: Repr). Kind -> Kind
+type Constraint1 @r i = i -> Constraint @r
+
--------------------------------------------------------------------------------
-- | Used to declare unlifted values at the top-level. For example, for any @r@,
diff --git a/src/Lude/Pair.hs b/src/Lude/Pair.hs
@@ -2,24 +2,56 @@ module Lude.Pair (
Pair,
pattern Pair,
type (×),
+ fst,
+ snd,
+ --
+ Pair1 (..),
+ type (×^),
+ fst1,
+ snd1,
+ --
Fst,
Snd,
) where
-import Data.Kind
+import Lude.Kind
+
+-- TODO: Generalize fst and snd (and fst1 and snd1?) with Cartesian class
--------------------------------------------------------------------------------
type Pair :: Type -> Type -> Type
type Pair = (,)
--- For consistency with Either
+-- For consistency
pattern Pair :: a -> b -> Pair a b
pattern Pair a b = (a, b)
+{-# COMPLETE Pair #-}
type (×) = Pair
infixl 7 ×
+fst :: Pair a b -> a
+fst (Pair x _) = x
+
+snd :: Pair a b -> b
+snd (Pair _ y) = y
+
+--------------------------------------------------------------------------------
+
+type Pair1 :: forall i j. Type1 i -> Type1 j -> Type1 (i × j)
+data Pair1 f g a where
+ Pair1 :: f a0 -> g a1 -> Pair1 f g '(a0, a1)
+
+type (×^) = Pair1
+infixl 7 ×^
+
+fst1 :: Pair1 p q '(i, j) -> p i
+fst1 (Pair1 x _) = x
+
+snd1 :: Pair1 p q '(i, j) -> q j
+snd1 (Pair1 _ y) = y
+
--------------------------------------------------------------------------------
type family Fst (x :: i × j) :: i where
diff --git a/src/Lude/Proxy.hs b/src/Lude/Proxy.hs
@@ -0,0 +1,5 @@
+module Lude.Proxy (
+ Proxy (..),
+) where
+
+import Data.Proxy
