Про свободные теоремы

[deniok]

Свободная теорема - это содержательное тождество, которое следует из типа любой параметрически полиморфной функции в полиморфно типизированном лямбда-исчислении. В "простых" полиморфных системах (вроде System F) свободные теоремы выполняются безусловно. В более богатых системах, например, в Хаскелле, имеются некоторые ограничения, возникающие из-за наличия в языке примитивов неограниченной рекурсии fix и строго вычисления seq, подробности см. [Johann06].


Свободная теорема для любой полиморфной функции с типом

t :: [a] -> [a]

имеет вид

map g (t xs) == t (map g xs)

где g - совершенно произвольная функция, а xs - список, передаваемый в t в качестве аргумента. Например, взяв в качестве t функцию tail, в качестве g функцию succ, а в качестве xs список [1,2,3,4], получим

map succ (tail [1,2,3,4]) 
== map succ [2,3,4]
== [3,4,5]

tail (map succ [1,2,3,4])
== tail [2,3,4,5]
== [3,4,5]

Свободная теорема для

t :: [a] -> [a]

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

          t
     [a] --> [a]                a
      |       |                 | 
 map g|       |map g            |g
      v       v                 v
     [b] --> [b]                b
          t

Здесь g :: a -> b, а t, как параметрически полиморфная функция, может действовать на список любого типа: хоть [a], хоть [b]. Коммутативность таких квадратов есть следствие теоремы параметричности [Reynolds83], [Wadler89], [Johann06]. В терминах теории категорий полиморфная функция t - это естественное преобразование функтора списка в функтор списка.

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

t :: Functor fl, Functor fr => fl a -> fr a

тогда квадрат

            t
      fl a --> fr a                a
       |         |                 | 
fmapl g|         |fmapr g          |g
       v         v                 v
      fl b --> fr b                b
            t

даст свободную теорему

fmapr g (t x) == t (fmapl g x)

(Хотя в Хаскелле можно было бы использовать универсальное имя fmap для класса типов Functor, удобнее различать поведение разных функторов - отсюда обозначения fmapl и fmapr.)

В качестве примера можно привести функцию maybeToList. Она имеет тип Maybe a -> [a], что даёт свободную теорему

map g (maybeToList mv) == maybeToList (fmap g mv)

Взяв в качестве g функцию succ, а в качестве mv величину, например, Just 41, получим ожидаемый результат и в левой и в правой частях равенства (проверьте это).

Свободные теоремы полезно записывать в бесточечном стиле - это позволяет глубже проникнуть в их естество:) Первый шаг на этом пути для случая с двумя произвольными функторами очевиден - избавиться от экземпляра x функтора fl a. Это даст

fmapr g . t == t . fmapl g

Следующий шаг - избавление от t. Для этого воспользуемся сечениями композиции

fmapr g . t 
==(fmapr g .) t

t . fmapl g 
== (. fmapl g) t

Имеем свободную теорему для типа fl a -> fr a в виде сечений

(fmapr g .) == (. fmapl g)

(В качестве упражнения попробуйте избавиться и от g.)

Определим наиболее общие типы левой и правой частей последней версии нашей свободной теоремы. В стандартном контексте g :: a -> b имеем

(fmapr g .) :: Functor fr => (d -> fr a) -> d -> fr b
(. fmapl g) :: Functor fl => (fl b -> e) -> fl a -> e

Наивная унификация даст наиболее общий из возможных типов первого ранга

(Functor fl, Functor fr) => (fl b -> fr b) -> fl b -> fr b

К сожалению, это не то, что нам нужно: тип g станет окажется менее общим, чем хотелось бы, а именно b -> b. Однако, переходя к типам второго ранга, легко написать нужный нам тип, подходящий для обоих выражений

(fmapr g .) :: (Functor fl, Functor fr) => 
  (forall c . fl c -> fr c) -> fl a -> fr b
(. fmapl g) :: (Functor fl, Functor fr) => 
  (forall c . fl c -> fr c) -> fl a -> fr b

Несколько упражнений.

Проверьте, что для указанных типов имеют место приведённые свободные теоремы. Выведите "грамотно унифицированный" тип обеих частей равенства.

[[a]] -> [a]
(map g .)  ==  ( . map (map g))

(Functor flo, Functor fli, Functor fr) =>
  flo (fli a) -> fr a
(fmapr g .)  ==  ( . fmaplo (fmapli g))

[a] -> [a] -> [a]
((map g .) .)  ==  ((. map g) .) . (. map g)

(Functor fl, Functor fc, Functor fr) =>  fl a -> fc a -> fr a
((fmapr g .) .)  ==  ((. fmapc g) .) . (. fmapl g)

Здесь g :: a -> b - совершенно произвольная функция, а fmapXXX - это fmap для функтора fXXX.



PS. Ну и чтобы всё было в одном месте - автоматический генератор свободных теорем.

Comments

[ro-che.info (from livejournal.com)]

А в каком смысле они свободные?

Разве "free" в "free theorems" не употребляется в смысле "бесплатные"? (Хотя "бесплатные теоремы" тоже звучит странно.)

[deni-ok.livejournal.com]

Ещё был вариант "халявные" :)

[zelych.livejournal.com]

А они разве не свободные в смысле http://en.wikipedia.org/wiki/Free_object ?
Т.е. свободны от нелогических аксиом.

осторожно, текст выше может не нести никакого смысла

[ro-che.info (from livejournal.com)]

Parametricity, наверное, имеет какие-то связи со свойством быть свободным в категорном смысле, но чтоб сами теоремы образовывали категорию (и потому какие-то теоремы могли бы быть свободными) -- такого не слышал.

У Вадлера в abstract говорится "This provides a free source of useful theorems [...]", так что, видимо, это и есть обоснование названия free.

[alogic.livejournal.com]

Можно прямо в википедию постить. Там как раз статья про "бесплатные теоремы" пустая
Естественное_преобразование

[deni-ok.livejournal.com]

В русской википедии и более фундаментальных вещей нету, например, собственно System F.

[alogic.livejournal.com]

Если там хоть что-то есть, уже польза. Я могу и сам ваш пост туда поместить, если вы не против.

[deni-ok.livejournal.com]

Не против, конечно. Только, вроде, меня почти убедили, что "бесплатные" лучше.