htree: heterogeneous rose tree

This library implements a heterogeneous rose-tree (HTree) that is indexed by a type-level rosetree (TyTree).

It also offers some useful functions, highlights include:

• searching in the tree and creating evidence on the term-level via typeclasses
• record-dot syntax for accessing elements in the tree.
• mapping and traversing trees

to develop

• with direnv: direnv allow
• only with nix: nix develop
• to run all checks: nix flake check -Lv systems configurations
• build with nix nix build (or on ghc96, nix build .#ghc96-htree)
• documentation in the form of continuously deployed haddock can be found at mangoiv.srht.site

example

pattern I :: forall a. a -> Identity a
pattern I a = Identity a

-- the type that the tree is going to be indexed by
type Ex =
  TyNode Int
   [ TyNode Int
       [ TyNode Int '[]
       , TyNode Bool '[]
       , TyNode String '[ TyNode Int '[]]
       ]
    , TyNode Int '[]
    ]

-- we create an HTree of the example type 'Ex'
ex :: HTree Identity Ex
ex =
  HNode 5 do
    HNode 12 do
      HNode 13 HNil
        ::: HNode (I False) HNil
        ::: HNode "test" (HNode 9 HNil ::: HNil)
        ::: HNil
      ::: HNode 43 HNil
      ::: HNil
    

-- we can create a labeled Tree and search via DFS and BFS in it
-- the search happens on the type-level
type LabeledTree = TyNodeL "top" Int
  [ TyNodeL "inter" Int '[ TyNodeL "foo" Int '[] ]
  , TyNodeL "foo" Int '[]
  ]

-- >>> getElem @'DFS @"foo" @Int Proxy labeledTree
-- Identity 69
-- >>> getElem @'BFS @"foo" @Int Proxy labeledTree
-- Identity 67
labeledTree :: HTree Identity LabeledTree
labeledTree = 42 `HNodeL` HNodeL 4 (HNodeL 69 HNil ::: HNil) ::: HNodeL 67 HNil ::: HNil