commit 581a05b0802017cb1c3d34a2e9d73feddb9a4039
parent a8877191187dc9bc99ce0dba251579d521cd89b6
Author: Robert Russell <robert@rr3.xyz>
Date: Thu, 3 Sep 2026 00:13:21 -0700
WIP
Diffstat:
5 files changed, 134 insertions(+), 10 deletions(-)
diff --git a/src/Lude/Algebra.hs b/src/Lude/Algebra.hs
@@ -11,7 +11,7 @@ module Lude.Algebra (
import Data.Set (Set)
import Data.Set qualified as Set
-import Prelude (Eq, Ord)
+import Prelude (Ord)
import Lude.Kind
import Lude.Repr (Repr)
diff --git a/src/Lude/Algebra/Category.hs b/src/Lude/Algebra/Category.hs
@@ -13,7 +13,9 @@ import Lude.Kind
import Lude.Pair
-- TODO: Semicategory
+
-- TODO: Allow non-BoxL morphism Repr?
+
-- TODO: Filterable is functor from Kleisli Option to Hask
--------------------------------------------------------------------------------
@@ -38,15 +40,25 @@ instance Category Hask where
--------------------------------------------------------------------------------
+type Dual :: forall i. Cat i -> Cat i
+newtype Dual p a b = Dual (p b a)
+
+instance (Category p) => Category (Dual p) where
+ type Obj (Dual p) = Obj p
+ identity = Dual identity
+ compose (Dual f) (Dual g) = Dual (compose g f)
+
+--------------------------------------------------------------------------------
+
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)
+ 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
+instance (Obj p i, Obj q j) => ProdObj p q (i, j) where
prodObj = Pair1 Evidence1 Evidence1
instance (Category p, Category q) => Category (Prod p q) where
@@ -112,6 +124,9 @@ class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
map :: Dom f a b -> Cod f (f a) (f b)
+instance Functor (Pair b) where
+ map f (b, a) = (b, f a)
+
instance Functor (Either b) where
map _ (L b) = L b
map f (R a) = R (f a)
@@ -124,7 +139,12 @@ instance Functor (Either b) where
-- type Bifunctor :: forall i j k. (i -> j -> k) -> Constraint
-- class (Category (Bildom f), Category (Birdom f), Category (Bicod f)) => Bifunctor (f :: i -> j -> k) where
-- type Bildom f :: Cat i
+-- type Bildom f = DefaultCat
+
-- type Birdom f :: Cat j
+-- type Birdom f = DefaultCat
+
-- type Bicod f :: Cat k
+-- type Bicod f = DefaultCat
-- lmap :: Bildom f a b ->
diff --git a/src/Lude/Bool.hs b/src/Lude/Bool.hs
@@ -0,0 +1,9 @@
+module Lude.Bool (
+ Bool (..),
+) where
+
+import Data.Bool (Bool (..))
+
+-- TODO: Instances
+
+--------------------------------------------------------------------------------
diff --git a/src/Lude/Kind.hs b/src/Lude/Kind.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE UndecidableInstances #-}
+
module Lude.Kind (
Kind,
(:~:) (..),
@@ -42,6 +44,9 @@ type TypeU = Type @Repr.BoxU
type Type1 :: forall (r :: Repr). Kind -> Kind
type Type1 @r i = i -> Type @r
+type AnyType :: Kind
+data AnyType = forall (r :: Repr). MkAnyType (Type @r)
+
--------------------------------------------------------------------------------
type Constraint :: forall (r :: Repr). Kind
@@ -71,3 +76,51 @@ type Endo k = k -> k
type BiEndo :: Kind -> Kind
type BiEndo k = k -> k -> k
+
+--------------------------------------------------------------------------------
+
+-- | 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,14 +14,56 @@ 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.Experimental qualified as GHC
+import Prelude qualified
--- TODO: Generalize fst and snd (and fst1 and snd1?) with Cartesian class
+-- 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
-type Pair = (,)
+type Pair = GHC.Tuple2
-- For consistency
pattern Pair :: a -> b -> Pair a b
@@ -41,21 +83,21 @@ snd (Pair _ y) = y
type Pair1 :: forall i j. Type1 i -> Type1 j -> Type1 (i × j)
data Pair1 f g a where
- Pair1 :: f a0 -> g a1 -> Pair1 f g '(a0, a1)
+ Pair1 :: f a0 -> g a1 -> Pair1 f g (a0, a1)
type (×^) = Pair1
infixl 7 ×^
-fst1 :: Pair1 p q '(i, j) -> p i
+fst1 :: Pair1 p q (i, j) -> p i
fst1 (Pair1 x _) = x
-snd1 :: Pair1 p q '(i, j) -> q j
+snd1 :: Pair1 p q (i, j) -> q j
snd1 (Pair1 _ y) = y
--------------------------------------------------------------------------------
type family Fst (x :: i × j) :: i where
- Fst '(a, b) = a
+ Fst (a, b) = a
type family Snd (x :: i × j) :: j where
- Snd '(a, b) = b
+ Snd (a, b) = b
