commit 83c4f6a837370e1cf1f737d3cc6d07e082401a83
parent 2ddecefe35c1321a67e88cfd3b6515f7c2dce5f8
Author: Robert Russell <robert@rr3.xyz>
Date: Wed, 9 Sep 2026 14:53:09 -0700
Refactor Haskell-specific things; extend/update Algebra.Category
Diffstat:
36 files changed, 1072 insertions(+), 632 deletions(-)
diff --git a/Todo/Category.hs b/Todo/Category.hs
@@ -1,41 +1,72 @@
--------------------------------------------------------------------------------
-type Prod :: forall i j. Cat i -> Cat j -> Cat (i × j)
-data Prod p q a b where
- Prod :: p a0 b0 -> q a1 b1 -> Prod p q (a0, a1) (b0, b1)
-
--- We could simplify this, but this way it's consistent with SumObj.
-type ProdObj :: forall i j. Cat i -> Cat j -> Constraint1 (i × j)
-class ProdObj p q a where
- prodObj :: Pair1 (Evidence1 (Obj p)) (Evidence1 (Obj q)) a
-instance (Obj p i, Obj q j) => ProdObj p q (i, j) where
- prodObj = Pair1 Evidence1 Evidence1
-
-instance (Categorical p, Categorical q) => Categorical (Prod p q) where
- type Obj (Prod p q) = ProdObj p q
- identity @a = case prodObj @_ @_ @p @q @a of
- Pair1 Evidence1 Evidence1 -> Prod identity identity
- compose (Prod f0 f1) (Prod g0 g1) = Prod (compose f0 g0) (compose f1 g1)
+-- type Prod :: forall i j. Cat i -> Cat j -> Cat (i × j)
+-- data Prod p q a b where
+-- Prod :: p a0 b0 -> q a1 b1 -> Prod p q (a0, a1) (b0, b1)
+
+-- -- We could simplify this, but this way it's consistent with SumObj.
+-- type ProdObj :: forall i j. Cat i -> Cat j -> Constraint1 (i × j)
+-- class ProdObj p q a where
+-- prodObj :: Pair1 (Evidence1 (Obj p)) (Evidence1 (Obj q)) a
+-- instance (Obj p i, Obj q j) => ProdObj p q (i, j) where
+-- prodObj = Pair1 Evidence1 Evidence1
+
+-- instance (Categorical p, Categorical q) => Categorical (Prod p q) where
+-- type Obj (Prod p q) = ProdObj p q
+-- identity @a = case prodObj @_ @_ @p @q @a of
+-- Pair1 Evidence1 Evidence1 -> Prod identity identity
+-- compose (Prod f0 f1) (Prod g0 g1) = Prod (compose f0 g0) (compose f1 g1)
+
+--------------------------------------------------------------------------------
+
+-- type Sum :: forall i j. Cat i -> Cat j -> Cat (i + j)
+-- data Sum p q a b where
+-- SumL :: p a b -> Sum p q (L a) (L b)
+-- SumR :: q a b -> Sum p q (R a) (R b)
+
+-- type SumObj :: forall i j. Cat i -> Cat j -> Constraint1 (i + j)
+-- class SumObj p q a where
+-- sumObj :: Either1 (Evidence1 (Obj p)) (Evidence1 (Obj q)) a
+-- instance (Obj p a) => SumObj p q (L a) where
+-- sumObj = L1 Evidence1
+-- instance (Obj q a) => SumObj p q (R a) where
+-- sumObj = R1 Evidence1
+
+-- instance (Categorical p, Categorical q) => Categorical (Sum p q) where
+-- type Obj (Sum p q) = SumObj p q
+-- identity @a = case sumObj @_ @_ @p @q @a of
+-- L1 Evidence1 -> SumL identity
+-- R1 Evidence1 -> SumR identity
+-- compose (SumL f) (SumL g) = SumL (compose f g)
+-- compose (SumR f) (SumR g) = SumR (compose f g)
--------------------------------------------------------------------------------
-type Sum :: forall i j. Cat i -> Cat j -> Cat (i + j)
-data Sum p q a b where
- SumL :: p a b -> Sum p q (L a) (L b)
- SumR :: q a b -> Sum p q (R a) (R b)
-
-type SumObj :: forall i j. Cat i -> Cat j -> Constraint1 (i + j)
-class SumObj p q a where
- sumObj :: Either1 (Evidence1 (Obj p)) (Evidence1 (Obj q)) a
-instance (Obj p a) => SumObj p q (L a) where
- sumObj = L1 Evidence1
-instance (Obj q a) => SumObj p q (R a) where
- sumObj = R1 Evidence1
-
-instance (Categorical p, Categorical q) => Categorical (Sum p q) where
- type Obj (Sum p q) = SumObj p q
- identity @a = case sumObj @_ @_ @p @q @a of
- L1 Evidence1 -> SumL identity
- R1 Evidence1 -> SumR identity
- compose (SumL f) (SumL g) = SumL (compose f g)
- compose (SumR f) (SumR g) = SumR (compose f g)
+-- type Iso :: forall {k}. Cat k -> Cat k
+-- data Iso p a b = Iso (p a b) (p b a)
+
+-- type Representable :: forall {i} r. (i -> Type @r) -> Constraint
+-- class (Functorial f, Obj (Dom f) (ReprObj f)) => Representable (f :: i -> Type) where
+-- type ReprObj f :: i
+-- represent :: forall (a :: i). f a -> Dom f a (ReprObj f)
+
+--------------------------------------------------------------------------------
+
+-- type Either :: Biendo Type
+-- data Either a b = L a | R b
+
+-- instance forall a. Functorial (Either a) where
+-- map f = \case
+-- L x -> L x
+-- R y -> R (f y)
+
+-- instance Functorial Either where
+-- type Dom Either = Function
+-- type Cod Either = Function ==> Function
+-- map f = Natural \case
+-- L x -> L (f x)
+-- R y -> R y
+
+-- foo :: (a -> b) -> Either c a -> Either c b
+-- foo :: (a -> b) -> Nt Function Function (Either a) (Either b)
+-- foo f = map f
diff --git a/Todo/Const.hs b/Todo/Const.hs
@@ -0,0 +1,44 @@
+-- TODO: Const functors are also bifunctors?
+type HasConstFunctor :: forall {i} {j}. Cat i -> Cat j -> Constraint
+class (Categorical p, Categorical q, forall (b :: j) (f :: i -> j). (f ~ ConstOn p q b) => FunctorialOn p q f) => HasConstFunctor (p :: Cat i) (q :: Cat j) where
+ type ConstOn p q :: j -> i -> j
+
+ -- TODO: Use Iso abstraction here. Also, `p` is ambiguous, so we should
+ -- probably require the `p` type argument.
+ mkConstOn :: forall (a :: i) (b :: j). b `q` ConstOn p q b a
+ unConstOn :: forall (a :: i) (b :: j). ConstOn p q b a `q` b
+
+type Const :: forall {i}. Cat i -> Type -> i -> Type
+newtype Const p b a = MkConst {unConst :: b}
+instance (Categorical p) => Functorial (Const p b) where
+ type Dom (Const p b) = p
+ type Cod (Const p b) = Function
+ map _ = coerce
+instance (Categorical p) => HasConstFunctor p Function where
+ type ConstOn p Function = Const p
+ mkConstOn = MkConst
+ unConstOn = unConst
+
+-- TODO: Is this misnamed?
+type Tautology :: forall {i}. Cat i -> Constraint -> i -> Constraint
+class (b) => Tautology p b a
+instance (b) => Tautology p b a
+instance (Categorical p) => Functorial (Tautology p b) where
+ type Dom (Tautology p b) = p
+ type Cod (Tautology p b) = Entailment
+ map _ = Entail MkEvidence
+instance (Categorical p) => HasConstFunctor p Entailment where
+ type ConstOn p Entailment = Tautology p
+ mkConstOn = Entail MkEvidence
+ unConstOn = Entail MkEvidence
+
+instance (HasTerminalObject q, HasConstFunctor p q) => HasTerminalObject (NT p q) where
+ type Terminal (NT p q) = ConstOn p q (Terminal q)
+ terminate @f = Natural \ @a -> mkConstOn @p . terminate \\ f `preservesObj` a
+
+instance (HasInitialObject q, HasConstFunctor p q) => HasInitialObject (NT p q) where
+ type Initial (NT p q) = ConstOn p q (Initial q)
+ initiate @f = Natural \ @a -> initiate . unConstOn @p \\ f `preservesObj` a
+
+test :: forall p f. (FunctorialOn p Entailment f) => NT p Entailment f (Tautology p Verum)
+test = terminate
diff --git a/Todo/Constraint.hs b/Todo/Constraint.hs
@@ -1,21 +1,5 @@
--------------------------------------------------------------------------------
--- infixl 7 :&
-
---------------------------------------------------------------------------------
-
--- type Both :: Constraint -> Constraint -> Constraint
--- type Both = GHC.CTuple2
--- type (:&) = Both -- NOTE: Add signature once GHC#16754 is resolved
--- instance forall a b c. (a `Witnesses` b, a `Witnesses` c) => a `Witnesses` (b :& c) where
--- witness _ a = Evidence \\ witness b a \\ witness c a
-
--- type Simul :: forall {i}. Predicate i -> Predicate i -> Predicate i
--- class (p i, q i) => Simul p q i
--- instance (p i, q i) => Simul p q i
-
---------------------------------------------------------------------------------
-
-- type AllSatisfy :: forall {i}. Predicate i -> List i -> Constraint
-- type family AllSatisfy p xs where
-- AllSatisfy _ [] = Verum
diff --git a/Todo/Wip.hs b/Todo/Wip.hs
@@ -0,0 +1,9 @@
+-- type (==>) :: Constraint -> Constraint -> Constraint
+-- class a ==> b where hom :: a :- b
+
+-- curry :: forall a b c. ((a, b) ==> c) :- a ==> (b ==> c)
+-- curry = MkEntailment (withDict @(b ==> c) (MkEntailment MkEvidence) MkEvidence)
+
+-- type Cps :: Endo Constraint
+-- class Cps a where runCps :: forall r. ((a) => r) -> r
+-- instance (a) => Cps a where runCps k = k
diff --git a/package.yaml b/package.yaml
@@ -20,6 +20,7 @@ ghc-options:
- -Wall
- -Wno-name-shadowing
- -Wno-unused-foralls
+ - -Wno-unused-top-binds
- -fprint-explicit-foralls
- -fprint-explicit-kinds
- -fprint-explicit-runtime-reps
diff --git a/src/Lude/Algebra/Algebra.hs b/src/Lude/Algebra/Algebra.hs
@@ -13,13 +13,14 @@ module Lude.Algebra.Algebra (
) where
import Lude.Algebra.Category
-import Lude.Constraint
-import Lude.Kind
+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.
@@ -39,8 +40,8 @@ class DefaultRecursive p f r where
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 (Nt p q) f r) => DefaultRecursive (Nt p q) f r where
- defaultCata f@(MkNt _) = h where h = MkNt (comp f . comp (map h) . comp peel) \\ witnessMor (wrap @(Nt p q) @f @r)
+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
@@ -68,8 +69,8 @@ class DefaultCorecursive p g s where
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 (Nt p q) g s) => DefaultCorecursive (Nt p q) g s where
- defaultAna g@(MkNt _) = h where h = MkNt (comp wrap . comp (map h) . comp g) \\ witnessMor (peel @(Nt p q) @g @s)
+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
diff --git a/src/Lude/Algebra/Category.hs b/src/Lude/Algebra/Category.hs
@@ -2,10 +2,12 @@ module Lude.Algebra.Category (
module X,
) where
+import Lude.Algebra.Category.Bifunctor as X
import Lude.Algebra.Category.Core as X
import Lude.Algebra.Category.Discrete as X
-import Lude.Algebra.Category.Dual as X
-import Lude.Algebra.Category.Object as X
+import Lude.Algebra.Category.Hom as X
+import Lude.Algebra.Category.Initial as X
+import Lude.Algebra.Category.Terminal as X
-- TODO: Semicategory?
@@ -17,7 +19,8 @@ import Lude.Algebra.Category.Object as X
-- TODO: Adjunctions and zap
--- TODO: Constrained category wrapper (full subcategory with objects subject to
--- a constraint)
-
-- TODO: Eilenberg-Moore (co)algebras?
+
+-- TODO: Bifunctors? Profunctors? Etc... (other kinds of functors?)
+-- 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/Bifunctor.hs b/src/Lude/Algebra/Category/Bifunctor.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Lude.Algebra.Category.Bifunctor (
+ Bifunctorial,
+ BidomL,
+ BidomR,
+ Bicod,
+ bimap,
+ lmap,
+ rmap,
+) where
+
+import Lude.Algebra.Category.Core
+import Lude.Haskell
+
+--------------------------------------------------------------------------------
+
+-- NOTE: We ought not need to assume that BidomR p and Bicod p are categorical,
+-- because the Categorical (NT _ _) instance assumes it, but maybe there's
+-- some reason the constraint solver can't safely deduce that.
+
+type Bifunctorial :: forall {i} {j} {k}. (i -> j -> k) -> Constraint
+class (Functorial p, Cod p ~ NT (BidomR p) (Bicod p), Categorical (BidomR p), Categorical (Bicod p)) => Bifunctorial p
+instance (Functorial p, Cod p ~ NT (BidomR p) (Bicod p), Categorical (BidomR p), Categorical (Bicod p)) => Bifunctorial p
+
+type BidomL :: forall {i} {j} {k}. (i -> j -> k) -> Cat i
+type BidomL p = Dom p
+
+type BidomR :: forall {i} {j} {k}. (i -> j -> k) -> Cat j
+type BidomR p = NTDom (Cod p)
+
+type Bicod :: forall {i} {j} {k}. (i -> j -> k) -> Cat k
+type Bicod p = NTCod (Cod p)
+
+bimap
+ :: forall {i} {j} {k} (p :: i -> j -> k) la lb ra rb
+ . (Bifunctorial p)
+ => BidomL p la lb
+ -> BidomR p ra rb
+ -> Bicod p (p la ra) (p lb rb)
+bimap lf rf = (lmap lf \\ witnessMor rf) . (rmap rf \\ witnessMor lf)
+
+lmap
+ :: forall {i} {j} {k} (p :: i -> j -> k) la lb r
+ . (Bifunctorial p, Obj (BidomR p) r)
+ => BidomL p la lb
+ -> Bicod p (p la r) (p lb r)
+lmap lf = comp (map lf)
+
+rmap
+ :: forall {i} {j} {k} (p :: i -> j -> k) l ra rb
+ . (Bifunctorial p, Obj (BidomL p) l)
+ => BidomR p ra rb
+ -> Bicod p (p l ra) (p l rb)
+rmap rf = map rf \\ p `preservesObj` l
+
+--------------------------------------------------------------------------------
+
+type Homfunctorial :: forall {i}. (Cat i) -> Constraint
+class (Categorical p, Bifunctorial p, BidomL p ~ Dual p, BidomR p ~ p, Bicod p ~ Function) => Homfunctorial p
+instance (Categorical p, Bifunctorial p, BidomL p ~ Dual p, BidomR p ~ p, Bicod p ~ Function) => Homfunctorial p
diff --git a/src/Lude/Algebra/Category/Constrained.hs b/src/Lude/Algebra/Category/Constrained.hs
@@ -0,0 +1,34 @@
+module Lude.Algebra.Category.Constrained (
+ Constrained (..),
+) where
+
+import Lude.Algebra.Category.Core
+import Lude.Constraint.Core
+import Lude.Haskell
+
+--------------------------------------------------------------------------------
+
+-- | The full subcategory of objects satisfying the given constraint
+--
+-- Note the significance of "full" here: This category contains *all* morphisms
+-- between objects that satisfy the constraint, so it can not express categories
+-- that also constrain morphisms in some way (e.g., pointed objects with
+-- point-preserving morphisms).
+type Constrained :: forall {k}. Predicate k -> Cat k -> Cat k
+data Constrained c p a b = (c a, c b) => Constrain {unConstrain :: a `p` b}
+
+instance (Categorical p) => Categorical (Constrained c p) where
+ type Obj (Constrained c p) = Obj p :&: c
+ identity = Constrain identity
+ compose (Constrain f) (Constrain g) = Constrain (compose f g)
+ witnessMor (Constrain f) = MkEvidence \\ witnessMor f
+
+instance (Categorical p) => Functorial (Constrained c p a) where
+ type Dom (Constrained c p a) = Constrained c p
+ type Cod (Constrained c p a) = Function
+ map = compose
+
+instance (Categorical p) => Functorial (Constrained c p) where
+ type Dom (Constrained c p) = Dual (Constrained c p)
+ type Cod (Constrained c p) = (Constrained c p) ==> Function
+ map (MkDual f) = Natural (. f)
diff --git a/src/Lude/Algebra/Category/Core.hs b/src/Lude/Algebra/Category/Core.hs
@@ -1,47 +1,40 @@
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
+-- TODO: Consider what to re-export from Lude.Haskell.Category.
module Lude.Algebra.Category.Core (
Cat,
DefaultCat,
--
- DefaultCategorical (..),
Categorical (..),
Mor,
(.),
--
+ Dual (..),
+ --
Functorial (..),
FunctorialOn,
Endofunctorial,
EndofunctorialOn,
+ preservesObj,
--
- Nt (..),
- --
- Function,
- type (~>),
- Entailment (..),
- (:-),
- (:~),
+ NT (..),
+ type (==>),
+ NTDom,
+ NTCod,
) where
-import Lude.Constraint.Core
-import Lude.Constraint.Entailment
-import Lude.Constraint.Evidence
import Lude.Constraint.Predicate
-import Lude.Kind
+import Lude.Haskell
-- TODO: Allow non-BoxL morphism Repr?
--------------------------------------------------------------------------------
-infixr 1 ~>
-
---------------------------------------------------------------------------------
-
type DefaultCat :: forall i -> Cat i
type family DefaultCat i
-type instance DefaultCat (Type @r) = Function @r
-type instance DefaultCat (k -> l) = Nt (DefaultCat k) (DefaultCat l)
+type instance DefaultCat Type = Function
+type instance DefaultCat (k -> l) = DefaultCat k ==> DefaultCat l
-- NOTE: This is not allowed, because Type = Constraint :(
-- type instance DefaultCat Constraint = Entailment
@@ -49,15 +42,6 @@ type instance DefaultCat (k -> l) = Nt (DefaultCat k) (DefaultCat l)
--------------------------------------------------------------------------------
-- Categories
-type DefaultCategorical :: forall {i}. Predicate i -> Cat i -> Constraint
-class DefaultCategorical obj p where
- defaultWitnessObj :: (Categorical p, Obj p ~ obj) => forall a b. Witness (a `p` b) (Mor p a b)
-
-instance {-# INCOHERENT #-} (forall a b. p a b `Witnesses` Mor p a b) => DefaultCategorical obj p where
- defaultWitnessObj = witness _
-instance {-# INCOHERENT #-} DefaultCategorical Always p where
- defaultWitnessObj = tautology
-
type Categorical :: forall {i}. Cat i -> Constraint
class Categorical (p :: Cat i) where
type Obj p :: Predicate i
@@ -67,8 +51,8 @@ class Categorical (p :: Cat i) where
compose :: forall a b c. b `p` c -> a `p` b -> a `p` c
witnessMor :: forall a b. Witness (a `p` b) (Mor p a b)
- default witnessMor :: (DefaultCategorical (Obj p) p) => forall a b. Witness (a `p` b) (Mor p a b)
- witnessMor = defaultWitnessObj
+ default witnessMor :: forall a b. (Mor p a b) => Witness (a `p` b) (Mor p a b)
+ witnessMor = witnessOf tautology
type Mor :: forall {i}. Cat i -> i -> i -> Constraint
class (Obj p a, Obj p b) => Mor p a b
@@ -77,6 +61,37 @@ instance (Obj p a, Obj p b) => Mor p a b
(.) :: forall {i} (p :: Cat i) a b c. (Categorical p) => b `p` c -> a `p` b -> a `p` c
(.) = compose
+-- TODO: Flipped composition operator? More composition operators for CCCs?
+
+--------------------------------------------------------------------------------
+-- Dual
+
+-- TODO: Rename Dual to Yoneda and make Dual a type family that toggles Yoneda
+-- on and off, like Ed Kmett's hask package? It avoids some newtype wrappers
+-- at the expense of extra equality constraints.
+
+type Dual :: forall i. Cat i -> Cat i
+newtype Dual p a b = MkDual {unDual :: p b a}
+
+instance (Categorical p) => Dual p a b `Witnesses` Mor (Dual p) a b where
+ witness (MkDual f) = MkEvidence \\ witnessMor f
+
+instance (Categorical p) => Categorical (Dual p) where
+ type Obj (Dual p) = Obj p
+ identity = MkDual identity
+ compose (MkDual f) (MkDual g) = MkDual (compose g f)
+ witnessMor = witness
+
+instance (Categorical p) => Functorial (Dual p a) where
+ type Dom (Dual p a) = Dual p
+ type Cod (Dual p a) = Function
+ map = compose
+
+instance (Categorical p) => Functorial (Dual p) where
+ type Dom (Dual p) = Dual (Dual p)
+ type Cod (Dual p) = Dual p ==> Function
+ map (MkDual f) = Natural (. f)
+
--------------------------------------------------------------------------------
-- Functors
@@ -88,81 +103,107 @@ class (Categorical (Dom f), Categorical (Cod f)) => Functorial (f :: i -> j) whe
type Cod f :: Cat j
type Cod @j f = DefaultCat j
- map :: forall a b. Dom f a b -> Cod f (f a) (f b)
+ map :: forall (a :: i) (b :: i). Dom f a b -> Cod f (f a) (f b)
- preserveObj :: forall a. Obj (Dom f) a :- Obj (Cod f) (f a)
- preserveObj = MkEntailment (MkEvidence \\ witnessMor (map @f (identity :: Dom f a a)))
+ preservesObj_ :: forall (a :: i). Obj (Dom f) a :- Obj (Cod f) (f a)
+ preservesObj_ = Entail (MkEvidence \\ witnessMor (map @f (identity :: Dom f a a)))
-type FunctorialOn :: forall {k} {l}. Cat k -> Cat l -> (k -> l) -> Constraint
+type FunctorialOn :: forall {i} {j}. Cat i -> Cat j -> (i -> j) -> Constraint
class (Functorial f, Dom f ~ p, Cod f ~ q) => FunctorialOn p q f | f -> p q
instance (Functorial f, Dom f ~ p, Cod f ~ q) => FunctorialOn p q f
-type Endofunctorial :: forall {k}. (k -> k) -> Constraint
+type Endofunctorial :: forall {i}. (i -> i) -> Constraint
class (Functorial f, Dom f ~ Cod f) => Endofunctorial f
instance (Functorial f, Dom f ~ Cod f) => Endofunctorial f
-type EndofunctorialOn :: forall {k}. Cat k -> (k -> k) -> Constraint
+type EndofunctorialOn :: forall {i}. Cat i -> (i -> i) -> Constraint
class (FunctorialOn p p f) => EndofunctorialOn p f | f -> p
instance (FunctorialOn p p f) => EndofunctorialOn p f
--- TODO: Bifunctors? Profunctors? Etc... (other kinds of functors?)
--- That would allow being a functor in multiple ways (without losing coherence).
--- E.g., lists could be mappable "normally" and filterable (choose is map).
+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_
--------------------------------------------------------------------------------
-- Natural Transformations
-type Nt :: forall {i} {j}. Cat i -> Cat j -> Cat (i -> j)
-data Nt p q f g = (FunctorialOn p q f, FunctorialOn p q g) => MkNt {comp :: forall a. (Obj p a) => f a `q` g a}
+-- TODO: Add NT-like type *alias* (like ~> and :~, but with the Obj constraint)
+
+type NT :: forall {i} {j}. Cat i -> Cat j -> Cat (i -> j)
+data NT p q f g = (FunctorialOn p q f, FunctorialOn p q g) => Natural {comp :: forall a. (Obj p a) => f a `q` g a}
+
+type (==>) :: forall {i} {j}. Cat i -> Cat j -> Cat (i -> j)
+type (==>) = NT
+
+type NTDom :: forall {i} {j}. Cat (i -> j) -> Cat i
+type family NTDom _ where
+ NTDom (NT p q) = p
+
+type NTCod :: forall {i} {j}. Cat (i -> j) -> Cat j
+type family NTCod _ where
+ NTCod (NT p q) = q
+
+-- type TNT :: forall {i} r s. Cat i -> Cat (i -> Type @r)
+-- type TNT p = NT p Function
-- at :: forall {i} {j} (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j). forall (a :: i) -> (Obj p a) => Nt p q f g -> f a `q` g a
-- at _ m = comp m
-type instance Canonical Witnesses (Nt p q f g) = Mor (Nt p q) f g
-instance Nt p q f g `Witnesses` Mor (Nt p q) f g where
- witness _ (MkNt _) = MkEvidence
+instance NT p q f g `Witnesses` Mor (NT p q) f g where
+ witness (Natural _) = MkEvidence
-instance (Categorical p, Categorical q) => Categorical (Nt p q) where
- type Obj (Nt p q) = FunctorialOn p q
- identity @f = MkNt \ @a -> identity \\ (preserveObj :: Obj p a :- Obj q (f a))
- compose (MkNt a) (MkNt b) = MkNt (compose a b)
+instance (Categorical p, Categorical q) => Categorical (NT p q) where
+ type Obj (NT p q) = FunctorialOn p q
+ identity @f = Natural \ @a -> identity \\ f `preservesObj` a
+ compose (Natural a) (Natural b) = Natural (compose a b)
+ witnessMor = witness
---------------------------------------------------------------------------------
--- Function
+instance (Categorical p, Categorical q) => Functorial (NT p q a) where
+ type Dom (NT p q a) = NT p q
+ type Cod (NT p q a) = Function
+ map = compose
--- We implement this here to avoid orphans.
+instance (Categorical p, Categorical q) => Functorial (NT p q) where
+ type Dom (NT p q) = Dual (NT p q)
+ type Cod (NT p q) = NT p q ==> Function
+ map (MkDual f) = Natural (. f)
--- TODO: If Entailment doesn't belong here, then neither does Function. Move it.
-type Function :: forall r. Cat (Type @r)
-type Function @r = (->)
+--------------------------------------------------------------------------------
+-- Haskell
instance Categorical Function where
- identity x = x
- compose f g = \x -> f (g x)
+ identity = identityFunction
+ compose = composeFunction
--- | Natural transformations to `Function`/`->`
-type (~>) :: forall k r. Cat (k -> Type @r)
-type f ~> g = forall x. f x -> g x
+instance Functorial (Function a) where
+ type Dom (Function a) = Function
+ type Cod (Function a) = Function
+ map = compose
---------------------------------------------------------------------------------
--- Entailment
-
--- We implement this here to avoid orphans.
+instance Functorial Function where
+ type Dom Function = Dual Function
+ type Cod Function = Function ==> Function
+ map (MkDual f) = Natural (. f)
instance Categorical Entailment where
- identity = MkEntailment MkEvidence
- compose f g = MkEntailment (MkEvidence \\ f \\ g)
+ identity = identityEntailment
+ compose = composeEntailment
--- | Natural transformations to `Entailment`/`:-`
-type (:~) :: forall k. Cat (k -> Constraint)
-type f :~ g = forall x. f x :- g x
+instance Functorial (Entailment a) where
+ type Dom (Entailment a) = Entailment
+ type Cod (Entailment a) = Function
+ map = compose
---------------------------------------------------------------------------------
+instance Functorial Entailment where
+ type Dom Entailment = Dual Entailment
+ type Cod Entailment = Entailment ==> Function
+ map (MkDual f) = Natural (. f)
instance Functorial Evidence where
type Dom Evidence = Entailment
type Cod Evidence = Function
- map (MkEntailment f) = because f
+ map = mapEvidence
--- Dual functor Type -> Constraint? What's it do? Provide an element of the type?
--- Yes: See Ed Kmett's reflection package / the paper it's based on.
+instance Functorial Given where
+ type Dom Given = Function
+ type Cod Given = Entailment
+ map = mapGiven
diff --git a/src/Lude/Algebra/Category/Discrete.hs b/src/Lude/Algebra/Category/Discrete.hs
@@ -3,6 +3,7 @@ module Lude.Algebra.Category.Discrete (
) where
import Lude.Algebra.Category.Core
+import Lude.Haskell
-- TODO: Discrete is a groupoid.
@@ -10,8 +11,18 @@ import Lude.Algebra.Category.Core
type Discrete :: forall k. Cat k
data Discrete _ _ where
- Refl :: forall a. Discrete a a
+ MkDiscrete :: forall a. Discrete a a
instance Categorical Discrete where
- identity = Refl
- compose Refl Refl = Refl
+ identity = MkDiscrete
+ compose MkDiscrete MkDiscrete = MkDiscrete
+
+instance Functorial (Discrete a) where
+ type Dom (Discrete a) = Discrete
+ type Cod (Discrete a) = Function
+ map = compose
+
+instance Functorial Discrete where
+ type Dom Discrete = Dual Discrete
+ type Cod Discrete = Discrete ==> Function
+ map (MkDual f) = Natural (. f)
diff --git a/src/Lude/Algebra/Category/Dual.hs b/src/Lude/Algebra/Category/Dual.hs
@@ -1,21 +0,0 @@
-module Lude.Algebra.Category.Dual (
- Dual (..),
-) where
-
-import Lude.Algebra.Category.Core
-import Lude.Constraint.Core
-import Lude.Constraint.Evidence
-
---------------------------------------------------------------------------------
-
-type Dual :: forall i. Cat i -> Cat i
-newtype Dual p a b = MkDual {unDual :: p b a}
-
-type instance Canonical Witnesses (Dual p a b) = Mor (Dual p) a b
-instance (Categorical p) => Dual p a b `Witnesses` Mor (Dual p) a b where
- witness _ = deduce . witnessMor . unDual
-
-instance (Categorical p) => Categorical (Dual p) where
- type Obj (Dual p) = Obj p
- identity = MkDual identity
- compose (MkDual f) (MkDual g) = MkDual (compose g f)
diff --git a/src/Lude/Algebra/Category/Hom.hs b/src/Lude/Algebra/Category/Hom.hs
@@ -0,0 +1,38 @@
+module Lude.Algebra.Category.Hom (
+ Hom (..),
+) where
+
+import Lude.Algebra.Category.Core
+import Lude.Haskell
+
+-- NOTE: Ideally, we could use DerivingVia to implement (for all categories `p`
+-- and objects `a`) `Functorial` on `p a` and `p`, but DerivingVia doesn't
+-- really work with associated type families.
+
+--------------------------------------------------------------------------------
+
+-- | The Hom functor for a category
+--
+-- Most categories @p@ should implement `Functorial` directly, but @Hom p@ is
+-- available if they don't.
+type Hom :: forall i. Cat i -> Cat i
+newtype Hom p a b = MkHom {unHom :: p a b}
+
+instance (Categorical p) => Hom p a b `Witnesses` Mor (Hom p) a b where
+ witness (MkHom f) = MkEvidence \\ witnessMor f
+
+instance (Categorical p) => Categorical (Hom p) where
+ type Obj (Hom p) = Obj p
+ identity = MkHom identity
+ compose (MkHom f) (MkHom g) = MkHom (compose f g)
+ witnessMor = witness
+
+instance (Categorical p) => Functorial (Hom p a) where
+ type Dom (Hom p a) = Hom p
+ type Cod (Hom p a) = Function
+ map = compose
+
+instance (Categorical p) => Functorial (Hom p) where
+ type Dom (Hom p) = Dual (Hom p)
+ type Cod (Hom p) = Hom p ==> Function
+ map (MkDual f) = Natural (. f)
diff --git a/src/Lude/Algebra/Category/Initial.hs b/src/Lude/Algebra/Category/Initial.hs
@@ -0,0 +1,28 @@
+module Lude.Algebra.Category.Initial (
+ HasInitialObject (..),
+ absurd,
+) where
+
+import Lude.Algebra.Category.Core
+import Lude.Constraint.Falsum
+import Lude.Haskell
+import Lude.Void
+
+--------------------------------------------------------------------------------
+
+type HasInitialObject :: forall {i}. Cat i -> Constraint
+class (Categorical p) => HasInitialObject (p :: Cat i) where
+ type Initial p :: i
+ initiate :: forall (a :: i). (Obj p a) => Initial p `p` a
+
+-- | Alias for `initiate`
+absurd :: forall {i} (a :: i) (p :: Cat i). (HasInitialObject p, Obj p a) => Initial p `p` a
+absurd = initiate
+
+instance HasInitialObject Function where
+ type Initial Function = Void
+ initiate = \case {}
+
+instance HasInitialObject Entailment where
+ type Initial Entailment = Falsum
+ initiate = Entail contradiction
diff --git a/src/Lude/Algebra/Category/Object.hs b/src/Lude/Algebra/Category/Object.hs
@@ -1,52 +0,0 @@
-module Lude.Algebra.Category.Object (
- HasTerminalObject (..),
- trivial,
- HasInitialObject (..),
- absurd,
-) where
-
-import Lude.Algebra.Category.Core
-import Lude.Constraint.Core
-import Lude.Constraint.Falsum
-import Lude.Constraint.Verum
-import Lude.Kind
-import Lude.Unit
-import Lude.Void
-
---------------------------------------------------------------------------------
-
-type HasTerminalObject :: forall {k}. Cat k -> Constraint
-class (Categorical p) => HasTerminalObject (p :: Cat k) where
- type Terminal p :: k
- terminate :: forall a. a `p` Terminal p
-
--- | Alias for `terminate`
-trivial :: (HasTerminalObject p) => forall a. a `p` Terminal p
-trivial = terminate
-
-instance HasTerminalObject Function where
- type Terminal Function = Unit
- terminate = \_ -> ()
-
-instance HasTerminalObject Entailment where
- type Terminal Entailment = Verum
- terminate = MkEntailment MkEvidence
-
---------------------------------------------------------------------------------
-
-type HasInitialObject :: forall {k}. Cat k -> Constraint
-class (Categorical p) => HasInitialObject (p :: Cat k) where
- type Initial p :: k
- initiate :: forall a. Initial p `p` a
-
--- | Alias for `initiate`
-absurd :: (HasInitialObject p) => forall a. Initial p `p` a
-absurd = initiate
-
-instance HasInitialObject Function where
- type Initial Function = Void
- initiate = \case {}
-
-instance HasInitialObject Entailment where
- type Initial Entailment = Falsum
- initiate = MkEntailment contradiction
diff --git a/src/Lude/Algebra/Category/README.md b/src/Lude/Algebra/Category/README.md
@@ -0,0 +1,2 @@
+The design of the encoding of categories in this module is heavily inspired
+by Ed Kmett's hask package.
diff --git a/src/Lude/Algebra/Category/Terminal.hs b/src/Lude/Algebra/Category/Terminal.hs
@@ -0,0 +1,28 @@
+module Lude.Algebra.Category.Terminal (
+ HasTerminalObject (..),
+ trivial,
+) where
+
+import Lude.Algebra.Category.Core
+import Lude.Constraint.Verum
+import Lude.Haskell
+import Lude.Unit
+
+--------------------------------------------------------------------------------
+
+type HasTerminalObject :: forall {i}. Cat i -> Constraint
+class (Categorical p) => HasTerminalObject (p :: Cat i) where
+ type Terminal p :: i
+ terminate :: forall (a :: i). (Obj p a) => a `p` Terminal p
+
+-- | Alias for `terminate`
+trivial :: forall {i} (a :: i) {p :: Cat i}. (HasTerminalObject p, Obj p a) => a `p` Terminal p
+trivial = terminate
+
+instance HasTerminalObject Function where
+ type Terminal Function = Unit
+ terminate = \_ -> ()
+
+instance HasTerminalObject Entailment where
+ type Terminal Entailment = Verum
+ terminate = Entail MkEvidence
diff --git a/src/Lude/Constraint.hs b/src/Lude/Constraint.hs
@@ -3,18 +3,10 @@ module Lude.Constraint (
) where
import Lude.Constraint.Core as X
-import Lude.Constraint.Entailment as X
-import Lude.Constraint.Evidence as X
import Lude.Constraint.Falsum as X
import Lude.Constraint.Predicate as X
import Lude.Constraint.Verum as X
--- TODO: "Dual" concept to Witnesses? (Swap roles of types and constraints.)
---
--- type Induces :: Constraint -> Type -> Constraint
--- class Induces a b where
--- induce :: (a) => b
-
-- TODO: In multiple places, we have the same thing "normally" and with an
-- index. This should be abstracted-out.
diff --git a/src/Lude/Constraint/Core.hs b/src/Lude/Constraint/Core.hs
@@ -1,43 +1,31 @@
{-# LANGUAGE UndecidableSuperClasses #-}
module Lude.Constraint.Core (
- Canonical,
- Canonically,
- Evidence (..),
- Entailment (..),
- (:-),
+ And,
+ type (&),
+ And',
+ (:&:),
) where
-import Lude.Kind
+import Prelude.Experimental qualified as GHC
---------------------------------------------------------------------------------
-
-infixr 1 :-
+import Lude.Haskell
--------------------------------------------------------------------------------
-type Canonical :: forall {k} {l}. Relation k l -> k -> l
-type family Canonical r a
-
--- | Constrain a relation @a `r` b@ to have a *canonical* `b` per `a` (i.e.,
--- `r` is a "function")
-type Canonically :: forall {k} {l}. Endo (Relation k l)
-class (a `r` b, b ~ Canonical r a) => Canonically r a b
-
-instance (a `r` b, b ~ Canonical r a) => Canonically r a b
+infixl 7 &
--------------------------------------------------------------------------------
--- | Evidence of a constraint
-type Evidence :: Constraint -> Type
-data Evidence a = (a) => MkEvidence
+type And :: Biendo Constraint
+type And = GHC.CTuple2
+
+type (&) :: Biendo Constraint
+type (&) = And
--- | Evidence that one constraint entails another
---
--- `Entailment` (`:-`) is to `Constraint` what `Function` (`->`) is to `Type`.
-type Entailment :: Cat Constraint
-newtype Entailment a b = MkEntailment {unEntailment :: (a) => Evidence b}
+type And' :: forall {k}. Biendo (Predicate k)
+class (a x, b x) => And' a b x
+instance (a x, b x) => And' a b x
--- | Infix alias for `Entailment`
-type (:-) :: Cat Constraint
-type (:-) = Entailment
+type (:&:) :: forall {k}. Biendo (Predicate k)
+type (:&:) = And'
diff --git a/src/Lude/Constraint/Entailment.hs b/src/Lude/Constraint/Entailment.hs
@@ -1,17 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-
-module Lude.Constraint.Entailment (
- pattern Duh,
- entails,
-) where
-
-import Lude.Constraint.Core
-
---------------------------------------------------------------------------------
-
-pattern Duh :: forall a b. (a) => (b) => a :- b
-pattern Duh = MkEntailment MkEvidence
-{-# COMPLETE Duh #-}
-
-entails :: forall a b. ((a) => b) => a :- b
-entails = MkEntailment MkEvidence
diff --git a/src/Lude/Constraint/Evidence.hs b/src/Lude/Constraint/Evidence.hs
@@ -1,69 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-
-module Lude.Constraint.Evidence (
- Witness,
- Witnesses (..),
- (:=>),
- consider,
- tautology,
- because,
- (\\),
- deduce,
-) where
-
-import Lude.Constraint.Core
-import Lude.Kind
-
---------------------------------------------------------------------------------
-
-infixr 1 :=>
-infixl 1 \\
-
---------------------------------------------------------------------------------
--- Witnesses
-
-type Witness :: Type -> Constraint -> Type
-type Witness a b = a -> Evidence b
-
--- | Relation that a type carries evidence of a constraint
-type Witnesses :: Relation Type Constraint
-class Witnesses a b where
- -- | Witness a conclusion `b` of `a`
- --
- -- `a` does not determine `b`, so we require a type argument.
- witness :: forall b' -> (b' ~ b) => Witness a b'
-
--- | Infix alias for @Canonically Witnesses@
-type (:=>) :: Relation Type Constraint
-type (:=>) = Canonically Witnesses
-
--- | Witness the canonical conclusion `b` of `a`
---
--- Unlike `witness`, `a` determines `b`, so we don't require a type argument.
-consider :: forall a b. (a :=> b) => Witness a b
-consider = witness b
-
-tautology :: forall a b. (b) => Witness a b
-tautology _ = MkEvidence
-
--- | Given that `a` (canonically) witnesses `c`, resolve a `c`-predicated
--- `b` with an `a`
-because, (\\) :: forall b a c. (a :=> c) => ((c) => b) -> a -> b
-b `because` a = case consider a of MkEvidence -> b
-(\\) = because
-
--- | Given that `a` (canonically) witnesses `b` and `b` implies `c`, we know
--- that `a` witnesses `c`
-deduce :: forall c a b. (a :=> b, (b) => c) => Witness a c
-deduce = (MkEvidence \\)
-
---------------------------------------------------------------------------------
--- Instances
-
-type instance forall a. Canonical Witnesses (Evidence a) = a
-instance forall a. Evidence a `Witnesses` a where
- witness _ e = e
-
-type instance forall a b. Canonical Witnesses (a :- b) = b
-instance forall a b. (a) => (a :- b) `Witnesses` b where
- witness _ (MkEntailment b) = b
diff --git a/src/Lude/Constraint/Falsum.hs b/src/Lude/Constraint/Falsum.hs
@@ -2,7 +2,7 @@ module Lude.Constraint.Falsum (
Falsum (..),
) where
-import Lude.Kind
+import Lude.Haskell
--------------------------------------------------------------------------------
diff --git a/src/Lude/Constraint/Predicate.hs b/src/Lude/Constraint/Predicate.hs
@@ -1,17 +1,16 @@
module Lude.Constraint.Predicate (
Always,
- Never,
always,
+ Never,
never,
) where
-import Lude.Constraint.Core
-import Lude.Constraint.Evidence
import Lude.Constraint.Falsum
-import Lude.Kind
+import Lude.Haskell
-- TODO: I don't like this organization. Why isn't Always/Never treated the
--- same as Verum/Falsum?
+-- same as Verum/Falsum? These can probably just be terminal/initial objects
+-- in a functor category.
--------------------------------------------------------------------------------
@@ -19,11 +18,8 @@ type Always :: forall {i}. Predicate i
class Always x
instance forall x. Always x
-instance {-# INCOHERENT #-} forall a x. a `Witnesses` Always x where
- witness _ _ = MkEvidence
-
always :: forall a x. a :- Always x
-always = MkEntailment MkEvidence
+always = Entail MkEvidence
--------------------------------------------------------------------------------
@@ -31,4 +27,4 @@ type Never :: forall {i}. Predicate i
class (Falsum) => Never x
never :: forall x a. Never x :- a
-never = MkEntailment contradiction
+never = Entail contradiction
diff --git a/src/Lude/Constraint/Verum.hs b/src/Lude/Constraint/Verum.hs
@@ -2,15 +2,10 @@ module Lude.Constraint.Verum (
Verum,
) where
-import Lude.Constraint.Core
-import Lude.Constraint.Evidence
-import Lude.Kind
+import Lude.Haskell
--------------------------------------------------------------------------------
type Verum :: Constraint
class Verum
instance Verum
-
-instance {-# INCOHERENT #-} forall a. a `Witnesses` Verum where
- witness _ _ = MkEvidence
diff --git a/src/Lude/Either.hs b/src/Lude/Either.hs
@@ -6,7 +6,7 @@ module Lude.Either (
type (+^),
) where
-import Lude.Kind
+import Lude.Haskell
-- TODO: It's probably not worth defining our own type here.
diff --git a/src/Lude/Haskell.hs b/src/Lude/Haskell.hs
@@ -0,0 +1,10 @@
+module Lude.Haskell (
+ module X,
+) where
+
+import Lude.Haskell.Category as X -- TODO: Probably hide some stuff from here.
+import Lude.Haskell.Constraint as X
+import Lude.Haskell.Equality as X
+import Lude.Haskell.Kind as X
+import Lude.Haskell.Repr as X (Repr)
+import Lude.Haskell.Type as X
diff --git a/src/Lude/Haskell/Category.hs b/src/Lude/Haskell/Category.hs
@@ -0,0 +1,271 @@
+module Lude.Haskell.Category (
+ Cat,
+ Function,
+ type (~>),
+ identityFunction,
+ composeFunction,
+ Entailment (..),
+ (:-),
+ (:~),
+ identityEntailment,
+ composeEntailment,
+ --
+ Evidence (..),
+ mapEvidence,
+ unmapEvidence,
+ Given (..),
+ give,
+ explicit,
+ implicit,
+ mapGiven,
+ unmapGiven,
+ --
+ Witness,
+ Coprovision,
+ Provision,
+ Cowitness,
+ pattern MkProvision,
+ unProvision,
+ pattern MkCowitness,
+ unCowitness,
+ --
+ witnessSelf,
+ coprovisionSelf,
+ provisionSelf,
+ cowitnessSelf,
+ witnessOf,
+ coprovisionOf,
+ provisionOf,
+ cowitnessOf,
+ --
+ Witnesses (..),
+ (:|=),
+ Provisions (..),
+ (:|-),
+ --
+ because,
+ (\\),
+ tautology,
+) where
+
+import Data.Function qualified
+import GHC.Exts qualified as GHC
+
+import Lude.Haskell.Constraint
+import Lude.Haskell.Kind
+import Lude.Haskell.Type
+
+-- NOTE: `Entailment`/`:-` is to `Constraint` what `Function`/`->` is to `Type`.
+
+--------------------------------------------------------------------------------
+
+infixr 1 ~>, :-, :~, :|=, :|-
+infixl 1 \\
+
+--------------------------------------------------------------------------------
+-- The Function and Entailment categories
+
+-- | The kind of categories
+type Cat :: Kind -> Kind
+type Cat i = i -> i -> Type
+
+-- | Functions between two types (which form a category)
+type Function :: Cat Type
+type Function = (->)
+
+-- | Natural transformations to `Function`/`->`
+type (~>) :: forall i r. Cat (i -> Type @r)
+type f ~> g = forall x. f x -> g x
+
+identityFunction :: forall a. a -> a
+identityFunction = Data.Function.id
+
+composeFunction :: forall a b c. (b -> c) -> (a -> b) -> (a -> c)
+composeFunction = (Data.Function..)
+
+-- | Entailments between two constraints (which form a category)
+type Entailment :: Cat Constraint
+newtype Entailment a b = Entail {unEntail :: (a) => Evidence b}
+
+-- | Infix alias for `Entailment` (like `(->)` for `Function`)
+type (:-) :: Cat Constraint
+type (:-) = Entailment
+
+-- | Natural transformations to `Entailment`/`:-`
+type (:~) :: forall i. Cat (i -> Constraint)
+type f :~ g = forall x. f x :- g x
+
+identityEntailment :: forall a. a :- a
+identityEntailment = Entail MkEvidence
+
+composeEntailment :: forall a b c. (b :- c) -> (a :- b) -> (a :- c)
+composeEntailment bc ab = Entail case ab of
+ Entail MkEvidence -> case bc of
+ Entail MkEvidence -> MkEvidence
+
+--------------------------------------------------------------------------------
+-- The Evidence and Given functors
+
+-- | Type of evidence of a constraint
+--
+-- `Evidence` and `Given` form an adjoint equivalence of the `Function` and
+-- `Entailment` categories.
+type Evidence :: Constraint -> Type
+data Evidence a = (a) => MkEvidence
+
+mapEvidence :: forall a b. (a :- b) -> (Evidence a -> Evidence b)
+mapEvidence f = \MkEvidence -> unEntail f
+
+unmapEvidence :: forall a b. (Evidence a -> Evidence b) -> (a :- b)
+unmapEvidence f = Entail (f MkEvidence)
+
+-- | Constraint that a value of a type is given
+--
+-- `Given` and `Evidence` form an adjoint equivalence of the `Function` and
+-- `Entailment` categories.
+type Given :: Type -> Constraint
+class Given a where given :: a
+
+give :: forall a r. a -> ((Given a) => r) -> r
+give = GHC.withDict @(Given a)
+
+-- | Make an \"implicit\" function \"explicit\"
+explicit :: forall a b. ((Given a) => b) -> (a -> b)
+explicit x = (`give` x)
+
+-- | Make an \"explicit\" function \"implicit\"
+implicit :: forall a b. (a -> b) -> ((Given a) => b)
+implicit f = f given
+
+mapGiven :: forall a b. (a -> b) -> (Given a :- Given b)
+mapGiven f = Entail (give (f given) MkEvidence)
+
+unmapGiven :: forall a b. (Given a :- Given b) -> (a -> b)
+unmapGiven f = explicit case f of Entail MkEvidence -> given
+
+--------------------------------------------------------------------------------
+-- Morphism types involved in the ambidextrous adjunction between Evidence
+-- and Given
+
+-- | @a -> Evidence b@
+type Witness :: Type -> Constraint -> Type
+type Witness a b = a -> Evidence b
+
+-- | @Given a :- b@
+type Coprovision :: Type -> Constraint -> Type
+type Coprovision a b = Given a :- b
+
+-- | @a :- Given b@
+type Provision :: Constraint -> Type -> Type
+type Provision a b = a :- Given b
+
+-- | @Evidence a -> b@
+type Cowitness :: Constraint -> Type -> Type
+type Cowitness a b = Evidence a -> b
+
+-- NOTE: Provision/Cowitness essentially correspond to conditional types
+-- `(a) => b`, so we provide constructors/destructors for Provision and
+-- Cowitness that make this connection explicit.
+
+pattern MkProvision :: forall a b. ((a) => b) -> Provision a b
+pattern MkProvision ab <- (unProvision -> ab)
+ where
+ MkProvision ab = Entail (give ab MkEvidence)
+{-# COMPLETE MkProvision #-}
+
+unProvision :: forall a b. Provision a b -> ((a) => b)
+unProvision (Entail MkEvidence) = given
+
+pattern MkCowitness :: forall a b. ((a) => b) -> Cowitness a b
+pattern MkCowitness ab <- (unCowitness -> ab)
+ where
+ MkCowitness ab = \MkEvidence -> ab
+{-# COMPLETE MkCowitness #-}
+
+unCowitness :: forall a b. Cowitness a b -> ((a) => b)
+unCowitness h = h MkEvidence
+
+--------------------------------------------------------------------------------
+-- (Co)units and transposes for the ambidextrous adjunction between Evidence
+-- and Given
+
+witnessSelf :: forall a. Witness a (Given a)
+witnessSelf = explicit MkEvidence
+
+coprovisionSelf :: forall a. Coprovision (Evidence a) a
+coprovisionSelf = Entail given
+
+provisionSelf :: forall a. Provision a (Evidence a)
+provisionSelf = MkProvision MkEvidence
+
+cowitnessSelf :: forall a. Cowitness (Given a) a
+cowitnessSelf = MkCowitness given
+
+witnessOf :: forall a b. Coprovision a b -> Witness a b
+witnessOf h = explicit (unEntail h)
+
+coprovisionOf :: forall a b. Witness a b -> Coprovision a b
+coprovisionOf h = Entail (h given)
+
+provisionOf :: forall a b. Cowitness a b -> Provision a b
+provisionOf h = MkProvision (unCowitness h)
+
+cowitnessOf :: forall a b. Provision a b -> Cowitness a b
+cowitnessOf h = MkCowitness (unProvision h)
+
+--------------------------------------------------------------------------------
+-- "Canonical" witnesses/coprovisions and provisions/cowitnesses
+
+-- NOTE: There are some asymmetries here that we owe to the Function-bias of
+-- Haskell. I.e., both Function and Entailment homs live in Function.
+
+-- | Types `a` that "canonically" witness/coprovision `b`
+type Witnesses :: Type -> Constraint -> Constraint
+class Witnesses a b | a -> b where
+ {-# MINIMAL witness | coprovision #-}
+ witness :: Witness a b
+ witness = witnessOf coprovision
+ coprovision :: Coprovision a b
+ coprovision = coprovisionOf witness
+
+-- | Alias for `Witnesses`
+type (:|=) = Witnesses
+
+instance forall a. Evidence a `Witnesses` a where
+ witness = identityFunction
+instance forall a b. (a) => (a :- b) `Witnesses` b where
+ witness (Entail x) = x
+
+-- | Compose a canonical witness with a cowitness
+-- witnessVia :: forall a c b. (a :|= b) => Cowitness b c -> (a -> c)
+-- witnessVia = (`composeFunction` witness)
+
+-- | Constraints `a` that "canonically" provision/cowitness `b`
+type Provisions :: Constraint -> Type -> Constraint
+class Provisions a b | a -> b where
+ {-# MINIMAL provision | cowitness #-}
+ provision :: Provision a b
+ provision = provisionOf cowitness
+ cowitness :: Cowitness a b
+ cowitness = cowitnessOf provision
+
+-- | Alias for `Provisions`
+type (:|-) = Provisions
+
+instance forall a. Given a `Provisions` a where
+ provision = identityEntailment
+
+-- | Compose a canonical provision with a coprovision
+-- provisionVia :: forall a c b. (a :|- b) => Coprovision b c -> (a :- c)
+-- provisionVia = (`composeEntailment` provision)
+
+--------------------------------------------------------------------------------
+-- Utility
+
+-- | \"Compose\" a canonical witness with a conditional type
+because, (\\) :: forall a c b. (a :|= b) => ((b) => c) -> a -> c
+because bc = MkCowitness bc `composeFunction` witness
+(\\) = because
+
+tautology :: forall a b. (b) => a :- b
+tautology = Entail MkEvidence
diff --git a/src/Lude/Haskell/Constraint.hs b/src/Lude/Haskell/Constraint.hs
@@ -0,0 +1,45 @@
+module Lude.Haskell.Constraint (
+ Constraint,
+ Constraint1,
+ Predicate,
+ Relation,
+ All,
+) where
+
+import Data.Tuple.Experimental qualified as GHC
+import GHC.Exts qualified as GHC
+
+import Lude.Haskell.Kind
+
+-- TODO: Delete Constraint1 in favor of Predicate? We'd also need a replacement
+-- name for Type1. Maybe "Family"?
+
+--------------------------------------------------------------------------------
+
+type Constraint :: KindR
+type Constraint @r = GHC.CONSTRAINT r
+
+type Constraint1 :: Kind -> KindR
+type Constraint1 i @r = Predicate i @r
+
+type Predicate :: Kind -> KindR
+type Predicate i @r = i -> Constraint @r
+
+type Relation :: Kind -> Kind -> KindR
+type Relation i j @r = i -> j -> Constraint @r
+
+--------------------------------------------------------------------------------
+
+type All :: forall {k}. k -> Constraint
+type family All _ where
+ All () = GHC.CTuple0
+ All (a) = GHC.CTuple1 a
+ All (a, b) = GHC.CTuple2 a b
+ All (a, b, c) = GHC.CTuple3 a b c
+ All (a, b, c, d) = GHC.CTuple4 a b c d
+ All (a, b, c, d, e) = GHC.CTuple5 a b c d e
+ All (a, b, c, d, e, f) = GHC.CTuple6 a b c d e f
+ All (a, b, c, d, e, f, g) = GHC.CTuple7 a b c d e f g
+ All (a, b, c, d, e, f, g, h) = GHC.CTuple8 a b c d e f g h
+ All (a, b, c, d, e, f, g, h, i) = GHC.CTuple9 a b c d e f g h i
+ All (GHC.MkSolo a) = GHC.CTuple1 a
diff --git a/src/Lude/Haskell/Defunctionalization.hs b/src/Lude/Haskell/Defunctionalization.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Lude.Haskell.Defunctionalization (
+
+) where
+
+import Lude.Haskell.Kind
+
+-- TODO: All this is tentative. It's mostly for functors which aren't determined
+-- by their object map.
+
+--------------------------------------------------------------------------------
+
+-- | An empty kind with a phantom kind index, used to make @T k@ opaque
+type T' :: Kind -> Kind
+data T' k
+
+-- | A type expression (of a given kind)
+type T :: Kind -> Kind
+type T k = T' k -> Kind
+
+type Splice :: forall {k}. T k -> k
+type family Splice _
+
+data Quote :: forall {k}. k -> T k
+type instance Splice (Quote a) = a
+
+-- | Defunctionalized @(->)@
+type (-->) :: Kind -> Kind -> Kind
+type k --> l = k -> T l
+
+infixr 1 -->
+
+type Apply :: forall {k} {l}. (k --> l) -> k -> l
+type Apply f a = Splice (f a)
+
+type (@@) :: forall {k} {l}. (k --> l) -> k -> l
+type f @@ a = Apply f a
+infixl 7 @@
+
+type Defun = Defun1
+data Defun1 :: forall k0 k. (k0 -> k) -> (k0 --> k)
+type instance Splice (Defun1 f a) = f a
+
+data Defun2 :: forall k0 k1 k. (k0 -> k1 -> k) -> (k0 --> k1 --> k)
+type instance Splice (Defun2 f a) = Defun1 (f a)
+
+data Defun3 :: forall k0 k1 k2 k. (k0 -> k1 -> k2 -> k) -> (k0 --> k1 --> k2 --> k)
+type instance Splice (Defun3 f a) = Defun2 (f a)
+
+data Defun4 :: forall k0 k1 k2 k3 k. (k0 -> k1 -> k2 -> k3 -> k) -> (k0 --> k1 --> k2 --> k3 --> k)
+type instance Splice (Defun4 f a) = Defun3 (f a)
+
+type Ident :: forall {k}. k --> k
+type Ident = Quote
+
+data Compose :: forall {k} {l} {m}. (l --> m) -> (k --> l) -> (k --> m)
+type instance Splice (Compose f g x) = Splice (f (Splice (g x)))
diff --git a/src/Lude/Haskell/Equality.hs b/src/Lude/Haskell/Equality.hs
@@ -0,0 +1,10 @@
+module Lude.Haskell.Equality (
+ (:~:) (..),
+ (:~~:) (..),
+ type (~),
+ type (~~),
+) where
+
+import Data.Type.Equality ((:~:) (..), (:~~:) (..), type (~), type (~~))
+
+--------------------------------------------------------------------------------
diff --git a/src/Lude/Haskell/Kind.hs b/src/Lude/Haskell/Kind.hs
@@ -0,0 +1,25 @@
+module Lude.Haskell.Kind (
+ Kind,
+ KindR,
+ Endo,
+ Biendo,
+) where
+
+import GHC.Exts qualified as GHC
+
+import Lude.Haskell.Repr (Repr)
+import Lude.Haskell.Repr qualified as Repr
+
+--------------------------------------------------------------------------------
+
+type Kind = GHC.TYPE Repr.BoxL
+
+-- | The kind of "invisibly" `Repr`-generic types and constraints
+type KindR :: Kind
+type KindR = forall (r :: Repr). Kind
+
+type Endo :: Kind -> Kind
+type Endo i = i -> i
+
+type Biendo :: Kind -> Kind
+type Biendo i = i -> i -> i
diff --git a/src/Lude/Haskell/Repr.hs b/src/Lude/Haskell/Repr.hs
@@ -0,0 +1,90 @@
+module Lude.Haskell.Repr (
+ Levity (..),
+ Repr,
+ Tuple,
+ Sum,
+ Box,
+ BoxL,
+ BoxU,
+ Addr,
+ Int,
+ Int8,
+ Int16,
+ Int32,
+ Int64,
+ Nat,
+ Nat8,
+ Nat16,
+ Nat32,
+ Nat64,
+ Flt32,
+ Flt64,
+) where
+
+import GHC.Exts (Levity (..))
+import GHC.Exts qualified as GHC
+
+-- TODO: SIMD
+
+-- TODO: Export patterns? (Non-exhaustive until we add SIMD support.)
+
+-- TODO: Rename "Tuple" and "Sum". I don't like how asymmetric these names are.
+
+--------------------------------------------------------------------------------
+
+type Repr = GHC.RuntimeRep
+
+type Tuple = GHC.TupleRep
+type Sum = GHC.SumRep
+type Box = GHC.BoxedRep
+type BoxL = GHC.BoxedRep Lifted
+type BoxU = GHC.BoxedRep Unlifted
+type Addr = GHC.AddrRep
+type Int = GHC.IntRep
+type Int8 = GHC.Int8Rep
+type Int16 = GHC.Int16Rep
+type Int32 = GHC.Int32Rep
+type Int64 = GHC.Int64Rep
+type Nat = GHC.WordRep
+type Nat8 = GHC.Word8Rep
+type Nat16 = GHC.Word16Rep
+type Nat32 = GHC.Word32Rep
+type Nat64 = GHC.Word64Rep
+type Flt32 = GHC.FloatRep
+type Flt64 = GHC.DoubleRep
+
+--------------------------------------------------------------------------------
+
+-- pattern Tuple :: [Repr] -> Repr
+-- pattern Tuple rs = GHC.TupleRep rs
+
+-- pattern Sum :: [Repr] -> Repr
+-- pattern Sum rs = GHC.SumRep rs
+
+-- pattern Box :: Levity -> Repr
+-- pattern Box l = GHC.BoxedRep l
+
+-- pattern BoxL, BoxU :: Repr
+-- pattern BoxL = Box Lifted
+-- pattern BoxU = Box Unlifted
+
+-- pattern Addr :: Repr
+-- pattern Addr = GHC.AddrRep
+
+-- pattern Int, Int8, Int16, Int32, Int64 :: Repr
+-- pattern Int = GHC.IntRep
+-- pattern Int8 = GHC.Int8Rep
+-- pattern Int16 = GHC.Int16Rep
+-- pattern Int32 = GHC.Int32Rep
+-- pattern Int64 = GHC.Int64Rep
+
+-- pattern Nat, Nat8, Nat16, Nat32, Nat64 :: Repr
+-- pattern Nat = GHC.WordRep
+-- pattern Nat8 = GHC.Word8Rep
+-- pattern Nat16 = GHC.Word16Rep
+-- pattern Nat32 = GHC.Word32Rep
+-- pattern Nat64 = GHC.Word64Rep
+
+-- pattern Flt32, Flt64 :: Repr
+-- pattern Flt32 = GHC.FloatRep
+-- pattern Flt64 = GHC.DoubleRep
diff --git a/src/Lude/Haskell/Type.hs b/src/Lude/Haskell/Type.hs
@@ -0,0 +1,83 @@
+module Lude.Haskell.Type (
+ Type,
+ Type1,
+ Lev,
+ Tuple#,
+ Tuple,
+) where
+
+import Data.Tuple.Experimental qualified as GHC
+import GHC.Exts qualified as GHC
+
+import Lude.Haskell.Kind
+import Lude.Haskell.Repr (Repr)
+import Lude.Haskell.Repr qualified as Repr
+
+--------------------------------------------------------------------------------
+
+type Type :: KindR
+type Type @r = GHC.TYPE r
+
+type Type1 :: Kind -> KindR
+type Type1 i @r = i -> Type @r
+
+-- | Transparently box a type of any representation
+--
+-- Use `Lev` to declare unlifted values at the top-level. For example, for any
+-- @r :: Repr@, @A :: Type r@, and @bar :: A@:
+-- @
+-- foo :: Lev A
+-- foo = bar
+-- @
+type Lev :: forall {r}. Type @r -> Type
+type Lev a = (GHC.CTuple0) => a
+
+--------------------------------------------------------------------------------
+-- Tuples
+
+type R :: forall {r}. Type @r -> Repr
+type family R _ where
+ R (_ :: Type @r) = r
+
+type TupleRepr :: forall {k}. k -> Repr
+type family TupleRepr _ where
+ TupleRepr () = Repr.Tuple []
+ TupleRepr (a) = Repr.Tuple [R a]
+ TupleRepr (a, b) = Repr.Tuple [R a, R b]
+ TupleRepr (a, b, c) = Repr.Tuple [R a, R b, R c]
+ TupleRepr (a, b, c, d) = Repr.Tuple [R a, R b, R c, R d]
+ TupleRepr (a, b, c, d, e) = Repr.Tuple [R a, R b, R c, R d, R e]
+ TupleRepr (a, b, c, d, e, f) = Repr.Tuple [R a, R b, R c, R d, R e, R f]
+ TupleRepr (a, b, c, d, e, f, g) = Repr.Tuple [R a, R b, R c, R d, R e, R f, R g]
+ TupleRepr (a, b, c, d, e, f, g, h) = Repr.Tuple [R a, R b, R c, R d, R e, R f, R g, R h]
+ TupleRepr (a, b, c, d, e, f, g, h, i) = Repr.Tuple [R a, R b, R c, R d, R e, R f, R g, R h, R i]
+ TupleRepr (GHC.MkSolo a) = Repr.Tuple [R a]
+
+-- TODO: Rename so that it doesn't have a # in the name.
+type Tuple# :: forall {k}. forall (a :: k) -> Type @(TupleRepr a)
+type family Tuple# _ where
+ Tuple# () = GHC.Tuple0#
+ Tuple# (a) = GHC.Tuple1# a
+ Tuple# (a, b) = GHC.Tuple2# a b
+ Tuple# (a, b, c) = GHC.Tuple3# a b c
+ Tuple# (a, b, c, d) = GHC.Tuple4# a b c d
+ Tuple# (a, b, c, d, e) = GHC.Tuple5# a b c d e
+ Tuple# (a, b, c, d, e, f) = GHC.Tuple6# a b c d e f
+ Tuple# (a, b, c, d, e, f, g) = GHC.Tuple7# a b c d e f g
+ Tuple# (a, b, c, d, e, f, g, h) = GHC.Tuple8# a b c d e f g h
+ Tuple# (a, b, c, d, e, f, g, h, i) = GHC.Tuple9# a b c d e f g h i
+ Tuple# (GHC.MkSolo a) = GHC.Tuple1# a
+
+type Tuple :: forall {k}. k -> Type
+type family Tuple _ where
+ Tuple () = GHC.Tuple0
+ Tuple (a) = GHC.Tuple1 a
+ Tuple (a, b) = GHC.Tuple2 a b
+ Tuple (a, b, c) = GHC.Tuple3 a b c
+ Tuple (a, b, c, d) = GHC.Tuple4 a b c d
+ Tuple (a, b, c, d, e) = GHC.Tuple5 a b c d e
+ Tuple (a, b, c, d, e, f) = GHC.Tuple6 a b c d e f
+ Tuple (a, b, c, d, e, f, g) = GHC.Tuple7 a b c d e f g
+ Tuple (a, b, c, d, e, f, g, h) = GHC.Tuple8 a b c d e f g h
+ Tuple (a, b, c, d, e, f, g, h, i) = GHC.Tuple9 a b c d e f g h i
+ Tuple (GHC.MkSolo a) = GHC.Tuple1 a
diff --git a/src/Lude/Kind.hs b/src/Lude/Kind.hs
@@ -1,152 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-
-module Lude.Kind (
- Kind,
- (:~:) (..),
- (:~~:) (..),
- type (~),
- type (~~),
- --
- Type,
- TypeL,
- TypeU,
- Type1,
- --
- Constraint,
- ConstraintL,
- ConstraintU,
- Constraint1,
- Predicate,
- Relation,
- --
- Lev,
- Endo,
- BiEndo,
- Cat,
-) where
-
-import Data.Tuple.Experimental qualified as GHC
-import Data.Type.Equality ((:~:) (..), (:~~:) (..), type (~), type (~~))
-import GHC.Exts qualified as GHC
-
-import Lude.Repr (Repr)
-import Lude.Repr qualified as Repr
-
---------------------------------------------------------------------------------
-
-type Kind = GHC.TYPE Repr.BoxL
-
--- | The kind of "invisibly" `Repr`-generic things
-type KindR :: Kind
-type KindR = forall (r :: Repr). Kind
-
---------------------------------------------------------------------------------
-
-type Type :: KindR
-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 Fam :: Kind -> KindR
--- type Fam i @r = i -> Type @r
-
--- TODO: What's this for? I forget.
-type AnyType :: Kind
-data AnyType = forall (r :: Repr). MkAnyType (Type @r)
-
---------------------------------------------------------------------------------
-
-type Constraint :: forall (r :: Repr). Kind
-type Constraint @r = GHC.CONSTRAINT r
-
-type ConstraintL = Constraint @Repr.BoxL
-type ConstraintU = Constraint @Repr.BoxU
-
--- TODO: Delete in favor of Predicate? We'd also need a replacement name for
--- Type1.
-type Constraint1 :: Kind -> forall (r :: Repr). Kind
-type Constraint1 k @r = Predicate k @r
-
-type Predicate :: Kind -> forall (r :: Repr). Kind
-type Predicate k @r = k -> Constraint @r
-
-type Relation :: Kind -> Kind -> forall (r :: Repr). Kind
-type Relation k l @r = k -> l -> Constraint @r
-
---------------------------------------------------------------------------------
-
--- | Transparently box a type of any representation
---
--- Use `Lev` to declare unlifted values at the top-level. For example, for any
--- @r :: Repr@, @A :: Type r@, and @bar :: A@:
--- @
--- foo :: Lev A
--- foo = bar
--- @
-type Lev :: forall {r :: Repr}. Type @r -> Type
-type Lev a = (GHC.CTuple0 :: ConstraintL) => a
-
-type Endo :: Kind -> Kind
-type Endo k = k -> k
-
-type BiEndo :: Kind -> Kind
-type BiEndo k = k -> k -> k
-
-type Cat :: Kind -> Kind
-type Cat i = i -> i -> Type
-
---------------------------------------------------------------------------------
--- Defunctionalization
-
--- TODO: All this is tentative. It's mostly for functors which aren't determined
--- by their object map.
-
--- | An empty kind with a phantom kind index, used to make @T k@ opaque
-type T' :: Kind -> Kind
-data T' k
-
--- | A type expression (of a given kind)
-type T :: Kind -> Kind
-type T k = T' k -> Kind
-
-type Splice :: forall {k}. T k -> k
-type family Splice _
-
-data Quote :: forall {k}. k -> T k
-type instance Splice (Quote a) = a
-
--- | Defunctionalized @(->)@
-type (-->) :: Kind -> Kind -> Kind
-type k --> l = k -> T l
-
-infixr 1 -->
-
-type Apply :: forall {k} {l}. (k --> l) -> k -> l
-type Apply f a = Splice (f a)
-
-type (@@) :: forall {k} {l}. (k --> l) -> k -> l
-type f @@ a = Apply f a
-infixl 7 @@
-
-type Defun = Defun1
-data Defun1 :: forall k0 k. (k0 -> k) -> (k0 --> k)
-type instance Splice (Defun1 f a) = f a
-
-data Defun2 :: forall k0 k1 k. (k0 -> k1 -> k) -> (k0 --> k1 --> k)
-type instance Splice (Defun2 f a) = Defun1 (f a)
-
-data Defun3 :: forall k0 k1 k2 k. (k0 -> k1 -> k2 -> k) -> (k0 --> k1 --> k2 --> k)
-type instance Splice (Defun3 f a) = Defun2 (f a)
-
-data Defun4 :: forall k0 k1 k2 k3 k. (k0 -> k1 -> k2 -> k3 -> k) -> (k0 --> k1 --> k2 --> k3 --> k)
-type instance Splice (Defun4 f a) = Defun3 (f a)
-
-type Ident :: forall {k}. k --> k
-type Ident = Quote
-
-data Compose :: forall {k} {l} {m}. (l --> m) -> (k --> l) -> (k --> m)
-type instance Splice (Compose f g x) = Splice (f (Splice (g x)))
diff --git a/src/Lude/Pair.hs b/src/Lude/Pair.hs
@@ -14,52 +14,12 @@ module Lude.Pair (
Snd,
) where
-import GHC.Exts qualified as GHC
-import Lude.Bool
-import Lude.Kind
-import Lude.Repr (Repr)
-import Lude.Repr qualified as Repr
-import Prelude qualified
+import Lude.Haskell
import Prelude.Experimental qualified as GHC
-- TODO: Generalize fst and snd (and fst1 and snd1?) with Cartesian class.
-- Probably name them outl and outr for symmetry with inl and inr.
-type HType :: Kind
-data HType = forall (r :: Repr). HType (Type @r)
-
-type HRepr :: HType -> Repr
-type family HRepr _ where
- HRepr ('HType @r _) = r
-
-type UnHType :: forall (h :: HType) -> Type @(HRepr h)
-type family UnHType _ where
- UnHType ('HType a) = a
-
-type ProdRepr :: GHC.List HType -> Repr
-type family ProdRepr _ where
- ProdRepr [] = GHC.TupleRep []
- ProdRepr (h : hs) = GHC.TupleRep [HRepr h, ProdRepr hs]
-
-type Prod :: forall (hs :: GHC.List HType) -> Type @(ProdRepr hs)
-type family Prod _ where
- Prod [] = GHC.Tuple0#
-
--- Prod (x ': xs) = (# UnHType x, Prod xs #)
-
-type Cool :: Type @(Repr.Tuple [Repr.Int, Repr.Tuple [Repr.BoxL, Repr.Tuple []]])
-type Cool = Prod ['HType GHC.Int#, 'HType GHC.Unit]
-
-type Tup :: GHC.List Type -> Type
-type family Tup _ where
- Tup [] = GHC.Tuple0
- Tup [a] = GHC.Tuple1 a
-
--- 1. "raw" tuples (various arity); "raw" sums (various arity)
--- 2. "semantic" types implemented with those (Either, Both, etc.)
-
-data Shape = Shape Bool Bool Bool Bool
-
--------------------------------------------------------------------------------
type Pair :: Type -> Type -> Type
diff --git a/src/Lude/Repr.hs b/src/Lude/Repr.hs
@@ -1,88 +0,0 @@
-module Lude.Repr (
- Levity (..),
- Repr,
- Tuple,
- Sum,
- Box,
- BoxL,
- BoxU,
- Addr,
- Int,
- Int8,
- Int16,
- Int32,
- Int64,
- Nat,
- Nat8,
- Nat16,
- Nat32,
- Nat64,
- Flt32,
- Flt64,
-) where
-
-import GHC.Exts (Levity (..))
-import GHC.Exts qualified as GHC
-
--- TODO: SIMD
-
--- TODO: Export patterns? (Non-exhaustive until we add SIMD support.)
-
---------------------------------------------------------------------------------
-
-type Repr = GHC.RuntimeRep
-
-type Tuple = GHC.TupleRep
-type Sum = GHC.SumRep
-type Box = GHC.BoxedRep
-type BoxL = GHC.BoxedRep Lifted
-type BoxU = GHC.BoxedRep Unlifted
-type Addr = GHC.AddrRep
-type Int = GHC.IntRep
-type Int8 = GHC.Int8Rep
-type Int16 = GHC.Int16Rep
-type Int32 = GHC.Int32Rep
-type Int64 = GHC.Int64Rep
-type Nat = GHC.WordRep
-type Nat8 = GHC.Word8Rep
-type Nat16 = GHC.Word16Rep
-type Nat32 = GHC.Word32Rep
-type Nat64 = GHC.Word64Rep
-type Flt32 = GHC.FloatRep
-type Flt64 = GHC.DoubleRep
-
---------------------------------------------------------------------------------
-
--- pattern Tuple :: [Repr] -> Repr
--- pattern Tuple rs = GHC.TupleRep rs
-
--- pattern Sum :: [Repr] -> Repr
--- pattern Sum rs = GHC.SumRep rs
-
--- pattern Box :: Levity -> Repr
--- pattern Box l = GHC.BoxedRep l
-
--- pattern BoxL, BoxU :: Repr
--- pattern BoxL = Box Lifted
--- pattern BoxU = Box Unlifted
-
--- pattern Addr :: Repr
--- pattern Addr = GHC.AddrRep
-
--- pattern Int, Int8, Int16, Int32, Int64 :: Repr
--- pattern Int = GHC.IntRep
--- pattern Int8 = GHC.Int8Rep
--- pattern Int16 = GHC.Int16Rep
--- pattern Int32 = GHC.Int32Rep
--- pattern Int64 = GHC.Int64Rep
-
--- pattern Nat, Nat8, Nat16, Nat32, Nat64 :: Repr
--- pattern Nat = GHC.WordRep
--- pattern Nat8 = GHC.Word8Rep
--- pattern Nat16 = GHC.Word16Rep
--- pattern Nat32 = GHC.Word32Rep
--- pattern Nat64 = GHC.Word64Rep
-
--- pattern Flt32, Flt64 :: Repr
--- pattern Flt32 = GHC.FloatRep
--- pattern Flt64 = GHC.DoubleRep
