Haskell Recursion Schemes: Traverse two structures simultaneously

Question

I'm trying to write Robinson's unification algorithm using recursion schemes. The unification algorithm takes two types and spits a result. A type is a:

data TypeF a
    = TypeApplication a a
    | TypeVariable Name
    deriving (Read,Show,Eq,Functor,Foldable,Traversable)
type Type = Fix TypeF

unify :: Type -> Type -> Result
unify = ...

How can this be done elegantly using recursion schemes?

Answer 1

I'd just suggest currying and a hylomorphism.

data TypeF a
    = TypeApplication a a
    | TypeVariable Name
    deriving (Read,Show,Eq,Functor,Foldable,Traversable)
type Type = Fix TypeF

unify :: (Type, Type) -> Result
unify = hylo algebra coalgebra
    where algebra :: TypeF Result -> Result
          algebra = ...
          coalgebra :: (Type, Type) -> TypeF (Type, Type)
          coalgebra = ...

As an aside, I would probably with TypeF as follows, using the recursion-schemes package.

import Data.Functor.Foldable.TH (makeBaseFunctor)

data Type = TypeApplication Type Type
          | TypeVariable Name

makeBaseFunctor ''Type

This will automatically generate exactly what you want in this case, with no need to use to Fix.