Bidirectional, open-recursion AST

BiAST.hs

data Ty = Bool | Arr Ty Ty deriving (Eq, Show)

data IExpr c i
  = Var Int
  | App i c
  | Annot c Ty
  | If c i i
  | ETrue
  | EFalse

data CExpr i c
  = Lam c
  | CI i

x :: Weave CExpr IExpr
x = Weave (App (Weave (Var 0)) (Weave (CI (Weave (Var 1)))))

data Fix f = Fix (f (Fix f))

data Weave f g = Weave (g (Weave g f) (Weave f g))

-- interesting eliminator
weave :: (Bifunctor f, Bifunctor g) => (f a a -> a) -> (g a a -> a) -> (Weave f g -> a)
weave f g = go where go (Weave x) = g (bimap (weave g f) go x)