Замените тип ReaderT и const композицией функций

Я пытаюсь выяснить, каков тип функциональной композиции ReaderT и const и хочу разобраться сам.

(.) ReaderT const :: ???  

Во-первых, посмотрите на сигнатуру типа ReaderT и (.):

ReaderT :: (r -> m a) -> ReaderT r m a
(.)     :: (b -> c) -> (a -> b) -> a -> c

затем я сделал следующую замену:

(.) ReaderT

шаг за шагом:

((r -> m a) -> ReaderT r m a) -> (a1 -> (r -> m a)) -> a1 -> ReaderT r m a

становится:

(a1 -> r -> m a) -> a1 -> ReaderT r m a

следующая замена на const:

const :: (a  -> ( b -> a  ))
         (a1 -> ( r -> m a)) -> a1 -> ReaderT r m a

Мой мозг остановился на этом месте. Как продолжить замену типа?


person softshipper    schedule 26.09.2017    source источник
comment
(r -> m a) ~ b и ReaderT r m a ~ c в типе (.) применительно к ReaderT.   -  person arrowd    schedule 26.09.2017
comment
Почему (r -> m a) ~ b и где переменная типа a функции const?   -  person softshipper    schedule 26.09.2017


Ответы (1)


ReaderT — унарная функция: она принимает (r -> m a) в качестве аргумента и возвращает ReaderT r m a в качестве результата.

Первый аргумент (.) также является унарной функцией b -> c. Передача ReaderT в качестве первого аргумента естественным образом дает (r -> m a) ~ b и ReaderT r m a ~ c:

(r -> m a) -> ReaderT r m a
    b      ->        c

Итак, подставив его в тип (.), получим

> :t (.) ReaderT
(.) ReaderT :: (a -> r -> m a1) -> a -> ReaderT r m a1

(.) был передан первый аргумент из двух, так что теперь это унарная функция (грубо говоря, (a -> b) -> a -> c часть (b -> c) -> (a -> b) -> a -> c), где b и c фиксированы к тому, что мы написали выше.

Теперь const :: a -> b -> a, бинарная функция и именно то, что (.) ReaderT ожидает дальше:

(a -> r -> m a1)
 a -> b -> a

Это означает, что a ~ m a1 и за счет этого a в типе (.) превращается в m a.

Итак, мы передали оба аргумента в (.), и это дает нам a -> c, где a ~ m a (обратите внимание, что эти a разные!) и c ~ ReaderT b m a.

person arrowd    schedule 26.09.2017
comment
Что будет с a в (a -> r -> m a1)? - person softshipper; 26.09.2017
comment
Поскольку const :: a -> b -> a и мы передаем его вместо (a -> r -> m a1), система типов делает вывод о том, что a ~ m a1 в последней подписи. - person arrowd; 26.09.2017
comment
Могу я сказать m a1 -> r -> m a1? - person softshipper; 26.09.2017
comment
Да, вы можете сказать это. - person arrowd; 26.09.2017