Skip to content

Instantly share code, notes, and snippets.

@plaidfinch
Created July 12, 2014 19:08
Show Gist options
  • Save plaidfinch/2d402bb9d10d4050fc44 to your computer and use it in GitHub Desktop.
Save plaidfinch/2d402bb9d10d4050fc44 to your computer and use it in GitHub Desktop.
Binary-tree zippers with type witnesses of position in tree
{-# 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)
@plaidfinch
Copy link
Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment