15 May
2015
15 May
'15
8:48 p.m.
On 15/05/15 19:08, anakreon wrote:
Could you suggest a solution for transforming trees encoded as Exp into equivalent Expr (e.g Not Not a ~> a)? cata does not work since it expects a function f a -> a while a transformation would be f a -> f a.
As you say, you have something of type f a -> f a, but you need something of type f a -> a to pass it to cata. Or, more specifically (replacing f with BExpr and a with Expr), you have something of type BExpr Expr -> BExpr Expr, and you need something of type BExpr Expr -> Expr. If only BExpr Expr was isomorphic to Expr! Oh wait... it is. You define Expr as the fixpoint of BExpr, which means that BExpr Expr and Expr are essentially the same. Roman