Рассуждения о типах в Haskell

Глава 16 книги Haskell Programming from First Principles на стр. 995 содержит упражнение для ручного определения того, как (fmap . fmap) выполняет проверку типов. Он предлагает заменить тип каждого fmap на типы функций в типе оператора композиции:

T1 (.) :: (b -> c) -> (a -> b) -> a -> c

T2 fmap :: Functor f => (m -> n) -> f m -> f n

T3 fmap :: Functor g => (x -> y) -> g x -> g y

(Пытаясь) заменить T2 и T3 на T1, я пришел к следующему:

T4: ((m -> n) -> f m -> f n) -> ((x -> y) -> g x -> g y) -> a -> c

Кроме того, предлагается проверить тип (fmap . fmap), чтобы увидеть, как должен выглядеть конечный тип.

T5: (fmap . fmap) :: (Functor f1, Functor f2) => (a -> b) -> f1 (f2 a) -> f1 (f2 b)

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


types function-composition type-inference haskell hindley-milner
person Unsatisfied Zebra    schedule 17.05.2021    source источник
comment
Я даю сокращенный вывод в конце этого ответа, посмотрите, поможет ли это.   -  person Will Ness    schedule 17.05.2021
comment
Вы заменили a и c в некоторых местах, но не в других. Вы должны сделать это везде, чтобы получить правильный тип.   -  person dfeuer    schedule 19.05.2021

Ответы (1)


arrow_upward
3
arrow_downward

Приступаем к делу шаг за шагом:

--- fmap . fmap  =  (.) fmap fmap
--- Functor f, g, ... => ..... 

(.)      :: (   b     ->      c    ) -> (a ->  b ) -> a ->     c
    fmap ::  (d -> e) -> f d -> f e
             --------    ----------
(.) fmap ::                             (a ->d->e) -> a -> f d -> f e
                                             ----          ----------
-- then,

(.) fmap      :: (   a     ->  d  ->  e ) -> a   -> f   d   -> f   e
         fmap ::  (b -> c) -> g b -> g c
                  --------    ---    ---
(.) fmap fmap ::                          (b->c) -> f (g b) -> f (g c)
                                          ------      -----      -----

Важно последовательно переименовывать все переменные типа при каждом отдельном использовании типа, чтобы избежать смешения.

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

 A -> B -> C   ~   A -> (B -> C)

и правило вывода типа

   f   :: A -> B
     x :: C
   --------------
   f x ::      B    ,  A ~ C

(f :: A -> B) (x :: C) :: B под эквивалентность/унификацию типов A ~ C и все что с этим связано.

person Will Ness    schedule 17.05.2021