Почему fmap отображает каждый элемент списка?

Прочитав книгу Учите вас Haskell For Great Good и очень полезную статью в wiki-книге Теория категорий Haskell, которая помогла мне преодолеть общую ошибку категории путающих объектов категории с объектами программирования, я все еще имею следующий вопрос:

Зачем нужно fmap отображать все элементы списка?

Мне нравится, что это так, я просто хочу понять, как это теоретически обоснована категория. (или, возможно, проще обосновать использование HoTT?)

В обозначениях Scala List - функтор, который принимает любой тип и отображает его в тип из множества всех типов списков, например, он сопоставляет тип Int с типом List[Int] и отображает его функции на Int например,

  • Int.successor: Int => Int to Functor[List].fmap(successor) : List[Int] => List[Int]
  • Int.toString: Int => String to Functor[List].fmap(toString): List[Int] => List[String]

Теперь каждый экземпляр List[X] является моноидом с empty function (mempty в Haskell) и combine function (mappend в Haskell). Я предполагаю, что можно использовать тот факт, что списки являются моноидами, чтобы показать, что map должен отображать все элементы списка. Мое чувство здесь заключается в том, что если добавить pure функцию из аппликативного, это дает нам список только с одним элементом другого типа. например, Applicative[List[Int]].pure(1) == List(1). Так как map(succ) на этих элементах дает нам одноэлементный список со следующим элементом, это охватывает все эти подмножества. Тогда я полагаю, что функция combine на всех этих синглетонах дает нам все остальные элементы списков. Почему-то я полагаю, что это ограничивает способ работы карты.

Другим наводящим аргументом является то, что map должен отображать функции между списками. Так как каждый элемент из a List[Int] имеет тип Int, а если отображать на List[String], то нужно отобразить каждый его элемент или не будет правильный тип.

Итак, оба этих аргумента, похоже, указывают в правильном направлении. Но мне было интересно, что нужно, чтобы пройти остаток пути.

контрпример?

Почему это не функция контрпримерных карт?

def map[X,Y](f: X=>Y)(l: List[X]): List[Y] = l match {
  case Nil => Nil
  case head::tail=> List(f(head))
}

Кажется, что следуют правилам

val l1 = List(3,2,1)
val l2 = List(2,10,100)

val plus2 = (x: Int) => x+ 2
val plus5 = (x: Int) => x+5

map(plus2)(List()) == List()
map(plus2)(l1) == List(5)
map(plus5)(l1) == List(8)

map(plus2 compose plus5)(l1) == List(10)
(map(plus2)_ compose map(plus5)_)(l1) == List(10)

Ааа. Но это не соответствует закону id.

def id[X](x: X): X = x

map(id[Int] _)(l1) == List(3)
id(l1) == List(3,2,1)

Ответы

Ответ 1

Это опирается на теоретический результат, называемый "параметричностью", который сначала был определен Рейнольдсом, а затем разработан Уодлером (среди прочих). Пожалуй, самая известная статья на эту тему - "Теоремы бесплатно!" Вадлер.

Основная идея заключается в том, что только из полиморфного типа функции мы можем получить некоторую информацию о семантике функции. Например:

foo :: a -> a

Только из этого типа мы можем видеть, что, если foo завершается, это - функция тождества. Интуитивно понятно, что foo не может различать различные a поскольку в Haskell у нас нет, например, Java instanceof который может проверять фактический тип времени выполнения. Так же,

bar :: a -> b -> a

должен вернуть первый аргумент. И baz :: a → a → a должен возвращать либо первое, либо второе. И quz :: a → (a → a) → a должны применить некоторое фиксированное число раз, которое функция использовала к первому аргументу. Вы, наверное, поняли идею сейчас.

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

Для типа map мы получаем следующее страшное свойство:

forall t1,t2 in TYPES, f :: t1 -> t2.
 forall t3,t4 in TYPES, g :: t3 -> t4.
  forall p :: t1 -> t3.
   forall q :: t2 -> t4.
    (forall x :: t1. g (p x) = q (f x))
    ==> (forall y :: [t1].
          map_{t3}_{t4} g (map2_{t1}_{t3} p y) =
          map2_{t2}_{t4} q (map_{t1}_{t2} f y))

Выше map является известной функцией map, а map2 - любая произвольная функция, имеющая тип (a → b) → [a] → [b].

Теперь предположим, что map2 удовлетворяет законам функторов, в частности map2 id = id. Затем мы можем выбрать p = id и t3 = t1. Мы получаем

forall t1,t2 in TYPES, f :: t1 -> t2.
 forall t4 in TYPES, g :: t1 -> t4.
   forall q :: t2 -> t4.
    (forall x :: t1. g x = q (f x))
    ==> (forall y :: [t1].
          map_{t1}_{t4} g (map2_{t1}_{t1} id y) =
          map2_{t2}_{t4} q (map_{t1}_{t2} f y))

Применение закона функторов на map2:

forall t1,t2 in TYPES, f :: t1 -> t2.
 forall t4 in TYPES, g :: t1 -> t4.
   forall q :: t2 -> t4.
    (forall x :: t1. g x = q (f x))
    ==> (forall y :: [t1].
          map_{t1}_{t4} g y =
          map2_{t2}_{t4} q (map_{t1}_{t2} f y))

Теперь давайте выберем t2 = t1 и f = id:

forall t1 in TYPES.
 forall t4 in TYPES, g :: t1 -> t4.
   forall q :: t1 -> t4.
    (forall x :: t1. g x = q x)
    ==> (forall y :: [t1].
          map_{t1}_{t4} g y =
          map2_{t1}_{t4} q (map_{t1}_{t1} id y))

По закону функтора map:

forall t1, t4 in TYPES.
   forall g :: t1 -> t4, q :: t1 -> t4.
    g = q
    ==> (forall y :: [t1].
          map_{t1}_{t4} g y =
          map2_{t1}_{t4} q y)

что значит

forall t1, t4 in TYPES.
 forall g :: t1 -> t4.
    (forall y :: [t1].
          map_{t1}_{t4} g y =
          map2_{t1}_{t4} g y)

что значит

forall t1, t4 in TYPES.
          map_{t1}_{t4} = map2_{t1}_{t4}

Подводя итог:

Если map2 - это любая функция с полиморфным типом (a → b) → [a] → [b] и такая, что она удовлетворяет первому закону функтора map2 id = id, тогда map2 должна быть эквивалентна стандартной функции map.

Также см. Сообщение в блоге Эдварда Кметта.

Обратите внимание, что в Scala вышеприведенное верно только в том случае, если вы не используете x.isInstanceOf[] и другие инструменты отражения, которые могут нарушить параметричность.