同构(透镜包)中正向和后向映射的关系

Question

为什么没有任何东西约束s与t同构，而b在Iso s t a b类型的同构中与a同构

我知道我们有一个前向映射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

您希望成为同构的不是s到t，也不是a到b，而是s到a，t到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)
• a是交换后的s类型，((), Bool)
• b是交换前的t类型，(String, Bool)

换句话说，我们正在使用类型为swapped的

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

每个映射s -> a和b -> t都是一个双射，但其他类型之间没有这种必要的关系。

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

编辑:上面评论中@bennofs发布的链接中的“为什么是镜头家族”一节为我澄清了一些事情。显然，Edward并不打算完全自由地改变这些类型。

虽然它不能直接表达在一种光学的类型而不使它的使用不便，但意图是一个类型改变的光学家族(Lens，Iso或其他)应该有类型家庭inner和outer给出的类型。如果Iso的类型之一是

anIso :: Iso s t a b

然后应该有两个索引类型i和j，以便

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

此外，您可以交换i和j，虽然没有自动执行，但是结果仍然应该是多态Iso的合法类型。也就是说，还应该允许您在类型中使用anIso。

anIso :: Iso t s b a

显然，这对于swapped来说是成立的。这两种类型都是它的法律类型：

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

换句话说，如果多态Iso家族正在更改类型，那么它也需要支持反向类型更改。(还包含类型更改。我从范畴理论中闻到了一种自然的转变，我怀疑这也是Kmett思考这个问题的一种方式。)

还请注意，如果您的多态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

请注意，在其第一个类型中使用的f具有与其第二个类型s -> a中使用的g相反的类型，而相应地则相反。

作为一个具体的例子，swapped在这里有点糟糕，因为用于元组的f和g是相同的，本质上它们都是\(x,y) -> (y,x)，这是它自己的反义词。我在Control.Lens.Iso中看到的另一个最好的非Control.Lens.Iso例子是curried，它似乎太复杂了，难以澄清。