为什么/不应该限制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)
问问题
355 次
1 回答
3
您想要同构的不是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在这里实际使用的是什么类型的 at 呢？
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都是双射，但其他类型之间没有这种必然关系。
至于为什么似乎没有列出Isos 的法律说这些需要是双射，我不知道。
编辑：@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
此外，您可以交换iand j，尽管不会自动执行此操作，但结果仍然应该是您的 polymorphic 的合法类型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
然后为了让 this也有类型iso f g :: Iso t s a b，我们需要f并且g也有类型
f :: t -> b
g :: a -> s
请注意fused at its first types -> a的正确类型是gused at its second type的逆类型a -> s，并且相应地相反。
举一个具体的例子，swapped这里有点糟糕，因为它用于元组的 和 是相同的，本质上它们都是f，这是它自己的逆。我在其中看到的最好的其他非示例是，这似乎有点太复杂而无法澄清。g\(x,y) -> (y,x)SimpleControl.Lens.Isocurried
于 2014-09-28T07:00:21.140 回答