Haskell cata types

Question

После прочтения (и реализации) части http://blog.sumtypeofway.com/recursion-schemes-part-2/ Мне все еще интересно, как работают функции в функции cata. cata функция определяется следующим образом:

mystery :: Functor f => (f a -> a) -> Term f -> a 
mystery f = f . fmap (mystery f) . unTerm 

У меня есть что-то вроде Term Expr. После распаковки я получаю Expr (Term Expr). Алгебра (f) определена, например, как f :: Expr Int -> Int. Я знаю, что я мог бы назвать следующие легко:

x = Literal "literal" :: Expr a 
f :: Expr Int -> Int 
f x :: Int 

Я также могу представить себе:

x = Literal "literal" :: Expr (Term Expr) 
f :: Expr a -> Int 
f x :: Int 

Но следующий, я полагаю, не будет работать:

x = Literal "literal" :: Expr (Term Expr) 
f :: Expr Int -> Int 
f x :: ??? 

Однако, я до сих пор дон Как это работает в функции cata - как мне добраться от Expr (Term Expr) до Expr a. Я понимаю, что значения действительно работают, но я просто не получаю типы - что происходит в листьях дерева? Это действительно mystery ...

Редактировать: Я постараюсь более четко указать, что я не понимаю.

Мысленно, то cata, кажется, работает так:

• Применить fmap f листьям.
• Теперь у меня есть Expr Int, и я могу позвонить fmap f на узел, который у меня есть, и встать.

Это не работает так, как я применяю fmap (cata f). Однако в конечном счете функция f вызывается с Expr Int в качестве аргумента (в листьях). Как этот тип был произведен с Expr (Term Expr), что он был раньше?

Answer 1

Таким образом, cata работает на листьях.

Предполагается, что f :: Expr Int -> Int. Тогда:

cata f :: Term Expr -> Int 
fmap (cata f) :: Expr (Term Expr) -> Expr Int 

Теперь для любой функции g :: a -> b, мы имеем

fmap g :: Expr a -> Expr b 
fmap g (Literal n) = Literal n 
... 

Так, на литер, g несущественно. Это означает, что, выбирая a ~ Term Expr, b ~ Int и g = cata f мы имеем

fmap (cata f) (Literal n) = Literal n :: Term Int 
f (fmap (cata f) (Literal n)) = f (Literal n) :: Int 

Таким образом, грубо говоря, на листьях fmap (cata f) является не-оп, но изменяет тип от Expr (Term Expr) к Expr Int. Это тривиальное преобразование с Literal n :: Expr a для любого a.