# Zippered Tree

    data Path where
      Root  : () -> Path
      Left  : Path -> Path
      Right : Path -> Path

    codata Tree : Path -> * -> * where
      node    : Tree p a -> a
      left    : Tree p a -> Tree (Left p) a
      right   : Tree p a -> Tree (Right p) a
      unLeft  : Tree (Left p) a  -> Tree p a
      unRight : Tree (Right p) a -> Tree p a

    ones : Tree Root Int
    ones =
      merge e from
        node e  <- 1
        left e  <- l e
        right e <- r e
      where
        l t = merge e from
                node e   <- 1
                left e   <- l e
                right e  <- r e
                unLeft e <- t
        r t = merge e from
                node e    <- 1
                left e    <- l e
                right e   <- r e
                unRight e <- t

# Typed Forth

    codata Forth s where
      push : Forth b -> a -> Forth (a, b)
      drop : Forth (a, b) -> Forth b
      app  : Forth (a, (b, c)) -> (a -> b -> d) -> Forth (d, c)
      get  : Forth (a, b) -> a

    prog1 : Int
    prog1 = empty
      .push 5
      .push 7
      .app (+)
      .get

    empty : Forth ()
    empty = merge e from
      push e <- push0

    push0 : a -> Forth (a, ())
    push0 x = merge e from
      push e <- push1 e
      drop e <- empty
      get e  <- x

    push1 : Forth (b, c) -> a -> Forth (a, (b, c))
    push1 f x = merge e from
      push e <- push1 e
      drop e <- f
      get e  <- x
      app e  <- doApp
        where doApp f =