Haskell中`join 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 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 派生了一个实现，以机械方式从其类型中获得函数。

Answer 3

这里是使用可见类型应用程序的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