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