时间戳

首页 > 解决方案 > Haskell 泛型。构建代表

haskell - Haskell 泛型。构建代表

问题描述

在尝试验证for when和, _mkl :*: rl = K1 _ afl = ((->) a)r = K1 _ bfr = ((->) b)

class Functor f => Mk rep f | rep -> f where
  mk :: f (rep a)

instance Mk (K1 i c) ((->) c) where
  mk = \x -> K1 x

instance (Mk l fl, Mk r fr) => Mk (l :*: r) (Compose fl fr) where
  mk = Compose (fmap (\l -> fmap (\r -> l :*: r) mk) mk)

现在通过类型类定义mk :: f (rep _)，我们有f = Compose ((->) a) ((->) b) = * -> a -> b -> *and rep _ = l:*:rso mk :: a -> b -> l:*:r。这是我所期望的。

但是，我认为(fmap (\l -> fmap (\r -> l :*: r) mk) mk) :: a -> b -> l:*:r并且我看不出如何将其用作第一个参数来Compose :: forall k k1. (k -> *) -> (k1 -> k) -> k1 -> *回馈mk??的预期签名。

另外，我发现这个答案https://stackoverflow.com/a/35424427/11998382很有帮助，但我迷路了

f :: Compose ((->) a) ((->) b) (f r)
g :: Compose ((->) c) ((->) d) (g r)
mk f g :: Compose (Compose ((->) a) ((->) b)) (Compose ((->) c) ((->) d)) ((:*:) f g r)

他们的意思是fl :: Compose ((->) a) ((->) b) (f r)还是mk f :: Compose ((->) a) ((->) b) (f r)？

标签： haskell

解决方案

我们有f = Compose ((->) a) ((->) b) = * -> a -> b -> *等等rep _ = l:*:rmk :: a -> b -> l:*:r

你有精神，但我想在这里狡辩一些细节。

第一：Compose ((->) a) ((->) b)不等于任何有趣的东西，除了它自己。但是，它与其他一些有趣的类型同构。例如，Compose ((->) a) ((->) b) c与 同构（但不等于！）a -> b -> c。（不过，我不确定*你的平等中的 ' 是什么或它们来自哪里。）

第二：在这种情况下，rep(not rep _) 被替换为l :*: r。因此，在您替换rep a为 的地方l :*: r，您实际上应该替换rep a为(l :*: r) a（或者，直到 alpha 重命名，rep c由(l :*: r) c）。就像我们对 所做的那样Compose，我们可以在这里观察到同构，即与(l :*: r) c同构(l c, r c)。

把这些放在一起，我们有

f (rep a)
= { alpha renaming: a is not bound (but f and rep are) }
f (rep c)
= { definition of f and rep }
Compose ((->) a) ((->) b) ((l :*: r) c)
~= { the two isomorphisms described above }
a -> b -> (l c, r c)

但是，我认为(fmap (\l -> fmap (\r -> l :*: r) mk) mk) :: a -> b -> l:*:r并且我看不出如何将其用作第一个参数来Compose :: forall k k1. (k -> *) -> (k1 -> k) -> k1 -> *回馈预期的签名mk

谨防！有两个名为 的实体Compose。一个是在类型级别，并且具有您提供的那种：

Compose :: forall k k1. (k -> *) -> (k1 -> k) -> k1 -> *

但是在计算级别还有另一个，看起来非常不同：

Compose :: f (g a) -> Compose f g a

在这种类型中，第一个Compose是计算级别Compose，第二个Compose是类型级别Compose。

Compose定义中使用的是术语级别，而mk不是您似乎假设的类型级别。（在这一部分中，你也没有注意和之间的区别l :*: r，(l :*: r) c就像最后一点一样。）所以引用语句的正确版本是：(fmap (\l -> fmap (\r -> l :*: r) mk) mk) :: a -> b -> (l:*:r) c，所以使用 this 作为第一个参数Compose :: f (g a) -> Compose f g a意味着Compose (fmap ... mk) :: Compose ((->) a) ((->) b) ((l:*:r) c)。

推荐阅读