commit 5724351a8a85cd9d3e272642b2c37eeb096d6f83 parent f9b36d26aad0e50d184854ea96098c8879bc4155 Author: Robert Russell <robert@rr3.xyz> Date: Mon, 5 Oct 2026 10:01:43 -0700 Todo: organize uncommitted experiments Diffstat:
| A | src/Todo/Bifunctors.hs | | | 49 | +++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | src/Todo/DependentKinds.hs | | | 44 | ++++++++++++++++++++++++++++++++++++++++++++ |
| A | src/Todo/ExternalProduct.hs | | | 47 | +++++++++++++++++++++++++++++++++++++++++++++++ |
| A | src/Todo/Quantifier.hs | | | 53 | +++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | src/Todo/SomeType.hs | | | 64 | ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | src/Todo/Yoneda.hs | | | 11 | +++++++++++ |
6 files changed, 268 insertions(+), 0 deletions(-)
diff --git a/src/Todo/Bifunctors.hs b/src/Todo/Bifunctors.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE UndecidableInstances #-} + +module Todo.Bifunctors where + +import Lude + +-------------------------------------------------------------------------------- + +bipreservesObj + :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k) + . forall (f :: i -> j -> k) + ->(BifunctorialOn p q r f) + => forall (a :: i) (b :: j) + ->Obj p a & Obj q b :- Obj r (f a b) +bipreservesObj f a b = Entail (MkEvidence \\ f a `preservesObj` b \\ f `preservesObj` a) + +lpreservesObj + :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k) + . forall (f :: i -> j -> k) + ->(BifunctorialOn p q r f) + => forall (a :: i) + ->forall (b :: j). (Obj q b) => Obj p a :- Obj r (f a b) +lpreservesObj f a @b = Entail (MkEvidence \\ f a `preservesObj` b \\ f `preservesObj` a) + +rpreservesObj + :: forall {i} {j} {k} (p :: Cat i) (q :: Cat j) (r :: Cat k) + . forall (f :: i -> j -> k) + ->(BifunctorialOn p q r f) + => forall (b :: j) + ->forall (a :: i). (Obj p a) => Obj q b :- Obj r (f a b) +rpreservesObj f b @a = Entail (MkEvidence \\ f a `preservesObj` b \\ f `preservesObj` a) + +-------------------------------------------------------------------------------- + +type Under :: forall {i} {j}. (i -> j) -> i -> j -> Type +newtype Under (f :: i -> j) (a :: i) (b :: j) = MkUnder {unUnder :: Cod f (f a) b} + +type Over :: forall {i} {j}. (i -> j) -> j -> i -> Type +newtype Over (f :: i -> j) (a :: j) (b :: i) = MkOver {unOver :: Cod f a (f b)} + +-------------------------------------------------------------------------------- + +type ProfunctorialOn :: forall {i} {j} {k}. Cat i -> Cat j -> Cat k -> (i -> j -> k) -> Constraint +class (BifunctorialOn (Dual p) q r f) => ProfunctorialOn p q r f | f -> p q r +instance (BifunctorialOn (Dual p) q r f) => ProfunctorialOn p q r f + +type EndoprofunctorialOn :: forall {i} {k}. Cat i -> Cat k -> (i -> i -> k) -> Constraint +class (ProfunctorialOn p p r f) => EndoprofunctorialOn p r f | f -> p r +instance (ProfunctorialOn p p r f) => EndoprofunctorialOn p r f diff --git a/src/Todo/DependentKinds.hs b/src/Todo/DependentKinds.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} + +module Todo.DependentKinds where + +import Lude + +-------------------------------------------------------------------------------- + +type (.) :: forall i j k. (j -> k) -> (i -> j) -> (i -> k) +type (f . g) x = f (g x) + +-------------------------------------------------------------------------------- + +type Forall :: forall k. (k -> Kind) -> Kind +type Forall @k f = forall (a :: k). f a + +type (@->) :: forall k -> (k -> Kind) -> Kind +type k @-> f = Forall @k f + +-------------------------------------------------------------------------------- + +type Exists :: forall k. (k -> Kind) -> Kind +data Exists _ where + MkExists :: forall k (f :: k -> Kind). forall (a :: k) -> f a -> Exists @k f + +type (@*) :: forall k -> (k -> Kind) -> Kind +type k @* f = Exists @k f + +type Idx :: forall k (f :: k -> Kind). Exists f -> k +type family Idx _ where + Idx (MkExists a _) = a + +type Val :: forall k (f :: k -> Kind). forall (e :: Exists f) -> f (Idx e) +type family Val _ where + Val (MkExists _ x) = x + +type OnIdx :: forall k (f :: k -> Kind). Predicate k -> Predicate (Exists f) +class (p (Idx e)) => OnIdx p e +instance forall k (f :: k -> Kind) (p :: Predicate k) (e :: Exists f). (p (Idx e)) => OnIdx p e + +type OnVal :: forall k (f :: k -> Kind). Forall (Predicate . f) -> Predicate (Exists f) +class (p (Val e)) => OnVal p e +instance forall k (f :: k -> Kind) (p :: Forall (Predicate . f)) (e :: Exists f). (p (Val e)) => OnVal p e diff --git a/src/Todo/ExternalProduct.hs b/src/Todo/ExternalProduct.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE UndecidableInstances #-} + +module Todo.ExternalProduct where + +import Lude + +-------------------------------------------------------------------------------- + +type Categorical4 :: forall {i} {j} {k} {l}. Cat i -> Cat j -> Cat k -> Cat l -> Constraint +type Categorical4 p q r s = All (Categorical p, Categorical q, Categorical r, Categorical s) + +type External + :: forall {i} {j} {k} {l} + . Cat i + -> Cat j + -> Cat k + -> Cat l + -> (k -> l -> Type) + -> (i -> k) + -> (j -> l) + -> (i -> j -> Type) +data External p q r s h f g a b = (Obj p a, Obj q b) => MkFoo {unFoo :: h (f a) (g b)} + +instance (BifunctorialOn r s Function h, FunctorialOn p r f, FunctorialOn q s g) => Functorial (External p q r s h f g a) where + type Dom (External p q r s h f g a) = q + type Cod (External p q r s h f g a) = Function + map m = \(MkFoo x) -> MkFoo (rmap (map m) x \\ f `preservesObj` a) \\ witnessMor m + +instance (Categorical4 p q r s, BifunctorialOn r s Function h, FunctorialOn p r f, FunctorialOn q s g) => Functorial (External p q r s h f g) where + type Dom (External p q r s h f g) = p + type Cod (External p q r s h f g) = q ==> Function + map m = Naturally \ @b (MkFoo x) -> MkFoo (lmap (map m) x \\ g `preservesObj` b) \\ witnessMor m + +instance (Categorical4 p q r s, BifunctorialOn r s Function h, FunctorialOn p r f) => Functorial (External p q r s h f) where + type Dom (External p q r s h f) = q ==> s + type Cod (External p q r s h f) = p ==> q ==> Function + map (Naturally m) = Binaturally \ @a @_b (MkFoo x) -> MkFoo (rmap m x \\ f `preservesObj` a) + +instance (Categorical4 p q r s, BifunctorialOn r s Function h) => Functorial (External p q r s h) where + type Dom (External p q r s h) = p ==> r + type Cod (External p q r s h) = (q ==> s) ==> (p ==> q ==> Function) + map (Naturally m) = Naturally \ @g -> Binaturally \ @_a @b (MkFoo x) -> MkFoo (lmap m x \\ g `preservesObj` b) + +instance (Categorical4 p q r s) => Functorial (External p q r s) where + type Dom (External p q r s) = r ==> s ==> Function + type Cod (External p q r s) = (p ==> r) ==> (q ==> s) ==> (p ==> q ==> Function) + map (Binaturally m) = Binaturally \ @f @g -> Binaturally \ @a @b (MkFoo x) -> MkFoo (m x \\ f `preservesObj` a \\ g `preservesObj` b) diff --git a/src/Todo/Quantifier.hs b/src/Todo/Quantifier.hs @@ -0,0 +1,53 @@ +module Todo.Quantifier where + +import Lude + +-------------------------------------------------------------------------------- + +-- TODO: zap? + +type Exists :: forall {i}. (i -> Type) -> Type +data Exists f = forall x. MkExists (f x) + +instance Functorial Exists where + type Dom Exists = Discrete ==> Function -- Could be generalized beyond Discrete. + type Cod Exists = Function + map (Naturally f) = \(MkExists a) -> MkExists (f a) + +type Forall :: forall {i}. (i -> Type) -> Type +data Forall f = MkForall (forall x. f x) + +instance Functorial Forall where + type Dom Forall = Discrete ==> Function -- Could be generalized beyond Discrete. + type Cod Forall = Function + map (Naturally f) = \(MkForall a) -> MkForall (f a) + +type Under :: forall {i}. (i -> Type) -> Type -> (i -> Type) +newtype Under f a x = MkUnder {unUnder :: f x -> a} + +instance Functorial (Under f a) where + type Dom (Under f a) = Dual Discrete + type Cod (Under f a) = Function + map (MkDual MkDiscrete) = identity + +instance Functorial (Under f) where + type Dom (Under f) = Function + type Cod (Under f) = Dual Discrete ==> Function + map f = Naturally \(MkUnder g) -> MkUnder (f . g) + +instance Functorial Under where + type Dom Under = Dual (Discrete ==> Function) + type Cod Under = Function ==> Dual Discrete ==> Function + map (MkDual (Naturally f)) = Naturally (Naturally \(MkUnder g) -> MkUnder (g . f)) + +-- elimExists :: forall {i} (f :: i -> Type) (a :: Type). Forall (Under f a) -> Exists f -> a +-- elimExists (MkForall k) (MkExists f) = unUnder k f + +-- elimForall :: forall {i} (f :: i -> Type) (a :: Type). Exists (Under f a) -> Forall f -> a +-- elimForall (MkExists k) (MkForall f) = unUnder k f + +elimExists :: forall {i} (f :: i -> Type) (a :: Type). Forall (Under f a) -> Under Exists a f +elimExists (MkForall k) = MkUnder \(MkExists f) -> unUnder k f + +elimForall :: forall {i} (f :: i -> Type) (a :: Type). Exists (Under f a) -> Under Forall a f +elimForall (MkExists k) = MkUnder \(MkForall f) -> unUnder k f diff --git a/src/Todo/SomeType.hs b/src/Todo/SomeType.hs @@ -0,0 +1,64 @@ +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Todo.SomeType where + +import Lude +import Lude.Haskell.Repr qualified as Repr +import Todo.DependentKinds + +-------------------------------------------------------------------------------- + +type instance DefaultCat SomeType = SomeFunction + +type SomeType :: Kind +type SomeType = Repr @* Type# + +-- | The full subcategory of arbitrarily-represented Haskell types and functions +-- whose `Repr`s are `Functional#` +type SomeFunction :: Cat SomeType +data SomeFunction a b = (Functional# `OnIdx` a, Functional# `OnIdx` b) => MkHFunction (Val a -> Val b) + +instance SomeFunction a b `Witnesses` Mor SomeFunction a b where + witness (MkHFunction _) = MkEvidence + +-- TODO: Ugghhhh this is a lie. Composition is not associative due to Haskell's +-- garbage lazy semantics. We could just say it's only lawful up to bottoms and +-- go on with life. +instance Categorical SomeFunction where + type Obj SomeFunction = OnIdx Functional# + identity = MkHFunction identityFunction + compose (MkHFunction f) (MkHFunction g) = MkHFunction (composeFunction f g) + witnessMor = witness + +type Some :: Type -> SomeType +type Some = MkExists Repr.BoxL +instance Functorial Some where + map f = MkHFunction f + +type Box :: SomeType -> Type +newtype Box a = MkBox {unBox :: Lev (Val a)} +instance Functorial Box where + map (MkHFunction f) = \(MkBox x) -> MkBox (app# f x) + +-- We can't define products `HFunction^2 -> HFunction` as +-- (r, a) * (s, b) := (Repr.Tuple [r, s], Tuple2# a b), +-- because we don't implement Functional# on tuples. Instead, +-- (r, a) * (s, b) := (BoxL, forall (t :: Repr) (c :: Type# t). (a -> b -> c) -> c), +-- i.e., Church-encoded. + +-- infixr 1 -># +-- type (->#) :: SomeType -> forall (r :: Repr). Type# r -> Type +-- type a -># b = Val a -> b + +-- infixr 1 -># +-- type (->#) :: SomeType -> SomeType -> SomeType +-- type a -># b = MkExists Repr.BoxL (Val a -> Val b) + +type Prod :: SomeType -> SomeType -> Type +newtype Prod a b = MkProd {unProd :: forall {r :: Repr} (c :: Type# r). (Val a -> Val b -> c) -> c} + +instance forall (a :: SomeType). (Obj SomeFunction a) => Functorial (Prod a) where + map (MkHFunction f) = \(MkProd p) -> MkProd \k -> p (k *.# f) +instance Functorial Prod where + map (MkHFunction f) = Naturally \(MkProd p) -> MkProd \k -> p (k .# f) diff --git a/src/Todo/Yoneda.hs b/src/Todo/Yoneda.hs @@ -0,0 +1,11 @@ +module Todo.Yoneda where + +import Lude + +-------------------------------------------------------------------------------- + +type Yoneda :: forall {i}. Endo (i -> Type) +data Yoneda f a = MkYoneda (forall x. Dom f a x -> f x) + +type Coyoneda :: forall {i}. Endo (i -> Type) +data Coyoneda f a = forall x. MkCoyoneda (Dom f x a) (f x)