Закон для типа [[a]] -> ([a], [a])

Question

Я пытаюсь ответить на этот вопрос из своей домашней работы:

Учитывая произвольный foo :: [[a]] -> ([a], [a]), запишите один закон, что функция foo удовлетворяет, включая map по спискам и парам.

Некоторый контекст: я учусь на первом курсе курса функционального программирования. Хотя курс носит довольно вводный характер, преподаватель упомянул многие вещи вне учебной программы, в том числе бесплатные теоремы. Итак, после попытки прочесть статью Вадлера я решил, чтоconcat :: [[a]] -> [a] с законом map f . concat = concat . map (map f) похоже на мою проблему, так как мы должны иметь foo xss = (concat xss, concat' xss) где concat а также concat' какие-либо функции типа [[a]] -> [a]. потомfoo удовлетворяет bimap (map f, map g) . foo = \xss -> ((fst . foo . map (map f)) xss, (snd . foo . map (map g)) xss).

Этот "закон" уже кажется слишком длинным, чтобы быть правильным, и я тоже не уверен в своей логике. Я подумал об использовании бесплатного онлайн-генератора теорем, но не понял, чтоlift{(,)} средства:

forall t1,t2 in TYPES, g :: t1 -> t2.
 forall x :: [[t1]].
  (f x, f (map (map g) x)) in lift{(,)}(map g,map g)

lift{(,)}(map g,map g)
  = {((x1, x2), (y1, y2)) | (map g x1 = y1) && (map g x2 = y2)}

Как мне понять этот вывод? И как мне вывести закон для функцииfoo должным образом?

Answer 1

Если R1 а также R2 отношения (скажем, R_i между A_i а также B_i, с участием i in {1,2}), тогда lift{(,)}(R1,R2) пары "приподнятых" отношений, между A1 * A2 а также B1 * B2, с участием * обозначение продукта (написано (,) в Haskell).

В поднятом отношении две пары (x1,x2) :: A1*A2 а также (y1,y2) :: B1*B2 связаны тогда и только тогда, когда x1 R1 y1 а также x2 R2 y2. В твоем случае,R1 а также R2 функции map g, map g, поэтому подъем также становится функцией: y1 = map g x1 && y2 = map g x2.

Следовательно, сгенерированный

(f x, f (map (map g) x)) in lift{(,)}(map g,map g)

означает:

fst (f (map (map g) x)) = map g (fst (f x))
AND
snd (f (map (map g) x)) = map g (snd (f x))

или, другими словами:

f (map (map g) x) = (map g (fst (f x)), map g (snd (f x)))

который я напишу как, используя Control.Arrow:

f (map (map g) x) = (map g *** map g) (f x)

или даже в безточечном стиле:

f . map (map g) = (map g *** map g) . f

Это не удивительно, так как ваш f можно записать как

f :: F a -> G a
where F a = [[a]]
      G a = ([a], [a])

а также F,G являются функторами (в Haskell нам нужно будет использовать newtypeдля определения экземпляра функтора, но я опущу это, поскольку это не имеет значения). В таком общем случае теорема о свободе имеет очень красивый вид: для каждогоg,

f . fmap_of_F g = fmap_of_G g . f

Это очень красивая форма, называемая естественностью (fможно интерпретировать как естественное преобразование в подходящую категорию). Обратите внимание, что дваfВышеупомянутые типы фактически создаются для отдельных типов, чтобы типы соответствовали остальным.

В вашем конкретном случае, поскольку F a = [[a]], это состав [] функтор с самим собой, поэтому (что неудивительно) получаем fmap_of_F g = fmap_of_[] (fmap_of_[] g) = map (map g).

Вместо, G a = ([a],[a]) композиция функторов [] а также H a = (a,a)(технически диагональный функтор, составленный с помощью функтора произведения). У нас естьfmap_of_H h = (h *** h) = (\x -> (h x, h x)), откуда fmap_of_G g = fmap_of_H (fmap_of_[] g) = (map g *** map g).

Answer 2

То же, что и ответ @chi с меньшей церемонией:

Неважно, если вы измените aс к bs до или после функции, вы получите то же самое (если вы используете fmap-как-то, что нужно сделать).

Для любого f: a -> b,

    [[a]] -------------> [[b]]
      | (карта) f |
      | |
     фу фу
      | |
      vv
    ([a],[a]) ---------> ([b],[b])
              bimap ff

ездит на работу.