棱柱或仿射遍历的对偶是什么？

Question

棱柱或仿射遍历的对偶是什么？

haskellhaskell-lenscategory-theorylenses

11

一个棱镜是一种用于聚焦到乘积类型的光学器件，而仿射遍历是一种可以在1元素的0处进行聚焦的光学器件，即AffineTraversal s t a b与(s -> Maybe a, (s, b) -> t)同构。据我所知，当适当编码棱镜时，将镜头与棱镜组合可以得到仿射遍历。

我有兴趣将那个（天真的）公式中的Maybe移到setter侧，而不是getter侧，以便我可以拥有一种始终精确提取一个元素但可能无法放回的光学器件。

我的用例与精化类型相关。假设我们有一个类型A及其精化B（B ⊆ A）。那么就会有一个棱镜refined :: Prism' A B：一个A可能是有效的B，也可能不是，但每个B都可以被重新获取为A。将Lens' C A与refined结合起来，我们就得到了一个仿射遍历。另一方面，可以想象一个比re refined更聪明的光学工具unrefined：如果A是有效的B，则它可以被转换为Just b，否则为Nothing。现在，如果我们将Lens' C B与unrefined结合起来，就得到了我们的对偶仿射遍历：它总是可以从C获得A，但将任何旧的A放回可能会违反C的不变量，并产生Nothing而不是Just c。可以通过类似的方式确保更复杂的不变量。

有趣的是，Scala的monocle库提供了用于细化类型的棱镜，但没有提供反向操作。

我很难为这些(s -> a, b -> Maybe t)和(s -> a, (s, b) -> Maybe t)小工具制定规则，想知道更抽象的光学公式是否有帮助。

我知道使用profunctor lens，我们可以

type Lens s t a b = forall p. Strong p => p a b -> p s t
type Prism s t a b = forall p. Choice p => p a b -> p s t
type AffineTraversal s t a b = forall p. (Strong p, Choice p) => p a b -> p s t

这段话的意思是镜头可以放大产品类型，棱镜可以放大余产品类型，而仿射遍历可以放大代数数据类型（仍然是产品或余乘积）。是否与Cochoice或者Costrong有关（从Profunctor中删除一个乘积/余乘积而不是引入它）？但我无法从中恢复出天真的公式。{{因为需要上下文才能理解的术语没有翻译}}

- Kristóf Marussy

2

我可能没有完全理解你的问题，但我相信Strong的对偶是Choice，相应地，Lens的对偶是Prism。这使得AffineTraversal的对偶是... AffineTraversal。 - Benjamin Hodgson

“双重”可能是ne不幸的措辞选择。 - Kristóf Marussy

你可以使用 Re 来“翻转光学”，将 Prisms a b s t 转换为 (s -> a, b -> Maybe t) 的 profunctor 光学等效形式，详见这篇博客文章 http://oleg.fi/gists/posts/2017-04-18-glassery.html。 - Li-yao Xia

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Li-yao Xia · Accepted Answer

这里有一半的答案，展示了Cochoice光学和(s -> a, b -> Maybe t)之间的对应关系。

{-# LANGUAGE RankNTypes #-}

module P where

import Data.Profunctor
import Control.Monad

data P a b s t = P (s -> a) (b -> Maybe t)

instance Profunctor (P a b) where
  dimap f g (P u v) = P (u . f) (fmap g . v)

instance Cochoice (P a b) where
  unleft (P u v) = P (u . Left) (v >=> v') where
    v' (Left t) = Just t
    v' (Right _) = Nothing

type Coprism s t a b = forall p. Cochoice p => p a b -> p s t

type ACoprism s t a b = P a b a b -> P a b s t

fromCoprism :: ACoprism s t a b -> P a b s t
fromCoprism p = p (P id Just)

toCoprism :: P a a s t -> Coprism s t a a
toCoprism (P u v) = unleft . dimap f g where
  f (Left s) = u s
  f (Right a) = a
  g b = case v b of
    Nothing -> Right b
    Just t -> Left t