Забывание Cofree аннотаций с использованием катаморфизма - PullRequest
Новая
       92

Забывание Cofree аннотаций с использованием катаморфизма

0 голосов
/ 26 июня 2018

У меня есть AST, который я аннотирую, используя Cofree: 

data ExprF a
  = Const Int
  | Add a
        a
  | Mul a
        a
  deriving (Show, Eq, Functor)

Я использую type Expr = Fix ExprF для представления нетегированных AST и type AnnExpr a = Cofree ExprF a для представления теговых. Я нашел функцию для преобразования помеченных AST в немаркированные, отбросив все аннотации: 

forget :: Functor f => Cofree f a -> Fix f
forget = Fix . fmap uncofree . unwrap

Похоже, это может быть своего рода катаморфизм (я использую определение из пакета рекурсивных схем Кметта ). 

cata :: (Base t a -> a) -> t -> a
cata f = c where c = f . fmap c . project

Я бы подумал, что вышеизложенное, переписанное с использованием катаморфизма, будет выглядеть примерно так, но я не могу понять, что положить на alg, чтобы сделать проверку типов. 

forget :: Functor f => Cofree f a -> Fix f
forget = cata alg where
  alg = ???

Любая помощь в выяснении, действительно ли это ката / анаморфизм, и некоторая интуиция, объясняющая, почему это так или нет, будет принята с благодарностью.

1 Ответ

0 голосов
/ 26 июня 2018 
forget :: Functor f => Cofree f a -> Fix f
forget = cata (\(_ :< z) -> Fix z)
-- (Control.Comonad.Trans.Cofree.:<)
-- not to be confused with
-- (Control.Comonad.Cofree.:<)

Объяснение

Глядя только на типы, мы можем показать, что на самом деле существует только один способ реализации forget. 

cata :: Recursive t => (Base t b -> b) -> t -> b

Здесь t ~ Cofree f a и экземпляр типа Base для Cofree дает: 

type instance Base (Cofree f a) = CofreeF f a

Где CofreeF: 

data CoFreeF f a b = a :< f b
-- N.B.: CoFree also defines a (:<) constructor so you have to be
-- careful with imports.

то есть тип причудливой пары. Давайте заменим его фактическим типом пары, чтобы прояснить ситуацию: 

cata :: Functor f => ((a, f b) -> b) -> Cofree f a -> b

Теперь мы действительно специализируемся cata с более конкретным a, а именно Fix f: 

-- expected type of `cata` in `forget`
cata :: Functor f => ((a, f (Fix f)) -> Fix f) -> Cofree f a -> Fix f

forget является параметрическим в a и f, поэтому функция, которую мы даем cata, ничего не может сделать с a в паре, и единственный разумный способ реализовать оставшиеся f (Fix f) -> Fix f - это Fix обертка.

Оперативно, Fix - это идентификатор, поэтому (\(_ :< z) -> Fix z) на самом деле (\(_ :< z) -> z), что соответствует интуиции удаления аннотации, то есть первого компонента пары (_ :< z).

...