lude

Haskell prelude alternative
git clone git://git.rr3.xyz/lude | git clone gits://git.rr3.xyz/lude
Log | Files | Refs | README | LICENSE

Category.hs (2816B)

      1 --------------------------------------------------------------------------------
      2 
      3 -- type Prod :: forall i j. Cat i -> Cat j -> Cat (i × j)
      4 -- data Prod p q a b where
      5 --     Prod :: p a0 b0 -> q a1 b1 -> Prod p q (a0, a1) (b0, b1)
      6 
      7 -- -- We could simplify this, but this way it's consistent with SumObj.
      8 -- type ProdObj :: forall i j. Cat i -> Cat j -> Constraint1 (i × j)
      9 -- class ProdObj p q a where
     10 --     prodObj :: Pair1 (Evidence1 (Obj p)) (Evidence1 (Obj q)) a
     11 -- instance (Obj p i, Obj q j) => ProdObj p q (i, j) where
     12 --     prodObj = Pair1 Evidence1 Evidence1
     13 
     14 -- instance (Categorical p, Categorical q) => Categorical (Prod p q) where
     15 --     type Obj (Prod p q) = ProdObj p q
     16 --     identity @a = case prodObj @_ @_ @p @q @a of
     17 --         Pair1 Evidence1 Evidence1 -> Prod identity identity
     18 --     compose (Prod f0 f1) (Prod g0 g1) = Prod (compose f0 g0) (compose f1 g1)
     19 
     20 --------------------------------------------------------------------------------
     21 
     22 -- type Sum :: forall i j. Cat i -> Cat j -> Cat (i + j)
     23 -- data Sum p q a b where
     24 --     SumL :: p a b -> Sum p q (L a) (L b)
     25 --     SumR :: q a b -> Sum p q (R a) (R b)
     26 
     27 -- type SumObj :: forall i j. Cat i -> Cat j -> Constraint1 (i + j)
     28 -- class SumObj p q a where
     29 --     sumObj :: Either1 (Evidence1 (Obj p)) (Evidence1 (Obj q)) a
     30 -- instance (Obj p a) => SumObj p q (L a) where
     31 --     sumObj = L1 Evidence1
     32 -- instance (Obj q a) => SumObj p q (R a) where
     33 --     sumObj = R1 Evidence1
     34 
     35 -- instance (Categorical p, Categorical q) => Categorical (Sum p q) where
     36 --     type Obj (Sum p q) = SumObj p q
     37 --     identity @a = case sumObj @_ @_ @p @q @a of
     38 --         L1 Evidence1 -> SumL identity
     39 --         R1 Evidence1 -> SumR identity
     40 --     compose (SumL f) (SumL g) = SumL (compose f g)
     41 --     compose (SumR f) (SumR g) = SumR (compose f g)
     42 
     43 --------------------------------------------------------------------------------
     44 
     45 -- type Iso :: forall {k}. Cat k -> Cat k
     46 -- data Iso p a b = Iso (p a b) (p b a)
     47 
     48 -- type Representable :: forall {i} r. (i -> Type @r) -> Constraint
     49 -- class (Functorial f, Obj (Dom f) (ReprObj f)) => Representable (f :: i -> Type) where
     50 --     type ReprObj f :: i
     51 --     represent :: forall (a :: i). f a -> Dom f a (ReprObj f)
     52 
     53 --------------------------------------------------------------------------------
     54 
     55 -- type Either :: Biendo Type
     56 -- data Either a b = L a | R b
     57 
     58 -- instance forall a. Functorial (Either a) where
     59 --     map f = \case
     60 --         L x -> L x
     61 --         R y -> R (f y)
     62 
     63 -- instance Functorial Either where
     64 --     type Dom Either = Function
     65 --     type Cod Either = Function ==> Function
     66 --     map f = Naturally \case
     67 --         L x -> L (f x)
     68 --         R y -> R y
     69 
     70 -- foo :: (a -> b) -> Either c a -> Either c b
     71 -- foo :: (a -> b) -> Nt Function Function (Either a) (Either b)
     72 -- foo f = map f