commit 01d1b0101f473d851219a8c8600d111a61df252f
parent dbef37fab440d8243484712e6b4a50829383f3a9
Author: Robert Russell <robert@rr3.xyz>
Date: Mon, 9 Mar 2026 00:10:40 -0700
Add more human slop
Diffstat:
3 files changed, 349 insertions(+), 228 deletions(-)
diff --git a/src/Lude.hs b/src/Lude.hs
@@ -1,123 +1,102 @@
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',
- (^&!^),
- -}
+-- 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',
+(^&!^),
+-}
+
) 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))
+{-
+
+-- 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
-infixl 8 ∙
-type (∙) f a = f a
-
--------------------------------------------------------------------------------
-- Types
--- | An alias for the empty constraint.
---
--- Used to declare unlifted values at the top-level. For example, for any @r@
--- and @A :: Type r@:
--- @
--- a :: Thunked => A
--- a = ...
--- @
-type Thunked = () :: Constraint
-
-type LRep = BoxedRep Lifted
-type URep = BoxedRep Unlifted
-
-type Type = GHC.TYPE
-type BoxedType l = Type (BoxedRep l)
-type LType = BoxedType Lifted
-type UType = BoxedType Unlifted
-
--- | An alias for `LType`.
-type Kind = LType
-
-- | Types with an unlifted alternative.
--
-- Laws:
@@ -128,135 +107,196 @@ class Unlift a where
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 $, $!
+-- infixl 0 &, &!
+-- infixl 1 $, $!
-- | Function application.
-($) :: (a -> b) -> a -> b
-f $ x = f x
+-- ($) :: (a -> b) -> a -> b
+-- f $ x = f x
-- | Strict function application.
-($!) :: (a -> b) -> a -> b
-f $! !x = f x
+-- ($!) :: (a -> b) -> a -> b
+-- f $! !x = f x
-- Flipped function application, or "pipe".
-(&) :: a -> (a -> b) -> b
-x & f = f x
+-- (&) :: a -> (a -> b) -> b
+-- x & f = f x
-- Strict flipped function application, or "pipe".
-(&!) :: a -> (a -> b) -> b
-!x &! f = f x
+-- (&!) :: 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
+-- 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
+-- instance IsBool Bool where
+-- true = True
+-- false = False
+-- bool t f = \case
+-- True -> t
+-- False -> f
-data UBool :: UType where
- UTrue :: UBool
- UFalse :: UBool
+-- 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 IsBool UBool where
+-- true = UTrue
+-- false = UFalse
+-- bool t f = \case
+-- UTrue -> t
+-- UFalse -> f
-instance Unlift Bool where
- type U Bool = UBool
+-- instance Unlift Bool where
+-- type U Bool = UBool
- force True = UTrue
- force False = UFalse
+-- force True = UTrue
+-- force False = UFalse
- lift UTrue = True
- lift UFalse = False
+-- 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
+-- 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
+-- 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
+-- 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 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
+-- instance Unlift (Maybe a) where
+-- type U (Maybe a) = UMaybe a
- force (Just a) = UJust a
- force Nothing = UNothing
+-- force (Just a) = UJust a
+-- force Nothing = UNothing
- lift (UJust a) = Just a
- lift UNothing = Nothing
+-- lift (UJust a) = Just a
+-- lift UNothing = Nothing
-data Maybe' :: UType -> LType where
- Just' :: a -> Maybe' a
- Nothing' :: Maybe' a
+-- 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
+-- 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
+-- 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 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
+-- instance Unlift (Maybe' a) where
+-- type U (Maybe' a) = UMaybe' a
- force (Just' a) = UJust' a
- force Nothing' = UNothing'
+-- force (Just' a) = UJust' a
+-- force Nothing' = UNothing'
- lift (UJust' a) = Just' a
- lift UNothing' = Nothing'
+-- 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)
+-- 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)
+-- 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
@@ -596,3 +636,30 @@ plug' mx mf = do
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)
+
+-}
diff --git a/src/Lude/Algebra.hs b/src/Lude/Algebra.hs
@@ -3,6 +3,7 @@
module Lude.Algebra (
Category (..),
Functor (..),
+ Bifunctor (..),
Hask,
Op (..),
) where
@@ -11,51 +12,91 @@ import Lude.Kind
import Lude.Repr (Repr)
import Lude.Repr qualified as Repr
--- TODO: Defaults for lmap, rmap, bimap
-
--------------------------------------------------------------------------------
+-- Category
type Cat k r = k -> k -> Type r
-type Category :: forall k (r :: Repr). Cat k r -> Constraint
-class Category cat where
- identity :: Lev (cat a a)
- compose :: cat b c -> cat a b -> cat a c
+type Category :: forall k r. Cat k r -> Constraint
+class Category (cat :: Cat k r) where
+ type Ob @k @(r :: Repr) cat (a :: k) :: Constraint
+ type Ob cat a = ()
+ identity :: (Ob cat a) => cat a a
+ compose :: (Ob3 cat a b c) => cat b c -> cat a b -> cat a c
+
+type Ob2 :: forall k r. Cat k r -> k -> k -> Constraint
+type Ob2 cat a b = (Ob cat a, Ob cat b)
+
+type Ob3 :: forall k r. Cat k r -> k -> k -> k -> Constraint
+type Ob3 cat a b c = (Ob2 cat a b, Ob cat c)
-type Functor :: forall k0 k1 (r0 :: Repr) (r1 :: Repr). Cat k0 r0 -> Cat k1 r1 -> (k0 -> k1) -> Constraint
-class (Category cat0, Category cat1) => Functor cat0 cat1 f where
- map :: cat0 a b -> cat1 (f a) (f b)
+type Ob4 :: forall k r. Cat k r -> k -> k -> k -> k -> Constraint
+type Ob4 cat a b c d = (Ob3 cat a b c, Ob cat d)
+
+--------------------------------------------------------------------------------
+-- Functor
-type Endofunctor :: forall k (r :: Repr). Cat k r -> (k -> k) -> Constraint
+type Functor :: forall k0 k1 r0 r1. Cat k0 r0 -> Cat k1 r1 -> (k0 -> k1) -> Constraint
+class (Category cat0, Category cat1) => Functor cat0 cat1 f | cat0 f -> cat1, cat1 f -> cat0 where
+ map :: (Ob2 cat0 a b, Ob2 cat1 (f a) (f b)) => cat0 a b -> cat1 (f a) (f b)
+
+type Endofunctor :: forall k r. Cat k r -> (k -> k) -> Constraint
type Endofunctor cat f = Functor cat cat f
-type LFunctor :: forall k0 k1 k2 (r0 :: Repr) (r2 :: Repr). Cat k0 r0 -> Cat k2 r2 -> (k0 -> k1 -> k2) -> Constraint
-class (Category cat0, Category cat2) => LFunctor cat0 cat2 f where
- lmap :: cat0 a b -> cat2 (f a c) (f b c)
+--------------------------------------------------------------------------------
+-- Bifunctor
+
+type ObLmap :: forall k0 k1 k2 r0 r1 r2. Cat k0 r0 -> Cat k1 r1 -> Cat k2 r2 -> (k0 -> k1 -> k2) -> k0 -> k0 -> k1 -> Constraint
+type ObLmap cat0 cat1 cat2 f a b c = (Ob2 cat0 a b, Ob cat1 c, Ob2 cat2 (f a c) (f b c))
+
+type OpRmap :: forall k0 k1 k2 r0 r1 r2. Cat k0 r0 -> Cat k1 r1 -> Cat k2 r2 -> (k0 -> k1 -> k2) -> k0 -> k1 -> k1 -> Constraint
+type OpRmap cat0 cat1 cat2 f a c d = (Ob cat0 a, Ob2 cat1 c d, Ob2 cat2 (f a c) (f a d))
-type RFunctor :: forall k0 k1 k2 (r1 :: Repr) (r2 :: Repr). Cat k1 r1 -> Cat k2 r2 -> (k0 -> k1 -> k2) -> Constraint
-class (Category cat1, Category cat2) => RFunctor cat1 cat2 f where
- rmap :: cat1 c d -> cat2 (f a c) (f a d)
+type OpBimap :: forall k0 k1 k2 r0 r1 r2. Cat k0 r0 -> Cat k1 r1 -> Cat k2 r2 -> (k0 -> k1 -> k2) -> k0 -> k0 -> k1 -> k1 -> Constraint
+type OpBimap cat0 cat1 cat2 f a b c d = (Ob2 cat0 a b, Ob2 cat1 c d, Ob4 cat2 (f a c) (f a d) (f b c) (f b d))
-type Bifunctor :: forall k0 k1 k2 (r0 :: Repr) (r1 :: Repr) (r2 :: Repr). Cat k0 r0 -> Cat k1 r1 -> Cat k2 r2 -> (k0 -> k1 -> k2) -> Constraint
-class (LFunctor cat0 cat2 f, RFunctor cat1 cat2 f) => Bifunctor cat0 cat1 cat2 f where
- bimap :: cat0 a b -> cat1 c d -> cat2 (f a c) (f b d)
+type BifunctorRep :: Repr -> Repr -> Repr -> Constraint
+class BifunctorRep r0 r1 r2 where
+ lmapD :: forall k0 k1 k2 (cat0 :: Cat k0 r0) (cat1 :: Cat k1 r1) (cat2 :: Cat k2 r2) f a b c. (Bifunctor cat0 cat1 cat2 f, ObLmap cat0 cat1 cat2 f a b c) => cat0 a b -> cat2 (f a c) (f b c)
+ rmapD :: forall k0 k1 k2 (cat0 :: Cat k0 r0) (cat1 :: Cat k1 r1) (cat2 :: Cat k2 r2) f a c d. (Bifunctor cat0 cat1 cat2 f, OpRmap cat0 cat1 cat2 f a c d) => cat1 c d -> cat2 (f a c) (f a d)
+ bimapD :: forall k0 k1 k2 (cat0 :: Cat k0 r0) (cat1 :: Cat k1 r1) (cat2 :: Cat k2 r2) f a b c d. (Bifunctor cat0 cat1 cat2 f, OpBimap cat0 cat1 cat2 f a b c d) => cat0 a b -> cat1 c d -> cat2 (f a c) (f b d)
+
+instance BifunctorRep Repr.BoxL Repr.BoxL Repr.BoxL where
+ lmapD l = bimap l identity
+ rmapD r = bimap identity r
+ bimapD l r = compose (lmap l) (rmap r)
+
+type Bifunctor :: forall k0 k1 k2 r0 r1 r2. Cat k0 r0 -> Cat k1 r1 -> Cat k2 r2 -> (k0 -> k1 -> k2) -> Constraint
+class (Category cat0, Category cat1, Category cat2) => Bifunctor @k0 @k1 @k2 @r0 @r1 @r2 cat0 cat1 cat2 f | cat0 f -> cat1 cat2, cat1 f -> cat0 cat2, cat2 f -> cat0 cat1 where
+ {-# MINIMAL lmap, rmap | bimap #-}
+
+ lmap :: (ObLmap cat0 cat1 cat2 f a b c) => cat0 a b -> cat2 (f a c) (f b c)
+ default lmap :: (BifunctorRep r0 r1 r2, ObLmap cat0 cat1 cat2 f a b c) => cat0 a b -> cat2 (f a c) (f b c)
+ lmap = lmapD
+
+ rmap :: (OpRmap cat0 cat1 cat2 f a c d) => cat1 c d -> cat2 (f a c) (f a d)
+ default rmap :: (BifunctorRep r0 r1 r2, OpRmap cat0 cat1 cat2 f a c d) => cat1 c d -> cat2 (f a c) (f a d)
+ rmap = rmapD
+
+ bimap :: (OpBimap cat0 cat1 cat2 f a b c d) => cat0 a b -> cat1 c d -> cat2 (f a c) (f b d)
+ default bimap :: (BifunctorRep r0 r1 r2, OpBimap cat0 cat1 cat2 f a b c d) => cat0 a b -> cat1 c d -> cat2 (f a c) (f b d)
+ bimap = bimapD
type Biendofunctor :: forall k (r :: Repr). Cat k r -> (k -> k -> k) -> Constraint
type Biendofunctor cat f = Bifunctor cat cat cat f
type Hypoplexal :: forall k (r :: Repr). Cat k r -> (k -> k -> k) -> Constraint
class (Biendofunctor cat f) => Hypoplexal cat f where
- assoc :: Lev (cat (f (f a b) c) (f a (f b c)))
- coassoc :: Lev (cat (f a (f b c)) (f (f a b) c))
+ assoc :: (Ob3 cat a b c) => cat (f (f a b) c) (f a (f b c))
+ coassoc :: (Ob3 cat a b c) => cat (f a (f b c)) (f (f a b) c)
type Plexal :: forall k (r :: Repr). Cat k r -> (k -> k -> k) -> Constraint
class (Hypoplexal cat f) => Plexal @k cat f where
type IdObj cat f :: k
- idl :: Lev (cat (f (IdObj cat f) a) a)
- idr :: Lev (cat (f a (IdObj cat f)) a)
- coidl :: Lev (cat a (f (IdObj cat f) a))
- coidr :: Lev (cat a (f a (IdObj cat f)))
+ idl :: (Ob cat a) => cat (f (IdObj cat f) a) a
+ idr :: (Ob cat a) => cat (f a (IdObj cat f)) a
+ coidl :: (Ob cat a) => cat a (f (IdObj cat f) a)
+ coidr :: (Ob cat a) => cat a (f a (IdObj cat f))
-- type Hyperplexal :: forall k (r :: Repr). Cat k r -> (k -> k -> k) -> Constraint
-- class (Plexal cat f) => Hyperplexal @k cat f where
@@ -67,16 +108,19 @@ class (Hypoplexal cat f) => Plexal @k cat f where
--------------------------------------------------------------------------------
-type Hask :: forall (r :: Repr). Cat (Type r) Repr.BoxL
+type Hask :: forall r. Cat (Type r) Repr.BoxL
type Hask @r = (->)
-instance Category Hask where
+instance Category (Hask @Repr.BoxL) where
identity x = x
compose f g x = f (g x)
-instance LFunctor Hask Hask (,) where lmap f (a, b) = (f a, b)
-instance RFunctor Hask Hask (,) where rmap f (a, b) = (a, f b)
-instance Bifunctor Hask Hask Hask (,) where bimap f g (a, b) = (f a, g b)
+-- instance LFunctor Hask Hask (,) where lmap f (a, b) = (f a, b)
+-- instance RFunctor Hask Hask (,) where rmap f (a, b) = (a, f b)
+instance Bifunctor Hask Hask Hask (,) where
+ -- lmap f (a, b) = (f a, b)
+ -- rmap f (a, b) = (a, f b)
+ bimap f g (a, b) = (f a, g b)
instance Hypoplexal Hask (,) where
assoc ((a, b), c) = (a, (b, c))
coassoc (a, (b, c)) = ((a, b), c)
@@ -93,11 +137,19 @@ type Op :: forall k (r :: Repr). Cat k r -> Cat k r
newtype Op cat a b = Op (cat b a)
instance (Category cat) => Category (Op cat) where
+ type Ob (Op cat) a = Ob cat a
identity = Op identity
compose (Op f) (Op g) = Op (compose g f)
--------------------------------------------------------------------------------
+-- | Natural transformations to Hask
+type (~>) :: forall k (r :: Repr). Cat (k -> Type r) Repr.BoxL
+type f ~> g = forall a. f a -> g a
+
+{-
+
+data Natrans -- TODO: Rename Funct
type Funct :: forall k0 k1 (r0 :: Repr) (r1 :: Repr). Cat k0 r0 -> Cat k1 r1 -> Cat (k0 -> k1) r1
newtype Funct _cat0 cat1 f g = Funct (forall a. cat1 (f a) (g a))
@@ -122,6 +174,8 @@ instance LFunctor (Endofunct Hask) (Endofunct Hask) Compose where
instance RFunctor (Endofunct Hask) (Endofunct Hask) Compose where
rmap (Funct n) = Funct (Compose `compose` n `compose` unCompose)
+-}
+
--------------------------------------------------------------------------------
-- type HypoMonoid :: forall r. Type r -> Constraint
diff --git a/src/Lude/Kind.hs b/src/Lude/Kind.hs
@@ -12,7 +12,7 @@ import GHC.Exts qualified as GHC
import Lude.Repr qualified as Repr
--- TODO: CONSTRAINT
+-- TODO: CONSTRAINT (Repr-indexed)
--------------------------------------------------------------------------------
