Почему функция композиции с `join` может изменять входные данные функции? - PullRequest
Новая
       70

Почему функция композиции с `join` может изменять входные данные функции?

2 голосов
/ 05 октября 2019

Я недавно начал изучать Haskell, и я пытался выполнить следующую композицию функций (join . mapM), но получил некоторые странные типы из этой функции, которые я не понимаю. Я думал, что либо GHC будет предполагать, что t == m в типе mapM и вывод mapM станут m (m b), что будет совместимым или нет, и это приведет к ошибке из-за несоответствия типов. Вместо этого произошло следующее: 

mapM :: (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b)
join :: Monad m => m (m a) -> m a
join . mapM :: Traversable t => (a -> t a -> b) -> t a -> t b

Я не понимаю, как это возможно. Насколько я понимаю, в композиции функций должны использоваться входы первой (или второй, в зависимости от того, как вы на это смотрите) функции и выходы второй функции. Но здесь ожидаемая входная функция для mapM меняется с унарной функции на двоичную функцию, и я понятия не имею, почему. Даже если GHC не может просто сделать предположение, что t == m, как я, что я наполовину ожидал, он должен выдавать ошибку из-за несоответствия типов, а не изменять тип входной функции, верно? Что здесь происходит?

Ответы [ 2 ]

5 голосов
/ 05 октября 2019

Сначала вы специализируете mapM на: 

mapM' :: Traversable t => (a -> x -> b) -> t a -> x -> t b

(поскольку (->) x - это монада)

Затем вы специализируете его на: 

mapM'' :: Traversable t => (a -> t a -> b) -> t a -> t a -> t b

(мы просто устанавливаем x как t a)

Наконец мы соответствующим образом специализируем join: 

join' :: (x -> x -> r) -> x -> r

(опять же, (->) x - это монада)

И, надеюсь, становится понятнее, почему композиция join' . mapM'' равна 

join' . mapM'' :: Traversable t => (a -> t a -> b) -> t a -> t b
2 голосов
/ 05 октября 2019

Может быть, следующее будет более ярким, вместо этого: 

flip mapT :: (Traversable t, Monad m) => t a -> (a -> m b) -> t (m b)
sequenceA :: (Traversable t, Monad m) =>                      t (m b) -> m (t b)
flip mapM :: (Traversable t, Monad m) => t a -> (a -> m b)            -> m (t b)

           flip liftM :: Monad m      => m a -> (a -> m b) -> m (m b)
 join                 :: Monad m      =>                      m (m b) -> m    b
(join .) . flip liftM :: Monad m      => m a -> (a -> m b)            -> m    b
(>>=)                 :: Monad m      => m a -> (a -> m b)            -> m    b

(с использованием некоторых более специализированных типов, чем самые общие, здесь и там; также с переименованным mapT f = runIdentity . traverse (Identity . f)).

Ваш конкретный вопрос менее интересен. Тип деривации является полностью механическим процессом. Некоторые сущности должны быть совместимыми, чтобы все выражение имело смысл, поэтому их типы должны объединяться: 

 (join . mapM) a_mb  x  =       -- a_mb :: a -> m b
 = join (mapM  a_mb) x
 = join   ta_mtb     x          -- ta_mtb :: t a -> m (t b)

Чтобы присоединиться к функции, нужно вызвать ее дважды, 

 =        ta_mtb     x  x

, что означает x - это t a, поэтому m - это t a ->: 

        x :: t a 
 ta_mtb   :: t a -> m   (t b)
 ----------------------------
 ta_mtb x ::        m   (t b)
          ~       t a -> t b
          x ::    t a 
 ----------------------------
 ta_mtb x x ::           t b

, таким образом a_mb :: a -> m b ~ a -> t a -> b.

...