0 | module Data.Tree
  1 |
  2 | import Language.Reflection
  3 | import Derive.Prelude
  4 |
  5 | import Misc
  6 |
  7 | %language ElabReflection
  8 |
  9 | {-----------------------------------------------------------
 10 | {-----------------------------------------------------------
 11 | This file contains definitions of many useful tree types.
 12 | These definitions are all inductive, representing finite
 13 | trees, and generally used as concrete representations of
 14 | tree containers.
 15 |
 16 | -----------------------------------------------------------}
 17 | -----------------------------------------------------------}
 18 |
 19 | namespace BinaryTrees
 20 |   ||| Finite binary trees with labels on leaves and nodes
 21 |   public export
 22 |   data BinTree : (leafType : Type) -> (nodeType : Type) -> Type where
 23 |       Leaf : leafType -> -- leaf value
 24 |         BinTree leafType nodeType
 25 |       Node : nodeType -> -- node value
 26 |         BinTree leafType nodeType -> -- left subtree
 27 |         BinTree leafType nodeType -> -- right subtree
 28 |         BinTree leafType nodeType
 29 |
 30 |   %runElab derive "BinTree" [Eq, Show]
 31 |   %name BinTree bt, bt', bt''
 32 |
 33 |
 34 |   -- public export
 35 |   -- {a, b : Type} -> Display a => Display b => Display (BinTree a b) where
 36 |   --   display (Leaf a) = display a
 37 |   --   display (Node b lt rt) =
 38 |   --     let dlt = display lt 
 39 |   --         drt = display rt 
 40 |   --         (bh ** bw ** bc) = display b
 41 |   --     in ?hmm_1
 42 |
 43 |   public export
 44 |   Bifunctor BinTree where
 45 |       bimap f g (Leaf x) = Leaf (f x)
 46 |       bimap f g (Node n leftTree rightTree)
 47 |         = Node (g n) (bimap f g leftTree) (bimap f g rightTree)
 48 |
 49 |   namespace BinTreeSame
 50 |     ||| Binary trees with the same type of value on both leaves and nodes
 51 |     public export
 52 |     BinTreeSame : (content : Type) -> Type
 53 |     BinTreeSame content = BinTree content content
 54 |
 55 |     public export
 56 |     Functor BinTreeSame where
 57 |       map f (Leaf x) = Leaf (f x)
 58 |       map f (Node x leftTree rightTree) = Node (f x)
 59 |         (map {f=BinTreeSame} f leftTree)
 60 |         (map {f=BinTreeSame} f rightTree)
 61 |
 62 |
 63 |     ||| Smaller tree expands to the shape of a bigger one
 64 |     ||| We can do this for BinTreeSame but not for BinTree precisely
 65 |     ||| because we copy the leaf value across to the nodes
 66 |     public export
 67 |     liftA2BinTreeSame : BinTreeSame a -> BinTreeSame b -> BinTreeSame (a, b)
 68 |     liftA2BinTreeSame (Leaf a) (Leaf b) = Leaf (a, b)
 69 |     liftA2BinTreeSame l@(Leaf a) (Node b ltb rtb)
 70 |       = Node (a, b) (liftA2BinTreeSame l ltb) (liftA2BinTreeSame l rtb)
 71 |     liftA2BinTreeSame (Node a lta rta) l@(Leaf b)
 72 |       = Node (a, b) (liftA2BinTreeSame lta l) (liftA2BinTreeSame rta l)
 73 |     liftA2BinTreeSame (Node a lta rta) (Node b ltb rtb)
 74 |       = Node (a, b) (liftA2BinTreeSame lta ltb) (liftA2BinTreeSame rta rtb)
 75 |
 76 |
 77 |     public export
 78 |     Applicative BinTreeSame where
 79 |       {-
 80 |       Maps a single value to a Leaf node with that value
 81 |       We can technically create an arbitrary tree with this, but 
 82 |       it's not clear whether any one except Leaf is canonical
 83 |       -}
 84 |       pure a = Leaf a
 85 |       fs <*> xs = map {f=BinTreeSame} (uncurry ($)) $ liftA2BinTreeSame fs xs
 86 |   
 87 |   
 88 |
 89 |   namespace LeavesOnly
 90 |     public export
 91 |     BinTreeLeaf : (leafType : Type) -> Type
 92 |     BinTreeLeaf leafType = BinTree leafType ()
 93 |
 94 |     ||| Helper function to construct a node with a trivial value
 95 |     public export
 96 |     Node' : BinTree l () -> BinTree l () -> BinTree l ()
 97 |     Node' = Node ()
 98 |   
 99 |     public export
100 |     Functor BinTreeLeaf where
101 |         map f (Leaf x) = Leaf (f x)
102 |         map f (Node x leftTree rightTree) = Node x
103 |           (map {f=BinTreeLeaf} f leftTree)
104 |           (map {f=BinTreeLeaf} f rightTree)
105 |   
106 |     public export
107 |     liftA2BinTreeLeaf : BinTreeLeaf a -> BinTreeLeaf b -> BinTreeLeaf (a, b)
108 |     liftA2BinTreeLeaf (Leaf a) (Leaf b)
109 |       = Leaf (a, b)
110 |     liftA2BinTreeLeaf l@(Leaf x) (Node () z w)
111 |       = Node () (liftA2BinTreeLeaf l z) (liftA2BinTreeLeaf l w)
112 |     liftA2BinTreeLeaf (Node () z w) (Leaf x)
113 |       = Node () (liftA2BinTreeLeaf z (Leaf x)) (liftA2BinTreeLeaf w (Leaf x))
114 |     liftA2BinTreeLeaf (Node () y z) (Node () v s)
115 |       = Node () (liftA2BinTreeLeaf y v) (liftA2BinTreeLeaf z s)
116 |   
117 |     public export
118 |     Applicative BinTreeLeaf where
119 |         pure x = Leaf x
120 |         fs <*> xs = map {f=BinTreeLeaf} (uncurry ($)) $ liftA2BinTreeLeaf fs xs 
121 |   
122 |     ||| This requires us traversing a tree in a linear order
123 |     ||| This means we have to make a choice on which subtree to process first
124 |     ||| Another way is to first implement a traversal of the tree, and
125 |     ||| then use that
126 |     public export
127 |     Foldable BinTreeLeaf where
128 |       foldr f z (Leaf leaf) = f leaf z
129 |       foldr f z (Node () leftTree rightTree) =
130 |         -- Process left first, i.e. fold right with z, then use that 
131 |         -- as accumulator for left
132 |         let rightResult = foldr {t=BinTreeLeaf} f z rightTree
133 |         in foldr {t=BinTreeLeaf} f rightResult leftTree
134 |   
135 |   namespace NodesOnly
136 |     public export
137 |     BinTreeNode : (nodeType : Type) -> Type
138 |     BinTreeNode nodeType = BinTree () nodeType
139 |
140 |     ||| Helper function to construct a leaf with a trivial value
141 |     public export
142 |     Leaf' : BinTree () n
143 |     Leaf' = Leaf ()
144 |   
145 |     public export
146 |     Functor BinTreeNode where
147 |       map f (Leaf leaf) = Leaf leaf
148 |       map f (Node node leftTree rightTree)
149 |         = Node (f node) (map {f=BinTreeNode} f leftTree) (map {f=BinTreeNode} f rightTree) 
150 |
151 |     {--
152 |     In general no applicative instance for a tree with values only on nodes.
153 |     Note that you can define the `pure` and `liftA2`, but they won't satisfy applicative laws.
154 |     See https://www.reddit.com/r/haskell/comments/cb1j40/comment/etct1xk/
155 |     --} 
156 |   
157 |   namespace Traversals
158 |     {- 
159 |          4
160 |         / \
161 |        2   5
162 |       /\
163 |      1  3
164 |     
165 |      -}
166 |     MyTree : BinTree Int Int
167 |     MyTree = Node 4 (Node 2 (Leaf 1) (Leaf 3)) (Leaf 5)
168 |   
169 |     public export
170 |     inorder : BinTree a b -> List (Either a b)
171 |     inorder (Leaf leaf) = [Left leaf]
172 |     inorder (Node node leftTree rightTree) =
173 |       inorder leftTree ++ [Right node] ++ inorder rightTree
174 |   
175 |     testInorder :
176 |       Traversals.inorder MyTree = [Left 1, Right 2, Left 3, Right 4, Left 5]
177 |     testInorder = Refl
178 |   
179 |     public export
180 |     preorder : BinTree a b -> List (Either a b)
181 |     preorder (Leaf leaf) = [Left leaf]
182 |     preorder (Node node leftTree rightTree) =
183 |       [Right node] ++ preorder leftTree ++ preorder rightTree
184 |   
185 |     testPreorder : Traversals.preorder MyTree 
186 |       = [Right 4, Right 2, Left 1, Left 3, Left 5]
187 |     testPreorder = Refl
188 |   
189 |     public export
190 |     postorder : BinTree a b -> List (Either a b)
191 |     postorder (Leaf leaf) = [Left leaf]
192 |     postorder (Node node leftTree rightTree)
193 |       = postorder leftTree ++ postorder rightTree ++ [Right node]
194 |   
195 |     testPostorder : Traversals.postorder MyTree 
196 |       = [Left 1, Left 3, Right 2, Left 5, Right 4]
197 |     testPostorder = Refl
198 |   
199 |     public export
200 |     fromEitherUnit : List (Either a ()) -> List a
201 |     fromEitherUnit [] = []
202 |     fromEitherUnit ((Left a) :: xs) = a :: fromEitherUnit xs
203 |     fromEitherUnit ((Right ()) :: xs) = fromEitherUnit xs
204 |   
205 |     public export
206 |     fromUnitEither : List (Either () a) -> List a
207 |     fromUnitEither [] = []
208 |     fromUnitEither ((Right a) :: xs) = a :: fromUnitEither xs
209 |     fromUnitEither ((Left ()) :: xs) = fromUnitEither xs
210 |   
211 |     ||| For leaf-only trees, inorder=preorder=postorder
212 |     public export
213 |     traverseBinTreeLeaf : BinTreeLeaf a -> List a
214 |     traverseBinTreeLeaf bt = fromEitherUnit (inorder bt)
215 |   
216 |   
217 |     public export
218 |     inorderNode : BinTreeNode a -> List a
219 |     inorderNode bt = fromUnitEither (inorder bt)
220 |   
221 |     public export
222 |     preorderNode : BinTreeNode a -> List a
223 |     preorderNode bt = fromUnitEither (preorder bt)
224 |   
225 |     public export
226 |     postorderNode : BinTreeNode a -> List a
227 |     postorderNode bt = fromUnitEither (postorder bt)
228 |
229 |
230 |
231 | namespace RoseTrees
232 |   ||| This can likely be generalised to work for an arbitrary applicative
233 |   ||| instead of just List
234 |   public export
235 |   data RoseTree : (leafType : Type) -> (nodeType : Type) -> Type where
236 |     Leaf : leafType -> -- leaf value
237 |       RoseTree leafType nodeType
238 |     Node : nodeType -> -- node value
239 |       List (RoseTree leafType nodeType) -> -- list of children
240 |       RoseTree leafType nodeType
241 |
242 |   %runElab derive "RoseTree" [Eq, Show]
243 |   %name RoseTree rt, rt', rt''
244 |
245 |
246 |   namespace RoseTreeSame
247 |     public export
248 |     RoseTreeSame : (content : Type) -> Type
249 |     RoseTreeSame content = RoseTree content content
250 |
251 |     public export
252 |     Functor RoseTreeSame where
253 |       map f (Leaf x) = Leaf (f x)
254 |       map f (Node x subTrees) = Node (f x) (map {f=RoseTreeSame} f <$> subTrees)
255 |
256 |     public export
257 |     liftA2RoseTreeSame : RoseTreeSame a -> RoseTreeSame b -> RoseTreeSame (a, b)
258 |     liftA2RoseTreeSame (Leaf a) (Leaf b) = Leaf (a, b)
259 |     liftA2RoseTreeSame l@(Leaf a) (Node b subTreesb)
260 |       = Node (a, b) ((\st => liftA2RoseTreeSame l st) <$> subTreesb)
261 |     liftA2RoseTreeSame (Node a subTreesa) l@(Leaf b)
262 |       = Node (a, b) ((\st => liftA2RoseTreeSame st l) <$> subTreesa)
263 |     -- For this last case we need to use a particular applicative structure of List! 
264 |     liftA2RoseTreeSame (Node a subTreesa) (Node b subTreesb)
265 |       = Node (a, b) ((uncurry liftA2RoseTreeSame) <$> (listZip subTreesa subTreesb))
266 |
267 |     ||| Making RoseTreeSame an applicative relies on the applicative structure of lists
268 |     public export
269 |     Applicative RoseTreeSame where
270 |       pure a = Leaf a
271 |       fs <*> xs = map {f=RoseTreeSame} (uncurry ($)) $ liftA2RoseTreeSame fs xs
272 |
273 |
274 |     public export
275 |     {a : Type} -> Display a => Display (RoseTreeSame a) where
276 |       display (Leaf x) = display x
277 |       display (Node x rts)
278 |         = let (xh ** xw ** dx) = display x 
279 |           in ?whatt_1
280 |
281 |   -- TODO RoseTreeLeaf, RoseTreeNode?
282 |
283 |   -- Idris' totality checker does not accept this as total
284 |   -- public export
285 |   -- Bifunctor RoseTree where
286 |   --   bimap f g (Leaf a) = Leaf (f a)
287 |   --   bimap f g (Node b subTrees) = Node (g b) (bimap f g <$> subTrees)
288 |
289 |
290 | --   public export
291 | --   Foldable (RoseTree leafType) where
292 | --     foldr f z (Leaf x) = f x z
293 | --     foldr f z (Node n children) = foldr {f=RoseTree leafType} f (foldr {f=RoseTree leafType} f z children) n
294 | -- 
295 |   
296 |   
297 |
298 |