同构中前向和后向映射之间的关系(镜头包)

Question

为什么/ 在类型的同s构中t,不应该约束同构和b同a构Iso s t a b？

我知道我们有一个前向映射s -> a和一个后向映射b -> t,但为什么没有关系强加于这些映射

 type Iso s t a b = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t)

Answer 1

您想要同构的不是stot或ato b，而是stoa和tto b。考虑这个例子：

Prelude Control.Lens> (True, ()) & swapped . _1 %~ show
(True,"()")

在这里，我们将Iso swapped与Lens _1;组合起来。在此使用中，它们的组合相当于Lens _2, ，因此show应用于元组的第二个元素(True, ())。请注意，这show是类型更改。那么我们在这里实际使用的是什么类型Iso swapped？

• s是我们原始元组的类型，(Bool, ())
• t是最终结果的类型，(Bool, String)
• as是交换后的类型，((), Bool)
• bt是换回之前的类型，(String, Bool)

换句话说，我们正在使用swappedat 类型

swapped :: Iso (Bool, ()) (Bool, String) ((), Bool) (String, Bool)

每个映射s -> a和b -> t都是双射，但其他类型之间不存在这种必然关系。

至于为什么似乎没有列出Isos 的定律说这些需要是双射，我不知道。

编辑：上面评论中 @bennofs 发布的链接中的“为什么它是一个镜头系列”部分确实为我澄清了一些事情。显然，Edward Kmett 并不希望这些类型完全自由变化。

虽然它不能直接用光学器件的类型来表达而不会使使用变得尴尬，但其目的是改变类型的光学器件系列（Lens，Iso或其他）应该具有由类型系列inner和给出的类型outer。如果 an 的类型之一Iso是

anIso :: Iso s t a b

那么应该有两种索引类型i，j这样

s = outer i
t = outer j
a = inner i
b = inner j

此外，您可以交换i和j，尽管没有自动执行此操作，但结果仍然应该是您的多态的合法类型Iso。即您还应该被允许使用anIsoat 类型

anIso :: Iso t s b a

显然这适用于swapped. 这两种都是合法的类型：

swapped :: Iso (Bool, ()) (Bool, String) ((), Bool) (String, Bool)
swapped :: Iso (Bool, String) (Bool, ()) (String, Bool) ((), Bool)

换句话说，如果一个多态Iso族正在进行类型改变，那么它还需要支持反向类型改变。（还组成了类型变化。我在这里闻到了范畴论的自然转变，我怀疑这也是克梅特的一种思考方式。）

另请注意，如果您的多态性Iso构造为

f :: s -> a
g :: b -> t
iso f g :: Iso s t a b

然后为了使其也具有类型iso f g :: Iso t s a b，我们需要f和g也具有类型

f :: t -> b
g :: a -> s

请注意，fused at 其第一种类型具有与used at 其第二类型s -> a相反的正确类型，以及相应的另一种方式。ga -> s

举个具体的例子，swapped在这里有点糟糕，因为它的f和g用于元组时是相同的，本质上它们都是\(x,y) -> (y,x)，这是它自己的逆。Simple我在 中看到的最好的其他非示例Control.Lens.Iso是curried，这似乎有点太复杂而无法澄清。