Binary-tree zippers with type witnesses of position in tree

Truffula.hs

{-# LANGUAGE GADTs          #-}
{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE KindSignatures #-}

module Truffula where

data Path = LeftOf Path | RightOf Path | Root

data Tree (p :: Path) a where
   Tree :: { value  :: a
           , thread :: Thread p a
           , left   :: Tree (LeftOf  p) a
           , right  :: Tree (RightOf p) a
           } -> Tree p a

data Thread (p :: Path) a where
   WentLeft  :: Tree (LeftOf  p) a -> Thread p a -> Thread (LeftOf  p) a
   WentRight :: Tree (RightOf p) a -> Thread p a -> Thread (RightOf p) a
   StartedAt :: Tree Root a -> Thread Root a

up :: Thread (p r) a -> Thread r a
up (WentLeft  _ t) = t
up (WentRight _ t) = t
up _               = error "Impossible: can't go up from the root" -- exhaustiveness checking faulty

tree :: Thread p a -> Tree p a
tree (WentLeft  t _) = t
tree (WentRight t _) = t
tree (StartedAt t)   = t

unfold :: (a -> a) -> (a -> a) -> a -> Tree Root a
unfold leftFun rightFun seed = parent
   where parent = unfoldWithThread (StartedAt parent) leftFun rightFun seed

unfoldWithThread :: Thread p a -> (a -> a) -> (a -> a) -> a -> Tree p a
unfoldWithThread seedThread leftFun rightFun seed = parent
   where parent = Tree seed seedThread leftChild rightChild
         leftChild  = unfoldWithThread (WentLeft  leftChild  seedThread) leftFun rightFun (leftFun seed)
         rightChild = unfoldWithThread (WentRight rightChild seedThread) leftFun rightFun (rightFun seed)

Note that these aren't actually zippers; they don't permit in-place modification of the tree structure.