0 | module Data.Functor.Algebra
  1 |
  2 | import Data.Vect
  3 |
  4 | import Data.Trees
  5 | import Misc
  6 |
  7 | {-------------------------------------------------------------------------------
  8 | {-------------------------------------------------------------------------------
  9 | This file defines the Algebra interface, which is a pragmatic implementation of
 10 | the concept of F-algebra from category theory.
 11 |
 12 | It is pragmatic since it is not defined for an arbitrary category, but rather
 13 | for the (vaguely defined) category of Idris types and functions.
 14 |
 15 | Instantiating it for 'other' categories is solved by exposing the carrier of the algebra at the type level, as it allow us to use interface constraints to specify the constraints on the carrier.
 16 | This comes at the cost of needing to specify the carrier type explicitly at
 17 | every call site.
 18 | -------------------------------------------------------------------------------}
 19 | -------------------------------------------------------------------------------}
 20 |
 21 | ||| Generalised sum operation
 22 | ||| Categorically, an F-Algebra
 23 | public export
 24 | interface Algebra (f : Type -> Type) (0 carrier : Type)where
 25 |   constructor MkAlgebra
 26 |   reduce : f carrier -> carrier
 27 |
 28 | ||| In many instances below, we assume Num a defines a Rig structure on a
 29 | ||| This means we assume the sum operation is both commutative and associative,
 30 | ||| allowing us to define the Algebra instance for trees without any additional
 31 | ||| assumptions, for instance (TODO unpack why)
 32 | namespace Instances
 33 |   public export
 34 |   Num a => Algebra List a where
 35 |     reduce = foldr (+) (fromInteger 0)
 36 |
 37 |   -- Does this work for any Applicative? I think not, because in trees we have to choose an order of summation. But that might not impact things?
 38 |   -- if the sum operation is commutative, then it should not impact things
 39 |   public export
 40 |   {n : Nat} -> Num a => Algebra (Vect n) a where
 41 |     reduce = foldr (+) (fromInteger 0)
 42 |   
 43 |   ||| Summing up leaves of a tree given by the Num a structure
 44 |   ||| This assumes that Num a is a Rig structure, meaning the sum operation is
 45 |   ||| assumed to be both commutative and associative.
 46 |   ||| Otherwise we would need to be expose the data of the ordering and 
 47 |   ||| bracketing by which the summation below was performed
 48 |   public export
 49 |   Num a => Algebra BinTreeLeaf a where
 50 |     reduce (Leaf leaf) = leaf
 51 |     reduce (Node _ leftTree rightTree)
 52 |       = (reduce {f=BinTreeLeaf} leftTree) + 
 53 |         (reduce {f=BinTreeLeaf} rightTree)
 54 |   
 55 |   ||| Summing up nodes of a tree given by the Num a structure
 56 |   ||| This assumes that Num a is a Rig structure, meaning the sum operation is
 57 |   ||| assumed to be both commutative and associative.
 58 |   ||| Otherwise we would need to be expose the data of the ordering and 
 59 |   ||| bracketing by which the summation below was performed
 60 |   public export
 61 |   Num a => Algebra BinTreeNode a where
 62 |     reduce (Leaf _) = fromInteger 0
 63 |     reduce (Node node leftTree rightTree)
 64 |        = node + (reduce {f=BinTreeNode} leftTree)
 65 |               + (reduce {f=BinTreeNode} rightTree)
 66 |   
 67 |   ||| Summing up nodes and leaves of a tree given by the Num a structure
 68 |   ||| This assumes that Num a is a Rig structure, meaning the sum operation is
 69 |   ||| assumed to be both commutative and associative.
 70 |   ||| Otherwise we would need to be expose the data of the ordering and 
 71 |   ||| bracketing by which the summation below was performed
 72 |   public export
 73 |   Num a => Algebra BinTreeSame a where
 74 |     reduce (Leaf leaf) = leaf
 75 |     reduce (Node node leftTree rightTree)
 76 |       = node + (reduce {f=BinTreeSame} leftTree)
 77 |             + (reduce {f=BinTreeSame} rightTree)
 78 |   
 79 |   -- public export
 80 |   -- [usualSum] Num a => Applicative f => Algebra BinTreeSame (f a) where
 81 |   --   reduce (Leaf leaf) = leaf
 82 |   --   reduce (Node node leftTree rightTree)
 83 |   --     = let lt = reduce {f=BinTreeSame} leftTree 
 84 |   --           rt = reduce {f=BinTreeSame} rightTree
 85 |   --       in (uncurry (+)) <$> (liftA2 lt rt) 
 86 |   
 87 |   -- can be simplified by uncommenting the Num (f a) instance in Num.idr
 88 |   public export
 89 |   [usualSumLeaf] Num a => Applicative f => Algebra BinTreeLeaf (f a) where
 90 |     reduce (Leaf leaf) = leaf
 91 |     reduce (Node node leftTree rightTree)
 92 |       = let lt = reduce {f=BinTreeLeaf} leftTree 
 93 |             rt = reduce {f=BinTreeLeaf} rightTree
 94 |         in (uncurry (+)) <$> (liftA2 lt rt) 
 95 |   
 96 |   
 97 |   public export covering
 98 |   Num a => Algebra RoseTreeSame a where
 99 |     reduce (Leaf x) = x
100 |     reduce (Node x subTrees)
101 |       = x + reduce ((reduce {f=RoseTreeSame}) <$> subTrees)
102 |
103 |
104 |   -- public export
105 |   -- [appSum] {shape : Vect n Nat} -> 
106 |   -- Num a => Applicative f =>
107 |   -- Algebra (TensorA shape) (f a) using applicativeNum where
108 |   --   reduce (TZ val) = val
109 |   --   reduce (TS xs) = reduce (reduce <$> xs)
110 |   -- 
111 |   -- aa : Algebra (TensorA [2]) (TensorA [3] a) => a
112 |
113 |
114 | namespace Initial
115 |   ||| Initial algebra for an endofunctor
116 |   ||| Can we make it total by using containers, i.e. strictly positive functors?
117 |   public export covering
118 |   data Initial : (f : Type -> Type) -> Type where
119 |     ||| One part of the isomorphism
120 |     In : f (Initial f) -> Initial f
121 |   
122 |   ||| Second part of the isomorphism 
123 |   public export
124 |   Out : Initial f -> f (Initial f)
125 |   Out (In r) = r
126 |   
127 |   public export covering
128 |   cata : Functor f =>
129 |     Algebra f a -> (Initial f -> a)
130 |   cata (MkAlgebra g) rs = g $ cata (MkAlgebra g) <$> Out rs 
131 |
132 |
133 | namespace Final
134 |   public export covering
135 |   data Final : (f : Type -> Type) -> Type where
136 |     MkFinal : f (Inf (Final f)) -> Final f
137 |
138 |   ||| For some reason, inlining this function in `ana` causes a compiler error
139 |   public export covering
140 |   embedFinal : Final f -> Inf (Final f)
141 |   embedFinal x = x
142 |
143 |   public export covering
144 |   ana : Functor f =>
145 |     (a -> f a) -> a -> Final f
146 |   ana next seed = MkFinal $ (embedFinal . ana next) <$> next seed