Как получить тип для этой функции: - PullRequest
Новая
       18

Как получить тип для этой функции:

0 голосов
/ 07 февраля 2019

Я пытаюсь стать лучше, играя в "тетрис типа".У меня есть функции: 

(=<<) :: Monad m => (a -> m b) -> m a -> m b
zip :: [a] -> [b] -> [(a, b)]

И GHCi говорит мне: 

(zip =<<) :: ([b] -> [a]) -> [b] -> [(a, b)]

Мне трудно понять, как получить окончательную подпись из первых двух.Моя интуиция (из-за отсутствия лучшего слова) говорит, что первый аргумент =<<, а именно a -> mb каким-то образом согласован с сигнатурой zip, и тогда все должно выпасть из этого.Но я не могу понять, как сделать этот прыжок.Можно ли разбить его на серию простых шагов?

Ответы [ 3 ]

0 голосов
/ 07 февраля 2019

Это помогает сделать две вещи прежде всего:

  1. поставить явные скобки так, чтобы x->y->z стало x->(y->z)
  2. переименовывать переменные типа, чтобы не было конфликтов

С учетом этого давайте перепишем типы 

(=<<) :: Monad m => (a -> m b) -> (m a -> m b)
zip :: [x] -> ([y] -> [(x, y)])

Теперь сопоставим типы.Первый аргумент =<< равен zip, поэтому (a -> m b) совпадает с [x] -> ([y] -> [(x, y)]). 

a          ->        m b
[x]        ->        ([y] -> [(x, y)])

Так что a равно [x] и m b равно ([y] -> [(x, y)]).Переписав -> в префиксной записи, мы получим -> [y] [(x, y)], что совпадает с (-> [y]) [(x, y)]. 

m             b
(-> [y])      [(x, y)]

Так что m равно (-> [y]) (что действительно является монадой) и b это [(x, y)].

Итак, теперь мы знаем, что такое a, что такое b и что такое m.Давайте перепишем (m a -> m b) в следующих терминах: 

(m            a)          ->          (m            b)
((-> [y])     [x])        ->          ((-> [y])     [(x, y)])

Переписав снова в стиле инфикса, мы получим 

([y] -> [x])              ->          ([y] -> [(x, y)])

, то есть, вплоть до имен переменных, такой же ответ GHCдавая вам.

0 голосов
/ 07 февраля 2019

Вы просто записываете их один под другим с вертикальным выравниванием в качестве вспомогательного средства, последовательно переименовывая переменные типа, чтобы избежать случайного захвата: 

(=<<) :: Monad m => (a1  ->     m    b1       ) -> m a1 -> m b1
zip   ::             [a] -> ([b] ->  [(a, b)])
                     [a] -> ([b] ->) [(a, b)]
                     [a] -> (->) [b] [(a, b)]
-----------------------------------------------------------
               a1 ~ [a] ,  m ~ (->) [b] ,  b1 ~ [(a, b)]               (*)
-----------------------------------------------------------
(zip =<<) :: Monad m =>                            m a1 -> m b1
                                          ((->) [b]) a1 -> ((->) [b]) b1
                                            ([b] -> a1) -> ([b] -> b1)
                                           ([b] -> [a]) -> ([b] -> [(a, b)])
                                           ([b] -> [a]) ->  [b] -> [(a, b)]

при условии, что экземпляр Monad ((->) [b]) существует.Что он делает: 

> :i Monad
class Monad (m :: * -> *) where
    .......
instance Monad ((->) r) -- Defined in `GHC.Base'

Если мы следуем типам в конкретном случае функции монады, мы можем видеть, что (g =<< f) x == g (f x) x, и так 

(zip =<<) f xs = zip (f xs) xs

, из которого легче см. значение его типа.

(*) - это замена , полученная в результате успешного объединения типов a1 -> m b1 и[a] -> [b] -> [(a, b)] (то есть [a] -> ([b] -> [(a, b)]), когда заключены в круглые скобки, потому что -> в типах ассоциируются справа).Или в полном префиксе, 

    (->)  a1   ( m            b1       )
    (->)  [a]  ( ((->) [b])   [(a, b)] )
0 голосов
/ 07 февраля 2019

(zip =<<) эквивалентно (>>= zip), что делает его, возможно, немного более читабельным.В любом случае, zip занимает слот (a -> m b) в этих функциях, как вы правильно заметили.

Еще одно интуитивное преобразование - подумать об арности =<<.Он «принимает» два параметра, поэтому, если мы применим его к одному, у нас останется только еще один.Следовательно, подпись ([b] -> [a]) -> [b] -> [(a, b)] является унарной функцией! 

(zip =<<) :: ([b] -> [a]) -> ([b] -> [(a, b)])
             ------------    -----------------
                 m a'                m b'

Так что же такое m?Экземпляр Monad существует для функций (r ->) (или, альтернативно, (->) r).Таким образом, в этом случае r :: [b] (и, следовательно, m :: ([b] ->)), a' :: [a] и b' :: [(a, b)].

Следовательно, zip соответствует так, как мы утверждали в начале: 

a'  -> m b'                    -- substitute [(a,b)] for b'
a'  -> m [(a, b)]              -- substitute [a] for a'
[a] -> m [(a, b)]              -- substitute ([b] ->) for m
[a] -> ([b] -> [(a,b)])

[a] -> [b] -> [(a,b)]
...