Является ли лемма Йонеды полезной только с теоретической точки зрения?

Question

Например, слияние петель можно получить с помощью Yoneda:

newtype Yoneda f a =
    Yoneda (forall b. (a -> b) -> f b)

liftYo :: (Functor f) => f a -> Yoneda f a
liftYo x = Yoneda $ \f -> fmap f x

lowerYo :: (Functor f) => Yoneda f a -> f a
lowerYo (Yoneda y) = y id

instance Functor (Yoneda f) where
    fmap f (Yoneda y) = Yoneda $ \g -> y (g . f)

loopFusion = lowerYo . fmap f . fmap g . liftYo

Но я мог бы просто написать loopFusion = fmap (f . g). Зачем мне вообще использовать Yoneda? Есть ли другие варианты использования?

Answer 1

Ну, в этом случае вы могли бы выполнить слияние вручную, потому что два fmap "видны" в исходном коде, но дело в том, что Yoneda выполняет преобразование в во время выполнения. Это динамичная вещь, наиболее полезная, когда вы не знаете , сколько раз вам потребуется fmap над структурой. Например. рассмотрим лямбда-термины:

data Term v = Var v | App (Term v) (Term v) | Lam (Term (Maybe v))

Maybe в Lam представляет переменную, связанную абстракцией; в теле Lam переменная Nothing относится к связанной переменной, а все переменные Just v представляют переменные, связанные в среде. (>>=) :: Term v -> (v -> Term v') -> Term v' представляет замену - каждый v ariable может быть заменен на Term. Однако при замене переменной внутри Lam все переменные в произведенном Term должны быть заключены в Just. Э.Г.

Lam $ Lam $ Var $ Just $ Just $ ()
  >>= \() -> App (Var "f") (Var "x")
=
Lam $ Lam $ App (Var $ Just $ Just "f") (Var $ Just $ Just "x")

Наивная реализация (>>=) выглядит так:

(>>=) :: Term v -> (v -> Term v') -> Term v'
Var x >>= f = f x
App l r >>= f = App (l >>= f) (r >>= f)
Lam b >>= f = Lam (b >>= maybe (Var Nothing) (fmap Just . f))

Но, написанное так, каждый Lam, под которым (>>=) попадает, добавляет fmap Just к f. Если бы у меня был Var v похоронен под 1000 Lam с, то я бы в итоге позвонил fmap Just и перебрал бы новый f v термин 1000 раз! Я не могу просто применить трюк и объединить несколько fmap в один вручную, потому что в исходном коде есть только один fmap, вызываемый несколько раз.

Yoneda может облегчить боль:

bindTerm :: Term v -> (v -> Yoneda Term v') -> Term v'
bindTerm (Var x) f = lowerYoneda (f x)
bindTerm (App l r) f = App (bindTerm l f) (bindTerm r f)
bindTerm (Lam b) f =
  Lam (bindTerm b (maybe (liftYoneda $ Var Nothing) (fmap Just . f)))

(>>=) :: Term v -> (v -> Term v') -> Term v'
t >>= f = bindTerm t (liftYoneda . f)

Теперь fmap Just свободен; это просто сложная функциональная композиция. Фактическая итерация по произведенному Term находится в lowerYoneda, который вызывается только один раз для каждого Var. Повторим еще раз: исходный код нигде не содержит ничего вида fmap f (fmap g x). Такие формы возникают только во время выполнения, динамически, в зависимости от аргумента (>>=). Yoneda может переписать это, во время выполнения , до fmap (f . g) x, даже если вы не можете переписать его таким образом в исходном коде. Кроме того, вы можете добавить Yoneda к существующему коду с минимальными изменениями. (Однако есть недостаток: lowerYoneda - это всегда , вызываемый ровно один раз для каждого Var, что означает, например, Var v >>= f = fmap id (f v), где это было просто f v, до этого.)

Answer 2

Есть пример, похожий по духу на пример, описанный HTNW в объектив . Взгляд (перефразированная версия) функции lens иллюстрирует, как выглядит типичный объектив Ван Ларховена:

-- type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t
lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
lens getter setter = \f -> \s -> fmap (setter s) (f (getter s))

Наличие здесь fmap означает, что составление линз в принципе приведет к последовательному использованию fmap. Теперь, в большинстве случаев, это не имеет значения: реализации в lens используют много встроенных и принуждений нового типа, так что при использовании комбинаторов lens (view, over и т. Д.), Задействованный функтор (обычно Const или Identity) обычно оптимизируется. Однако в некоторых ситуациях это невозможно сделать (например, если линза используется таким образом, что конкретный выбор функтора не делается во время компиляции). В качестве компенсации, lens предлагает вспомогательную функцию, называемую fusing, которая позволяет производить слияние fmap в этих особых случаях. Его реализация:

-- type LensLike f s t a b = (a -> f b) -> s -> f t
fusing :: Functor f => LensLike (Yoneda f) s t a b -> LensLike f s t a b
fusing t = \f -> lowerYoneda . t (liftYoneda . f)

В таком случае, если вы напишите fusing (foo . bar), Yoneda f будет выбран в качестве функтора, который будет использоваться foo . bar, что гарантирует fmap fusion.

(Этот ответ был вдохновлен комментарием Эдварда Кметта , на который я наткнулся прямо перед тем, как увидеть этот вопрос.)