Унифицирующие типы в Haskell

Question

Я как бы застрял с назначением относительно моих экзаменов. Я хочу, чтобы выяснить типы этих двух функций, применяя алгоритм объединяющую вручную:

map map 
(\x -> x >>= (\y -> y)) 

Может кто-то мне точку в правильном направлении? Единственный ресурс, который я смог найти до сих пор, - это запись в википедии, которая на самом деле не помогает мне из-за высокого уровня абстракции.

Поздравления и благодарность.

Answer 1

Давайте просто сделаем первый.

map :: (a -> b) -> [a] -> [b] 

Теперь мы можем записать его снова с двумя разными именами, для ясности:

map :: (c -> d) -> [c] -> [d] 

Теперь мы подставляем вторую в качестве первого параметра из первого, получают:

(a -> b) === (c -> d) -> ([c] -> [d]) (recall the associativity of (->)) 
a === (c -> d) 
b === ([c] -> [d]) 

Теперь мы заменяем эти назначения типа на оставшуюся часть первой подписи, получая

map map :: [c -> d] -> [[c] -> [d]] 

Очистить?

Answer 2

Тип map: map :: (a -> b) -> [a] -> [b]. Следовательно, тип map foo получается из [a] -> [b] путем замены a и b на то, что может быть получено из типа foo. Если, например, foo :: t -> t, вы заменяете a = t, b = t и получаете [t] -> [t]. Если foo :: [t] -> Int, вы получаете [[t]] -> [Int].

В вашем случае foo (map) - (x -> y) -> [x] -> [y]. Вы должны объединить этот тип с a -> b, чтобы узнать, что a и b должны быть заменены. [Обратите внимание, что функция стрелок правоассоциативный, x -> y -> z = x -> (y -> z).]

Чтобы найти тип

\x -> x >>= (\y -> y) 

использовать известный тип (>>=) :: Monad m => m a -> (a -> m b) -> m b. Игнорировать ограничение (Monad m =>) пока.

В качестве первого аргумента (>>=), x должен иметь тип m a для неизвестной пока m и a. Второй аргумент (>>=) здесь личность,

(\y -> y) :: t -> t 

так что вы должны объединить t -> t с a -> m b. Это дает вам некоторую информацию о a, а именно a = m b.

Это дает x :: m (m b) и (\x -> x >>= (\y -> y)) :: type_of_x -> type_of_rhs.

Наконец, вспомните временно забытое ограничение Monad m =>.