commit d81444ca049f02f7c0ae74eb4d0d849709ab01df
parent 65434a8b929548b0f5cf317d9cc89ed47efa6e5f
Author: Robert Russell <robert@rr3.xyz>
Date: Thu, 10 Sep 2026 11:24:00 -0700
Reorganize
Diffstat:
9 files changed, 114 insertions(+), 704 deletions(-)
diff --git a/src/Lude.hs b/Todo/Lude.hs
diff --git a/src/Lude.hs b/src/Lude.hs
@@ -1,623 +1,12 @@
module Lude (
--- Types,
--- Constraint,
--- Levity (..),
--- RuntimeRep (..),
--- Thunked,
--- LRep,
--- URep,
--- Type,
--- BoxedType,
--- LType,
--- UType,
--- Kind,
--- Unlift (..),
--- Function
--- const,
--- fix,
--- flip,
--- ($),
--- ($!),
--- (&),
--- (&!),
--- Bool
--- IsBool (..),
--- Bool (..),
--- (&&),
--- (||),
--- not,
--- Category
--- Category (identity, compose),
--- (<.),
--- (.>),
--- Functor
-{-
-Functor,
-void,
-Compose (Compose, getCompose),
-Const (Const, getConst),
-Identity (Identity, runIdentity),
-map,
-($^),
-for,
-(^&),
-flap,
-(^$),
-flor,
-(&^),
-(<<^),
-(^>>),
-(^<<),
-(>>^),
--- Applicative
-Applicative (pure),
-pass,
-ap,
-(^$^),
-plug,
-(^&^),
-(^<<^),
-(^>>^),
--- Monad
-Monad,
-map',
-($!^),
-for',
-(^&!),
-flap',
-(^$!),
-flor',
-(&!^),
-ap',
-(^$!^),
-plug',
-(^&!^),
--}
-
+ module X,
) where
-{-
-
--- import Control.Applicative (Alternative (empty, (<|>)), Applicative (liftA2, pure, (<*>)), (<**>))
--- import Control.Monad (Monad ((>>=)))
--- import Data.Bool (Bool (..), not, (&&), (||))
--- import Data.Foldable (Foldable)
--- import Data.Function (const, fix, flip)
--- import Data.Functor (Functor (fmap), void)
--- import Data.Functor.Compose (Compose (Compose, getCompose))
--- import Data.Functor.Const (Const (Const, getConst))
--- import Data.Functor.Identity (Identity (Identity, runIdentity))
--- import Data.Maybe (Maybe (..))
--- import Data.Traversable (Traversable (sequenceA))
-
--- TODO: SIMD: VecCount (..) and VecElem (..)
-import GHC.Exts (Constraint, Levity (..), RuntimeRep (..))
-import GHC.Exts qualified as GHC
-
---------------------------------------------------------------------------------
--- Types
-
--- | Types with an unlifted alternative.
---
--- Laws:
--- - @force (lift x) = x@
-class Unlift a where
- type U a :: UType
- force :: a -> U a
- lift :: U a -> a
-
---------------------------------------------------------------------------------
-
-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
-
--- type SemiApplicative :: forall r s. (Type r -> Type s) -> Constraint
--- class (Functor f) => SemiApplicative @r f where
--- map2 :: forall (a :: Type r) (b :: Type r) (c :: Type r). (a -> b -> c) -> f a -> f b -> f c
-
--- type Applicative :: forall r s. (Type r -> Type s) -> Constraint
--- class (SemiApplicative f) => Applicative @r f where
--- pure :: forall (a :: Type r). a -> f a
-
--- type SemiMonad :: forall r s. (Type r -> Type s) -> Constraint
--- class (SemiApplicative f) => SemiMonad @r f where
--- bind :: forall (a :: Type r) (b :: Type r). (a -> f b) -> f a -> f b
-
--- type Monad :: forall r s. (Type r -> Type s) -> Constraint
--- class (Applicative f, SemiMonad f) => Monad @r f
-
--- type SemiComonad :: forall r s.
-
---------------------------------------------------------------------------------
--- Function
-
--- Note how the associativities and (relative) precedences differ with the
--- infix operators in Data.Function.
--- infixl 0 &, &!
--- infixl 1 $, $!
-
--- | Function application.
--- ($) :: (a -> b) -> a -> b
--- f $ x = f x
-
--- | Strict function application.
--- ($!) :: (a -> b) -> a -> b
--- f $! !x = f x
-
--- Flipped function application, or "pipe".
--- (&) :: a -> (a -> b) -> b
--- x & f = f x
-
--- Strict flipped function application, or "pipe".
--- (&!) :: a -> (a -> b) -> b
--- !x &! f = f x
-
---------------------------------------------------------------------------------
--- Bool
-
--- class IsBool (bool :: Type r) where
--- true :: (Thunked) => bool
--- false :: (Thunked) => bool
--- bool :: a -> a -> bool -> a
-
--- instance IsBool Bool where
--- true = True
--- false = False
--- bool t f = \case
--- True -> t
--- False -> f
-
--- data UBool :: UType where
--- UTrue :: UBool
--- UFalse :: UBool
-
--- instance IsBool UBool where
--- true = UTrue
--- false = UFalse
--- bool t f = \case
--- UTrue -> t
--- UFalse -> f
-
--- instance Unlift Bool where
--- type U Bool = UBool
-
--- force True = UTrue
--- force False = UFalse
-
--- lift UTrue = True
--- lift UFalse = False
-
---------------------------------------------------------------------------------
--- Maybe
-
--- class IsMaybe (maybe :: Type s -> Type r) where
--- just :: a -> maybe a
--- nothing :: (Thunked) => maybe a
--- maybe :: b -> (a -> b) -> maybe a -> b
-
--- instance IsMaybe Maybe where
--- just = Just
--- nothing = Nothing
--- maybe n j = \case
--- Just a -> j a
--- Nothing -> n
-
--- data UMaybe :: LType -> UType where
--- UJust :: a -> UMaybe a
--- UNothing :: UMaybe a
-
--- instance IsMaybe UMaybe where
--- just = UJust
--- nothing = UNothing
--- maybe n j = \case
--- UJust a -> j a
--- UNothing -> n
-
--- instance Unlift (Maybe a) where
--- type U (Maybe a) = UMaybe a
-
--- force (Just a) = UJust a
--- force Nothing = UNothing
-
--- lift (UJust a) = Just a
--- lift UNothing = Nothing
-
--- data Maybe' :: UType -> LType where
--- Just' :: a -> Maybe' a
--- Nothing' :: Maybe' a
-
--- instance IsMaybe Maybe' where
--- just = Just'
--- nothing = Nothing'
--- maybe n j = \case
--- Just' a -> j a
--- Nothing' -> n
-
--- data UMaybe' :: UType -> UType where
--- UJust' :: a -> UMaybe' a
--- UNothing' :: UMaybe' a
-
--- instance IsMaybe UMaybe' where
--- just = UJust'
--- nothing = UNothing'
--- maybe n j = \case
--- UJust' a -> j a
--- UNothing' -> n
-
--- instance Unlift (Maybe' a) where
--- type U (Maybe' a) = UMaybe' a
-
--- force (Just' a) = UJust' a
--- force Nothing' = UNothing'
-
--- lift (UJust' a) = Just' a
--- lift UNothing' = Nothing'
-
--- isJust :: forall s r (maybe :: Type s -> Type r) a. (IsMaybe maybe) => maybe a -> Bool
--- isJust = maybe False (const True)
-
--- isNothing :: (IsMaybe maybe) => maybe a -> Bool
--- isNothing = maybe True (const False)
-
--- type family Maybe# (r :: RuntimeRep) (l :: Levity) :: Type r -> BoxedType l
--- type instance Maybe# LRep Lifted = Maybe
--- type instance Maybe# URep Lifted = Maybe'
--- type instance Maybe# LRep Unlifted = UMaybe
--- type instance Maybe# URep Unlifted = UMaybe'
-
--- type family Lower (a :: Kind) :: Kind where
--- Lower (BoxedType l) = TypeU
--- Lower (k -> l) = k -> Lower l
--- type family X (a :: k) :: Lower k
--- type instance X (MaybeL @l) = MaybeL @Unlifted
-
---------------------------------------------------------------------------------
--- Numeric types
-
--- TODO
-
---------------------------------------------------------------------------------
--- Category
-
--- infixr 9 ∘
-
--- infixr 2 <.
--- infixl 2 .>
-
--- (⊲⊳)
--- (⋖⋗)
--- (⩹⩺)
--- (⨟)
--- (⦂)
--- (⋄)
--- (∧∨)
--- (⩓⩔)
--- (∩∪)
--- (=≠≡≢≈≉)
--- (<>≤≥≮≯≰≱)
--- (≺≻≼≽⊀⊁⋠⋡)
--- (⊂⊃⊆⊇⊄⊅⊈⊉)
--- (⊏⊐⊑⊒)
--- (⊢⊣⊤⊥)
--- y = h ∘ g ∘ f ∙^ x
--- (f ⦾ g ⦿ x)
--- y = h ◁ g ◁ f ◀ x
--- y = x ▶ f ▷ g ▷ h
--- (⧑⧒⧓⧔⧕⧖⧗⋈⋉⋊)
--- (↑↓↔↕↖↗↘↙)
--- (⥼⥽⥾⥿)
--- (⊰⊱)
--- (⭘∘)
--- (⦁∙⋅)
--- (⊙)
--- (⊚)
--- (⬬⬭⬮⬯)
--- (⬝⬞)
--- (⋆)
--- (⬥⬦⬧⬨⬩⬪⬫)
--- (◖◗)
--- (◐◑)
--- (⫾)
--- (■▪▬▮▰▲▶▼◀◆)
--- (∙⋆⋄*≀⌑▫)
--- y = x ▪ f ▫ g ▫ h
--- y = x ⦂ f ⨟ g ⨟ h
-
--- TODO: Op, Products, Sums, Clown, Joker
-
-{-
-
-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
- unitr :: Iso (Hask ρ) (f a (UnitOf f)) a
- assoc :: Iso (Hask ρ) (f (f a b) c) (f a (f b c))
-
--- TODO: Having this only work for Hask sucks and is needlessly specialized.
--- We can generalize this and some above definitions to any category whose
--- objects have kind Type ρ, which isn't just Hask (e.g., Kleisli).
-class (Monoidal f) => Cartesian (f :: Type ρ -> Type ρ -> Type ρ) where
- fst :: forall (a :: Type ρ) (b :: Type ρ). f a b -> a
- snd :: forall (a :: Type ρ) (b :: Type ρ). f a b -> b
-
- pair :: forall (a :: Type ρ) (b :: Type ρ) (c :: Type ρ). (a -> b) -> (a -> c) -> a -> f b c
- pair f g = bimap f g ∘ diag
-
- diag :: forall (a :: Type ρ). a -> f a a
- diag = pair identity identity
-
--}
-
--- | Right-to-left composition.
---
--- This operator is right associative to exploit laziness in the case where
--- the outer function doesn't need its argument:
---
--- > (const x <. (f <. g)) y ---> const x ((f <. g) y) ---> x
---
--- Note that @f <. g@ is never evaluated.
--- (<.) :: (Category v) => v b c -> v a b -> v a c
--- (<.) = (.)
-
--- | Left-to-right composition.
---
--- This operator is left associative to exploit laziness in the case where
--- the outer function doesn't need its argument:
---
--- > ((g .> f) .> const x) y ---> const x ((g .> f) y) ---> x
---
--- Note that @g .> f@ is never evaluated.
--- (.>) :: (Category v) => v a b -> v b c -> v a c
--- (.>) = flip (.)
-
--- TODO: (.:), (<.:), (.:>)
-
---------------------------------------------------------------------------------
--- Functor
-
-{-
-infixl 0 ^&, &^, ~^&, ^&~, ~&^, &^~
-infixl 1 $^, ^$, $^~, ~$^, ^$~, ~^$
-infixr 2 <<^, ^>>, ^<<, >>^
-
--- | The action of a functor on a function.
-map, ($^) :: (Functor f) => (a -> b) -> f a -> f b
-map = fmap
-($^) = map
-
--- | The action of a functor on a function, flipped.
---
--- With the BlockArguments extension, expressions like "@for xs \\x -> ...@"
--- look like for-loops, hence the name "for".
-for, (^&) :: (Functor f) => f a -> (a -> b) -> f b
-for = flip map
-(^&) = for
-
--- | Application of a function in a functor to a pure value.
-flap, (^$) :: (Functor f) => f (a -> b) -> a -> f b
-flap f a = f ^& ($ a)
-(^$) = flap
-
--- | Flipped application of a function in a functor to a pure value.
-flor, (&^) :: (Functor f) => a -> f (a -> b) -> f b
-flor = flip flap
-(&^) = flor
-
-($^~) :: (Functor f, Functor g) => (a -> b) -> g (f a) -> g (f b)
-f $^~ a = (f $^) $^ a
-
-(~^&) :: (Functor f, Functor g) => g (f a) -> (a -> b) -> g (f b)
-(~^&) = flip ($^~)
-
-(~$^) :: (Functor f, Functor g) => g (a -> b) -> f a -> g (f b)
-f ~$^ a = f ^& ($^ a)
-
-(^&~) :: (Functor f, Functor g) => f a -> g (a -> b) -> g (f b)
-(^&~) = flip (~$^)
-
-(^$~) :: (Functor f, Functor g) => f (a -> b) -> g a -> g (f b)
-f ^$~ a = (f ^$) $^ a
-
-(~&^) :: (Functor f, Functor g) => g a -> f (a -> b) -> g (f b)
-(~&^) = flip (^$~)
-
-(~^$) :: (Functor f, Functor g) => g (f (a -> b)) -> a -> g (f b)
-f ~^$ a = f ^& (^$ a)
-
-(&^~) :: (Functor f, Functor g) => a -> g (f (a -> b)) -> g (f b)
-(&^~) = flip (~^$)
-
--- TODO
-
--- | Right-to-left composition with the first function in a functor.
-(<<^) :: (Functor f, Category v) => v b c -> f (v a b) -> f (v a c)
-g <<^ f = (g <.) $^ f
-
--- TODO
-
--- | Left-to-right composition with the first function in a functor.
-(^>>) :: (Functor f, Category v) => f (v a b) -> v b c -> f (v a c)
-f ^>> g = f ^& (.> g)
-
--- TODO
-
--- | Right-to-left composition with the second function in a functor.
-(^<<) :: (Functor f, Category v) => f (v b c) -> v a b -> f (v a c)
-g ^<< f = g ^& (<. f)
-
--- TODO
-
--- | Left-to-right composition with the second function in a functor.
-(>>^) :: (Functor f, Category v) => v a b -> f (v b c) -> f (v a c)
-f >>^ g = (f .>) $^ g
-
--- TODO: *^, ^*
-
---------------------------------------------------------------------------------
--- Applicative
-
-infixl 0 ^&^, ~^&^~
-infixl 1 ^$^, ~^$^~
-infixr 2 ^<<^, ^>>^
-
--- | Functions with applicative effects.
-newtype Appy f a b = Appy {runAppy :: f (a -> b)}
-
-instance (Functor f) => Functor (Appy f a) where
- fmap f (Appy a) = Appy (f $^~ a)
-
-instance (Applicative f) => Applicative (Appy f a) where
- pure = Appy . pure . const
- Appy f <*> Appy a = Appy (f ~^$^~ a)
-
-hom :: (a -> b) -> (b -> b -> c) -> a -> a -> c
-hom f g x y = g (f x) (f y)
-
-instance (Alternative f) => Alternative (Appy f a) where
- empty = Appy empty
-
--- Appy x <|> Appy y = Appy (x <|> y)
--- (<|>) = hom runAppy (<|>)
-
-instance (Applicative f) => Category (Appy f) where
- id = Appy (pure id)
- Appy f . Appy g = Appy ((.) $^ f ^$^ g)
-
--- TODO: Remove ap and plug?
--- TODO: liftA{,1,2,3,4}
-
--- | An alias for @pure ()@.
-pass :: (Applicative f) => f ()
-pass = pure ()
-
--- | Application in an applicative functor.
-ap, (^$^) :: (Applicative f) => f (a -> b) -> f a -> f b
-ap = (<*>)
-(^$^) = ap
-
--- | Flipped application in an applicative functor (with effects resolved as
--- they appear, left-to-right).
-plug, (^&^) :: (Applicative f) => f a -> f (a -> b) -> f b
-plug = (<**>)
-(^&^) = plug
-
-(~^$^~) :: (Applicative f, Applicative g) => g (f (a -> b)) -> g (f a) -> g (f b)
-f ~^$^~ a = (^$^) $^ f ^$^ a
-
-(~^&^~) :: (Applicative f, Applicative g) => g (f a) -> g (f (a -> b)) -> g (f b)
-f ~^&^~ a = (^&^) $^ f ^$^ a
-
--- TODO: document
-(^<<^) :: (Applicative f, Category v) => f (v b c) -> f (v a b) -> f (v a c)
-(^<<^) = liftA2 (<.)
-
--- TODO: document
-(^>>^) :: (Applicative f, Category v) => f (v a b) -> f (v b c) -> f (v a c)
-(^>>^) = liftA2 (.>)
-
--- TODO: "semicolons"
-
---------------------------------------------------------------------------------
--- Monad
-
-infixl 0 ^&!, &!^, ^&!^
-infixl 1 $!^, ^$!, ^$!^
-
-map', ($!^) :: (Monad m) => (a -> b) -> m a -> m b
-map' f mx = mx >>= \x -> pure $! f x
-($!^) = map'
-
-for', (^&!) :: (Monad m) => m a -> (a -> b) -> m b
-for' = flip map'
-(^&!) = for
-
-flap', (^$!) :: (Monad m) => m (a -> b) -> a -> m b
-flap' mf x = mf >>= \f -> pure $! f x
-(^$!) = flap'
-
-flor', (&!^) :: (Monad m) => a -> m (a -> b) -> m b
-flor' = flip flap'
-(&!^) = flor'
-
-ap', (^$!^) :: (Monad m) => m (a -> b) -> m a -> m b
-ap' mf mx = do
- f <- mf
- x <- mx
- pure $! f x
-(^$!^) = ap'
-
-plug', (^&!^) :: (Monad m) => m a -> m (a -> b) -> m b
-plug' mx mf = do
- x <- mx
- f <- mf
- pure $! f x
-(^&!^) = plug'
--}
-
--- (.) :: (b0 -> c) -> (a0 -> b0) -> (a0 -> c)
--- (g . f) a0 = g (f a0)
--- (^.) :: (b0 -> b1 -> c) -> (a0 -> b1) -> (b0 -> a0 -> c)
--- (g ^. f) b0 a0 = g b0 (f a0)
--- (^^.) :: (b0 -> b1 -> b2 -> c) -> (a0 -> b2) -> (b0 -> b1 -> a0 -> c)
--- (g ^^. f) b0 b1 a0 = g b0 b1 (f a0)
--- (^^^.) :: (b0 -> b1 -> b2 -> b3 -> c) -> (a0 -> b3) -> (b0 -> b1 -> b2 -> a0 -> c)
--- (g ^^^. f) b0 b1 b2 a0 = g b0 b1 b2 (f a0)
--- (.^) :: (b0 -> c) -> (a0 -> a1 -> b0) -> (a0 -> a1 -> c)
--- (g .^ f) a0 a1 = g (f a0 a1)
--- (^.^) :: (b0 -> b1 -> c) -> (a0 -> a1 -> b1) -> (b0 -> a0 -> a1 -> c)
--- (g ^.^ f) b0 a0 a1 = g b0 (f a0 a1)
--- (^^.^) :: (b0 -> b1 -> b2 -> c) -> (a0 -> a1 -> b2) -> (b0 -> b1 -> a0 -> a1 -> c)
--- (g ^^.^ f) b0 b1 a0 a1 = g b0 b1 (f a0 a1)
--- (^^^.^) :: (b0 -> b1 -> b2 -> b3 -> c) -> (a0 -> a1 -> b3) -> (b0 -> b1 -> b2 -> a0 -> a1 -> c)
--- (g ^^^.^ f) b0 b1 b2 a0 a1 = g b0 b1 b2 (f a0 a1)
--- (.^^) :: (b0 -> c) -> (a0 -> a1 -> a2 -> b0) -> (a0 -> a1 -> a2 -> c)
--- (^.^^) :: (b0 -> b1 -> c) -> (a0 -> a1 -> a2 -> b1) -> (b0 -> a0 -> a1 -> a2 -> c)
--- (^^.^^) :: (b0 -> b1 -> b2 -> c) -> (a0 -> a1 -> a2 -> b2) -> (b0 -> b1 -> a0 -> a1 -> a2 -> c)
--- (^^^.^^) :: (b0 -> b1 -> b2 -> b3 -> c) -> (a0 -> a1 -> a2 -> b3) -> (b0 -> b1 -> b2 -> a0 -> a1 -> a2 -> c)
--- (.^^^) :: (b0 -> c) -> (a0 -> a1 -> a2 -> a3 -> b0) -> (a0 -> a1 -> a2 -> a3 -> c)
--- (^.^^^) :: (b0 -> b1 -> c) -> (a0 -> a1 -> a2 -> a3 -> b1) -> (b0 -> a0 -> a1 -> a2 -> a3 -> c)
--- (^^.^^^) :: (b0 -> b1 -> b2 -> c) -> (a0 -> a1 -> a2 -> a3 -> b2) -> (b0 -> b1 -> a0 -> a1 -> a2 -> a3 -> c)
--- (^^^.^^^) :: (b0 -> b1 -> b2 -> b3 -> c) -> (a0 -> a1 -> a2 -> a3 -> b3) -> (b0 -> b1 -> b2 -> a0 -> a1 -> a2 -> a3 -> c)
-
--}
+import Lude.Algebra as X
+import Lude.Bool as X
+import Lude.Constraint as X
+import Lude.Function as X
+import Lude.Haskell as X
+import Lude.List as X
+import Lude.Unit as X
+import Lude.Void as X
diff --git a/src/Lude/Algebra.hs b/src/Lude/Algebra.hs
@@ -0,0 +1,5 @@
+module Lude.Algebra (
+ module X,
+) where
+
+import Lude.Algebra.Category as X
diff --git a/src/Lude/Algebra/Algebra.hs b/src/Lude/Algebra/Algebra.hs
@@ -1,80 +0,0 @@
-module Lude.Algebra.Algebra (
- Algebra,
- Algebraic,
- --
- DefaultRecursive (..),
- Recursive (..),
- --
- Coalgebra,
- Coalgebraic,
- --
- DefaultCorecursive (..),
- Corecursive (..),
-) where
-
-import Lude.Algebra.Category
-import Lude.Haskell
-
--- TODO: Check whether we really need a separate default instance for Nt.
--- I think it's necessary, because composition with `map h` forces eager
--- evaluation of h.
-
--- TODO: Add Coalgebraic (Algebraic) as a super class of Recursive (Corecursive).
-
---------------------------------------------------------------------------------
-
--- | An algebra for an endofunctor.
-type Algebra :: forall {k}. Cat k -> Endo k -> k -> Type
-type Algebra p f a = f a `p` a
-
--- | A type equipped with an algebra for an endofunctor.
-type Algebraic :: forall {k}. Cat k -> Endo k -> k -> Constraint
-class (EndofunctorialOn p f) => Algebraic p f a | a -> f where
- wrap :: Algebra p f a
-
---------------------------------------------------------------------------------
-
-type DefaultRecursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
-class DefaultRecursive p f r where
- defaultCata :: (Algebraic p f r) => forall a. Algebra p f a -> r `p` a
-
-instance (Coalgebraic Function f r) => DefaultRecursive Function f r where
- defaultCata f = h where h = f . map h . peel
-instance (Categorical p, Categorical q, Coalgebraic (p ==> q) f r) => DefaultRecursive (NT p q) f r where
- defaultCata f@(Natural _) = h where h = Natural (comp f . comp (map h) . comp peel) \\ witnessMor (wrap @(p ==> q) @f @r)
-
--- | A type equipped with an initial algebra for an endofunctor.
-type Recursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
-class (Algebraic p f r) => Recursive p f r where
- cata :: forall a. Algebra p f a -> r `p` a
- default cata :: (DefaultRecursive p f r) => forall a. Algebra p f a -> r `p` a
- cata = defaultCata
-
---------------------------------------------------------------------------------
-
--- | A coalgebra for an endofunctor.
-type Coalgebra :: forall {k}. Cat k -> Endo k -> k -> Type
-type Coalgebra p g b = b `p` g b
-
--- | A type equipped with a coalgebra for an endofunctor.
-type Coalgebraic :: forall {k}. Cat k -> Endo k -> k -> Constraint
-class (EndofunctorialOn p g) => Coalgebraic p g b | b -> g where
- peel :: Coalgebra p g b
-
---------------------------------------------------------------------------------
-
-type DefaultCorecursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
-class DefaultCorecursive p g s where
- defaultAna :: (Coalgebraic p g s) => forall b. Coalgebra p g b -> b `p` s
-
-instance (Algebraic Function g s) => DefaultCorecursive Function g s where
- defaultAna g = h where h = wrap . map h . g
-instance (Categorical p, Categorical q, Algebraic (p ==> q) g s) => DefaultCorecursive (p ==> q) g s where
- defaultAna g@(Natural _) = h where h = Natural (comp wrap . comp (map h) . comp g) \\ witnessMor (peel @(p ==> q) @g @s)
-
--- | A type equipped with a final coalgebra for an endofunctor.
-type Corecursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
-class (Coalgebraic p g s) => Corecursive p g s where
- ana :: forall b. Coalgebra p g b -> b `p` s
- default ana :: (DefaultCorecursive p g s) => forall b. Coalgebra p g b -> b `p` s
- ana = defaultAna
diff --git a/src/Lude/Algebra/Category.hs b/src/Lude/Algebra/Category.hs
@@ -2,6 +2,8 @@ module Lude.Algebra.Category (
module X,
) where
+import Lude.Algebra.Category.Adjunction as X
+import Lude.Algebra.Category.Algebra as X
import Lude.Algebra.Category.Bifunctor as X
import Lude.Algebra.Category.Constrained as X
import Lude.Algebra.Category.Core as X
@@ -16,10 +18,6 @@ import Lude.Algebra.Category.Terminal as X
-- TODO: Free and cofree
--- TODO: Adjunctions and zap
-
--- TODO: Eilenberg-Moore (co)algebras?
-
-- TODO: Profunctors? Other special kinds of functors, given distinct names?
-- That would allow being a functor in multiple ways without losing coherence.
-- E.g., lists could be mappable "normally" and filterable (choose is map).
diff --git a/src/Lude/Algebra/Category/Adjunction.hs b/src/Lude/Algebra/Category/Adjunction.hs
@@ -6,6 +6,8 @@ import Lude.Algebra.Category.Core
import Lude.Algebra.Category.Iso
import Lude.Haskell
+-- TODO: Zappable?
+
--------------------------------------------------------------------------------
type Adjoint :: forall {i} {j}. (i -> j) -> (j -> i) -> Constraint
diff --git a/src/Lude/Algebra/Category/Algebra.hs b/src/Lude/Algebra/Category/Algebra.hs
@@ -0,0 +1,82 @@
+module Lude.Algebra.Category.Algebra (
+ Algebra,
+ Algebraic,
+ --
+ DefaultRecursive (..),
+ Recursive (..),
+ --
+ Coalgebra,
+ Coalgebraic,
+ --
+ DefaultCorecursive (..),
+ Corecursive (..),
+) where
+
+import Lude.Algebra.Category.Core
+import Lude.Haskell
+
+-- TODO: Check whether we really need a separate default instance for Nt.
+-- I think it's necessary, because composition with `map h` forces eager
+-- evaluation of h.
+
+-- TODO: Add Coalgebraic (Algebraic) as a super class of Recursive (Corecursive).
+
+-- TODO: Eilenberg-Moore (co)algebras?
+
+--------------------------------------------------------------------------------
+
+-- | An algebra for an endofunctor.
+type Algebra :: forall {k}. Cat k -> Endo k -> k -> Type
+type Algebra p f a = f a `p` a
+
+-- | A type equipped with an algebra for an endofunctor.
+type Algebraic :: forall {k}. Cat k -> Endo k -> k -> Constraint
+class (EndofunctorialOn p f) => Algebraic p f a | a -> f where
+ wrap :: Algebra p f a
+
+--------------------------------------------------------------------------------
+
+type DefaultRecursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
+class DefaultRecursive p f r where
+ defaultCata :: (Algebraic p f r) => forall a. Algebra p f a -> r `p` a
+
+instance (Coalgebraic Function f r) => DefaultRecursive Function f r where
+ defaultCata f = h where h = f . map h . peel
+instance (Categorical p, Categorical q, Coalgebraic (p ==> q) f r) => DefaultRecursive (NT p q) f r where
+ defaultCata f@(Natural _) = h where h = Natural (comp f . comp (map h) . comp peel) \\ witnessMor (wrap @(p ==> q) @f @r)
+
+-- | A type equipped with an initial algebra for an endofunctor.
+type Recursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
+class (Algebraic p f r) => Recursive p f r where
+ cata :: forall a. Algebra p f a -> r `p` a
+ default cata :: (DefaultRecursive p f r) => forall a. Algebra p f a -> r `p` a
+ cata = defaultCata
+
+--------------------------------------------------------------------------------
+
+-- | A coalgebra for an endofunctor.
+type Coalgebra :: forall {k}. Cat k -> Endo k -> k -> Type
+type Coalgebra p g b = b `p` g b
+
+-- | A type equipped with a coalgebra for an endofunctor.
+type Coalgebraic :: forall {k}. Cat k -> Endo k -> k -> Constraint
+class (EndofunctorialOn p g) => Coalgebraic p g b | b -> g where
+ peel :: Coalgebra p g b
+
+--------------------------------------------------------------------------------
+
+type DefaultCorecursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
+class DefaultCorecursive p g s where
+ defaultAna :: (Coalgebraic p g s) => forall b. Coalgebra p g b -> b `p` s
+
+instance (Algebraic Function g s) => DefaultCorecursive Function g s where
+ defaultAna g = h where h = wrap . map h . g
+instance (Categorical p, Categorical q, Algebraic (p ==> q) g s) => DefaultCorecursive (p ==> q) g s where
+ defaultAna g@(Natural _) = h where h = Natural (comp wrap . comp (map h) . comp g) \\ witnessMor (peel @(p ==> q) @g @s)
+
+-- | A type equipped with a final coalgebra for an endofunctor.
+type Corecursive :: forall {k}. Cat k -> Endo k -> k -> Constraint
+class (Coalgebraic p g s) => Corecursive p g s where
+ ana :: forall b. Coalgebra p g b -> b `p` s
+ default ana :: (DefaultCorecursive p g s) => forall b. Coalgebra p g b -> b `p` s
+ ana = defaultAna
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -130,6 +130,8 @@ instance (FunctorialOn p p f) => EndofunctorialOn p f
type ObjArg :: forall {i} {j}. (i -> j) -> Predicate i
type ObjArg f = Obj (Dom f)
+-- for :: forall {i} {j} (f :: i -> j) (a :: i) (b :: i). (Functorial f) => Dom f i j -> Cod f (f i) (f j)
+
preservesObj :: forall {i} {j} (p :: Cat i) (q :: Cat j). forall (f :: i -> j) -> (FunctorialOn p q f) => forall (a :: i) -> Obj p a :- Obj q (f a)
preservesObj _ _ = preservesObj_
diff --git a/src/Lude/Function.hs b/src/Lude/Function.hs
@@ -0,0 +1,12 @@
+module Lude.Function (
+ flip,
+ const,
+ ($),
+ (&),
+) where
+
+import Data.Function
+
+-- TODO: Generalize some of this? E.g., for CCCs?
+
+--------------------------------------------------------------------------------
