代码之家 › 专栏 › 技术社区 › Kristóf Marussy

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

lenses category-theory haskell-lens haskell

9

Kristóf Marussy · 技术社区 · 6 年前

A. 棱镜是一种聚焦于副产品类型的光学器件 affine traversal 是一种可以在1个元素的0处聚焦的光学元件,即。 AffineTraversal s t a b 同构于 (s -> Maybe a, (s, b) -> t) 。据我所知,如果使用适当的棱镜编码,当透镜由棱镜组成时,我们会得到仿射遍历。

我对移动 Maybe 在这个(天真的)公式中,我将其转换为setter端,而不是getter端,这样我就可以有一个始终只提取一个元素的光学元件,但可能无法将其放回。

我的用例与细化类型相关。假设我们有一种 A 以及它的精致 B ( B â A )。然后是一个棱镜 refined :: Prism' A B :an A. 可能有效,也可能无效 B ,但每个 B 可以是 re 进入 A. 。组合a Lens' C A 具有 refined ,我们有一个仿射遍历。在另一个方向,可以想象一个光学 unrefined 这比 re refined :an A. 可以变成 Just b ,如果它是有效的 B 或 Nothing ,如果不是。现在如果我们结合 Lens' C B 具有 未精炼的 ,我们有我们的双重仿射遍历:它总是可以 A. 从…起 C 但是把旧的 A. 可能违反 C 的不变量和屈服 没有什么 而不是 Just c 。可以以类似的方式确保更复杂的不变量。

有趣的是 monocle Scala库为细化类型提供棱柱体,但不为反向提供棱柱体。

我很难为这些制定法律 (s -> a, b -> Maybe t) 和 (s -> a, (s, b) -> Maybe t) 我想知道一个更抽象的光学公式是否有用。

我知道用profunctor镜头

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中删除产品/副产品,而不是引入它)?然而,我无法从他们那里还原出天真的表述。。。

1 回复 | 直到 6 年前

1

3

Li-yao Xia 6 年前

下面是半个答案,显示了 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