Haskell中“联接bimap`”的签名

Question

在关于代码战争的解决方案中，我遇到了以下表达式：

join bimap

其中有join :: Monad m => m (m a) -> m a和bimap :: Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d。结果表达式的类型为：Bifunctor p => (c -> d) -> p c c -> p d d。

我可以猜测bimap的类型可以用(->) (a->b) ((->) (c->d) p a c -> p b d)形式编写，但我不知道p a c是如何转换为p c c的，而p b d是如何转换为p d d的。请给我一些提示，如何解开这个谜题。

Answer 1

首先，让我们看看应用于函数的join类型。假设您有一个函数f :: t -> u -> v；或者，等效地说，是f :: (->) t ((->) u v)。通过比较这两种类型，我们可以尝试将其与join :: Monad m => m (m a) -> m a统一起来：

           (->) t ((->) u v)
Monad m => m      (m      a) -> m a

因此，我们可以尝试通过设置m ~ (->) t和a ~ v来统一类型。

(->) t ((->) u v)
(->) t ((->) t v) -> (->) t v

但是有一个问题:为了使这些类型匹配，我们还需要t ~ u！因此，我们可以得出结论，只有当前两个参数具有相同的类型时，join才能应用于一个函数--如果它们不是，那么只有在有方法使它们相等的情况下，才能将join应用于该函数。

现在，想想bimap :: Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d。通常情况下，a、b、c、d和p可能是任何类型。但是，如果您想将join应用于bimap，这就增加了一个约束，即bimap的前两个参数必须具有相同的类型:即(a -> b) ~ (c -> d)。由此我们可以得出a ~ c和b ~ d的结论。但是，当然，这意味着p a c必须与p a a相同，p b d必须与p b b相同，从而解决了这个难题。

Answer 2

下面是使用可见类型应用程序对join和bimap的完整实例化。它很混乱，因为在幕后发生了很多事情

joinBimap :: forall bi a a'. Bifunctor bi => (a -> a') -> (bi a a -> bi a' a')
joinBimap = join @((->) (a -> a')) @(bi a a -> bi a' a') (bimap @bi @a @a' @a @a')

下面是join @((->) _) bimap在ghci中的输出，有和没有bimap

>> :set -XTypeApplications
>> import Control.Monad (join)
>> import Data.Bifunctor (Bifunctor(bimap))
>>
>> :t join @((->) _) bimap
.. :: Bifunctor p => (c -> b) -> p c c -> p b b
>> :t join @((->) _)
.. :: (_ -> _ -> a) -> _ -> a

使用join @((->) _)类型的唯一合理实现是

joinReader :: (env -> env -> a) -> (env -> a)
joinReader (·) env = env · env

在ghci中引入类型变量是很棘手的。我们没有办法编写类似\@a @a' -> join @((->) (a -> a'))的东西。

一种不向函数添加参数的方法是给它一个部分类型签名，以量化新类型变量。

>> :set -XScopedTypeVariables
>> :set -XPartialTypeSignatures -Wno-partial-type-signatures
>>
>> :t join @((->) (a -> a')) bimap :: forall a a'. _
.. :: Bifunctor p => (a -> a') -> p a a -> p a' a'

还可以使用代理对象，并将其应用于获得预期的项。如果类型变量不止一个，或者是Type以外的其他类型，则可以使用像\(_ :: _ a a') -> ..这样的代理对象。

>> :t (\(_ :: a) (_ :: a') -> join @((->) (a -> a'))) undefined undefined
.. :: ((a1 -> a') -> (a1 -> a') -> a2) -> (a1 -> a') -> a2
>>
>> import Data.Function ((&))
>> :t undefined & \(_ :: _ a a') -> join @((->) (a -> a')
.. :: ((a1 -> a') -> (a1 -> a') -> a2) -> (a1 -> a') -> a2

Answer 3

类型派生纯粹是机械的事情：

join foo x = foo x x
=>
join bimap x = bimap x x 
  :: ( ((a->b)~(c->d)) => p a c -> p b d ) 
  ~  (   (a~c, b~d)    => p a c -> p b d ) 
  ~  p c c -> p d d

再一次，慢慢来：

bimap :: Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d
bimap (x :: a -> b) (y :: c -> d) :: Bifunctor p => p a c -> p b d
                     x :: a -> b
----------------------------------
                         a~c, b~d
----------------------------------
bimap (x :: a -> b) (x :: a -> b) :: Bifunctor p => p c c -> p d d

你问，为什么join foo x = foo x x是？我们甚至不知道这个foo是什么？但是我们看到join foo的结果是一个函数，因为我们将它应用于x。有了功能，

join :: Monad m        => m      (m      a)  -> m      a
     :: Monad ((->) r) => (->) r ((->) r a)  -> (->) r a
     :: Monad ((->) r) => (r  -> (r  ->  a)) -> (r ->  a)
     :: Monad ((->) r) => (r  ->  r  ->  a ) ->  r ->  a 
     foo               :: (r  ->  r  ->  a ) 
---------------------------------------------
join foo                                     ::  r ->  a

join foo是一个函数，因此foo是一个函数，foo :: r -> r -> a

join foo                                         x =   a
  where
  a = foo                  x      x -- :: a

在这里，我们甚至从函数的类型导出了函数的join实现。