Algebra.hs (4975B)
1 module Lude.Algebra.Category.Algebra ( 2 Algebra, 3 Algebraic (..), 4 AlgebraicOn, 5 wrap_default, 6 -- 7 Recursive (..), 8 cata_defaultFunction, 9 cata_defaultNT, 10 -- 11 Coalgebra, 12 Coalgebraic (..), 13 CoalgebraicOn, 14 peel_default, 15 -- 16 Corecursive (..), 17 ana_defaultFunction, 18 ana_defaultNT, 19 ) where 20 21 import Lude.Algebra.Category.Core 22 import Lude.Haskell 23 24 -- TODO: Check whether we really need a separate default instance for NT. 25 -- I think it's necessary, because composition with `map h` forces eager 26 -- evaluation of h. 27 28 -- TODO: Eilenberg-Moore (co)algebras? 29 30 -------------------------------------------------------------------------------- 31 32 -- | An algebra for an endofunctor 33 type Algebra :: forall {i}. Endo i -> i -> Type 34 type Algebra f a = Dom f (f a) a 35 36 -- | A type equipped with a canonical algebra for an endofunctor 37 type Algebraic :: forall {i}. Endo i -> i -> Constraint 38 class (Endofunctorial f) => Algebraic (f :: Endo i) (a :: i) | a -> f where 39 wrap :: Algebra f a 40 41 type AlgebraicOn :: forall {i}. Cat i -> Endo i -> i -> Constraint 42 class (Algebraic f a, Dom f ~ p) => AlgebraicOn p f a 43 instance (Algebraic f a, Dom f ~ p) => AlgebraicOn p f a 44 45 -- | Default: @wrap = ana (map peel)@ 46 wrap_default :: forall {i} (f :: Endo i) (a :: i). (Corecursive f a) => Algebra f a 47 wrap_default = ana (map peel) 48 49 -------------------------------------------------------------------------------- 50 51 -- | A type @r@ equipped with an initial algebra @wrap@ for an endofunctor @f@ 52 -- 53 -- Laws: 54 -- - __@r@ is an initial @f@-algebra:__ for all @f@-algebras @a@, 55 -- @cata a@ is an @f@-algebra homomorphism from @r@ to @a@ 56 -- (i.e., @cata a . wrap = a . map (cata a)@) and unique with this property 57 -- - __@peel@ is the inverse of @wrap@:__ @peel . wrap = identity@ (at @f r@) 58 -- and @wrap . peel = identity@ (at @r@) (cf., Lambek's theorem) 59 type Recursive :: forall {i}. Endo i -> i -> Constraint 60 class (Algebraic f r, Coalgebraic f r) => Recursive (f :: Endo i) (r :: i) where 61 cata :: forall (a :: i). Algebra f a -> Dom f r a 62 63 type DefaultCata :: forall {i}. Endo i -> i -> Type 64 type DefaultCata f r = (Algebraic f r, Coalgebraic f r) => forall a. Algebra f a -> Dom f r a 65 66 -- | Default: @cata f = f . map (cata f) . peel@ 67 cata_defaultFunction 68 :: forall (f :: Endo Type) r 69 . (Dom f ~ Function) => DefaultCata f r 70 cata_defaultFunction a = h where h = a . map h . peel 71 72 -- | Default: @cata f = f . map (cata f) . peel@ (modulo laziness) 73 cata_defaultNT 74 :: forall {i} {j} (p :: Cat i) (q :: Cat j) (f :: Endo (i -> j)) r 75 . (Categorical p, Categorical q, Dom f ~ NT p q) => DefaultCata f r 76 cata_defaultNT a@(Naturally _) = h where h = Naturally (comp a . comp (map h) . comp peel) \\ witnessMor (wrap @f @r) 77 78 -------------------------------------------------------------------------------- 79 80 -- | A coalgebra for an endofunctor 81 type Coalgebra :: forall {i}. Endo i -> i -> Type 82 type Coalgebra g b = Dom g b (g b) 83 84 -- | A type equipped with a canonical coalgebra for an endofunctor 85 type Coalgebraic :: forall {i}. Endo i -> i -> Constraint 86 class (Endofunctorial g) => Coalgebraic (g :: Endo i) (b :: i) | b -> g where 87 peel :: Coalgebra g b 88 89 type CoalgebraicOn :: forall {i}. Cat i -> Endo i -> i -> Constraint 90 class (Coalgebraic g b, Dom g ~ p) => CoalgebraicOn p g b 91 instance (Coalgebraic g b, Dom g ~ p) => CoalgebraicOn p g b 92 93 -- | Default: @peel = cata (map wrap)@ 94 peel_default :: forall {i} (g :: Endo i) (b :: i). (Recursive g b) => Coalgebra g b 95 peel_default = cata (map wrap) 96 97 -------------------------------------------------------------------------------- 98 99 -- | A type @s@ equipped with a terminal coalgebra @peel@ for an endofunctor @g@ 100 -- 101 -- Laws: 102 -- - __@s@ is a terminal @g@-coalgebra:__ for all @g@-coalgebras @b@, 103 -- @ana b@ is a @g@-coalgebra homomorphism from @b@ to @s@ 104 -- (i.e., @map (ana b) . b = peel . ana b@) and unique with this property 105 -- - __@wrap@ is the inverse of @peel@:__ @peel . wrap = identity@ (at @g s@) 106 -- and @wrap . peel = identity@ (at @s@) (cf., Lambek's theorem) 107 type Corecursive :: forall {i}. Endo i -> i -> Constraint 108 class (Algebraic g s, Coalgebraic g s) => Corecursive (g :: Endo i) (s :: i) where 109 ana :: forall (b :: i). Coalgebra g b -> Dom g b s 110 111 type DefaultAna :: forall {i}. Endo i -> i -> Type 112 type DefaultAna g s = (Coalgebraic g s, Algebraic g s) => forall b. Coalgebra g b -> Dom g b s 113 114 -- | Default: @ana g = wrap . map (ana g) . g@ 115 ana_defaultFunction 116 :: forall (g :: Endo Type) s 117 . (Dom g ~ Function) => DefaultAna g s 118 ana_defaultFunction b = h where h = wrap . map h . b 119 120 -- | Default: @ana g = wrap . map (ana g) . g@ (modulo laziness) 121 ana_defaultNT 122 :: forall {i} {j} (p :: Cat i) (q :: Cat j) (g :: Endo (i -> j)) s 123 . (Categorical p, Categorical q, Dom g ~ NT p q) => DefaultAna g s 124 ana_defaultNT b@(Naturally _) = h where h = Naturally (comp wrap . comp (map h) . comp b) \\ witnessMor (peel @g @s)