Определение fmap с идентификатором и возвращением - PullRequest
Новая
       30

Определение fmap с идентификатором и возвращением

0 голосов
/ 06 июня 2018

В Теория категорий для программистов Бартоша Милевского, Милевский пишет следующий код для определения возврата и оператора 'fish' (состав в категории Клейсли) для монады Writer.

return :: a -> Writer a
return x = (x, "")

(>=>) :: (a -> Writer b) -> (b -> Writer c) -> (a -> Writer c)
m1 >=> m2 = \x ->
  let (y, s1) = m1 x
      (z, s2) = m2 y
  in  (z, s1 ++ s2)

Затем он определяет fmap следующим образом: 

fmap f = id >=> (\x -> return (f x))

Мне сложно понять, как здесь используется функция id.Первый аргумент оператора fish явно (a -> Writer b), но id имеет сигнатуру типа a -> a.

Это ошибка или ошибка в моем понимании?Замена id на return имеет для меня больше смысла.

1 Ответ

0 голосов
/ 06 июня 2018

Не забудьте универсальные количественные показатели.

Рыба (>=>) имеет тип (a -> Writer b) -> ..... для любых a и b.

id имеет тип a -> a для любого a.

Следовательно, в частности, рыба также имеет тип (Writer b -> Writer b) -> ... для любого b (просто возьмите a = Writer b в качестве специальногоcase).

Кроме того, id также имеет тип Writer b -> Writer b (опять же, как особый случай).

«Хитрость» заключается в том, чтобы «объединить» два типа, используя унификация .Мы начинаем с требования (a -> Writer b) = (a' -> a'), а затем выводим a = a' и Writer b = a'.Отсюда мы видим, что эти два типа могут быть объединены, поэтому в передаче аргументов нет никакого противоречия.

(Также обратите внимание, что здесь мы переименовали a в типе id в a' во избежание путаницы с другими a для рыбы)

...