Haskell 中的 `join bimap` 签名

Question

在 codewars 的解决方案之一中，我遇到了以下表达式：

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')

这是 ghci 中 join @((->) _) bimap 的输出，有和没有 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 派生了一个实现。

Haskell 中的 `join bimap` 签名

Signature of `join bimap` in Haskell

haskell

type-inference

parametric-polymorphism