haskell - Isomorphism 中前向和后向映射的关系(Lens 包)

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

你想要同构的不是 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 Kmett 并不打算让这些类型完全自由变化。

虽然不能直接用光学元件的类型来表达，但使用起来会很尴尬，
目的是改变类型的光学系列( 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 的合法类型. IE。你也应该被允许使用 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 family 是换型，那么也需要支持反向换型。 (也是组合类型的变化。我在这里闻到了范畴论的自然转变，我怀疑这也是 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 的倒数用于第二种类型 a -> s , 和相应的另一种方式。

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