имхо, [для обучения программировать] достаточно всего двух пунктов: итерация ; ветвление
чтобы был иллюстративный материал, тоже два пункта: комбинаторика ; алгебраические структурыостальное нахрен не нужно
Андрей Мельников к Максиму Сохацкому
December 1 2014, 19:27:12 UTC
John Harrison
забудем про операции ввода-вывода и допустим, что программа работает конечное время, производя какой-либо результат. рассмотрим выполнение в абстрактном виде:
σ0 → σ1 → σ2 → · · · → σnпрограмма начинает работу с начального состояния σ0, содержащего входные значения для программы
избегая использования переменных и операций присваивания, мы получаем следующие преимущества:
чтобы создать надлежащую семантику для императивных методов, нам необходимо явно определить состояние. например, мы можем создавать команды как:
даже если позволить существование goto, то этого все-равно мало и нам еще нужна семантика, основанная на продолжениях
все эти методы достаточно сложны, но в функциональных программах у нас есть возможность проверить их корректность, а также корректность некоторых преобразований и оптимизаций
λ-нотация – это способ определения функций, предложенный Алонзо Чёрчем. мы пишем:
λx. Eчтобы определить «функцию от x, которая возвращает E». здесь E – это выражение, которое содержит или не содержит x. если оно содержит х, то х является связанной переменной , а если не содежит - то х называется свободной переменной
используя только:
возможности λ-нотации полезны для унификации понятия связанных переменных . в математике переменные обычно выражают зависимость некоторого выражения от значения этой переменной
в логике применяются кванторы ∀x.P[x] и ∃x.P[x]; в теории множеств — абстрактные множества, наподобие {x|P[x]}, а также индексированные объединения и пересечения
в таких случаях говорят, что переменная должна быть связанной (bound)
при использовании λ-нотации выражения λx.E[x] и λy.E[y] являются эквивалентными; это называется альфа-эквивалентностью , а процесс преобразования одного выражения в другое — альфа-преобразованием . следует особо оговорить, что переменная y не должна быть свободной в выражении E[x], иначе его значение изменится
λ-абстракция выглядит как подходящий примитив, в терминах которого проводится анализ связывания переменных. эта идея уходит корнями к записи логики высшего порядка в λ-нотации, использованной Чёрчем. идея использования λ-нотации в качестве универсального абстрактного синтаксиса была введена Мартином-Лёфом
основой λ-исчисления служит формальное понятие λ-термов, которые строятся из переменных и некоторого фиксированного множества констант при помощи операций применения (аппликации) функций и λ-абстракции. это значит, что всевозможные λ-термы разбиваются на четыре класса:
λ-термы строятся по индукции. это может быть выражено следующей грамматикой BNF:
Exp = Var | Const | Exp Exp | λ Var. Expтак как синтаксис задан по индукции, то мы можем определять сущности с помощью примитивной рекурсии и доказывать сущности с помощью структурной индукции
обозначим множество свободных переменных в терме s через FV(s) и дадим его рекурсивное определение:
FV (x) = {x} FV (c) = ∅ FV (s t) = FV (s) ∪ FV (t) FV (λx. s) = FV (s) − {x}аналогично вводится и понятие множества связанных переменных BV(s):
BV (x) = ∅ BV (c) = ∅ BV (s t) = BV (s) ∪ BV (t) BV (λx. s) = BV (s) ∪ {x}
одним из правил является соглашение о том, что λ-абстракция и применение функции представляют собой взаимно обратные операции. то есть, если мы возьмём терм λx.s и применим его как функцию к терму-аргументу t, результатом будет терм s, в котором все свободные вхождения переменной x заменены термом t
обозначим операцию подстановки терма s вместо переменной x в другой терм t как t[s/x]
x[t/x] = t y[t/x] = y, если x != y c[t/x] = c (s1 s2)[t/x] = s1[t/x] s2[t/x] (λx.s)[t/x] = λx. s (λy.s)[t/x] = λy.(s[t/x]), x != y и либо x !∈ FV(s), либо y !∈ FV(t) в противном случае λz.(s[z/y][t/x]), z !∈ FV(s) ∪ FV(t)
ещё одной из основ λ-исчисления служат три «преобразования» — операции получения по заданному терму другого, равного ему в интуитивном смысле. традиционно их обозначают буквами греческого алфавита: α (альфа), β (бета) и η (эта)
пример β-редукции:
fst (M , N) ==> M
snd (M , N) ==> N
(λx.M) N ==> M[N/x]
пример μ-редукции:
M : A ✗ B ==> (fst M , snd M) M : A -> B ==> (λx. M x) : B
η-преобразование воплощает принцип экстенсиональности. два свойства называются экстенсионально эквивалентными, если этими свойствами обладают в точности одни и те же объекты. в теории множеств принята аксиома экстенсиональности, согласно которой два множества совпадают, если они состоят из одних и тех же элементов. аналогично, будем говорить, что две функции эквивалентны, если области их определения совпадают, а значения функций для всевозможных аргументов также одинаковы
введение η-преобразования делает наше понятие λ-эквивалентности экстенсиональным. в самом деле, пусть f x и g x равны для произвольного значения x; в частности, f y = g y, где переменная y выбирается так, чтобы она не была свободной как в f, так и в g
согласно последнему из приведённых выше правил эквивалентности, λy.f y = λy.g y
применив дважды η-преобразование, получаем, что f = g
из экстенсиональности следует, что всевозможные η-преобразования не нарушают эквивалентности, поскольку согласно правилу β-редукции (λx.t x) y = t y для произвольного y, если переменная x не является свободной в терме t
s →α t или s →β t или s →η t ---------------------------- s = t ----- t = t s = t ----- t = s s = t и t = u ------------- s = u s = t -------- s u = t u s = t --------- u s = u t s = t ------------- λx. s = λx. t
программа на функциональном языке представляет собой выражение, а её выполнение — вычисление этого выражения. то есть, в терминах, изложенных выше, мы собираемся начать процесс вычислений с соответствующего терма и применять к нему правила редукции до тех пор, пока это возможно. нормальные формы, если они существуют, являются единственными с точностью до α-преобразования. это даёт нам первое обоснование того, что отношение λ-эквивалентности нетривиально, т. е. что существуют неэквивалентные термы. например, поскольку λx y.x и λx y.y несводимы друг к другу исключительно при помощи α-преобразований, они не эквивалентны
будем называть комбинатором терм λ-исчисления без свободных переменных. такие термы также принято называть замкнутыми , поскольку их значение не зависит от значений каких-либо переменных. оказывается, что произвольный терм может быть выражен при помощи определённого множества комбинаторов и всевозможных переменных, операция λ-абстракции становится ненужной. в частности, замкнутый терм может быть представлен исключительно через эти комбинаторы. дадим их определения:
I = λx. x K = λx y. x S = λf g x. (f x)(g x)
чтобы легче их запомнить, можно воспользоваться простыми мнемоническими правилами:
комбинатор I представляет собой тождественную функцию («идентичность»)
комбинатор K порождает семейство константных функций: после применения к аргументу 'a' он даёт функцию 'λy.a'
S — комбинатор «совместного применения», который принимает в качестве аргументов две функции, применяемые к общему аргументу
на самом деле достаточно использования S и K, ибо I = S K K
кажется, что сложно определить рекурсивную функцию не задав ей имени. однако, мы можем это сделать, используя комбинаторы неподвижной точки
говорят, что Y – комбинатор неподвижной точки, если, применив его к функции f , мы получим неподвижную точку x для f, то есть такое x, что f(x)=x. для всех f имеем:
f (Y f) = Y f
Как альтернативу Y , можно задать выражение:
T = (λx y. y (x x y)) (λx y. y (x x y))оно имеет более сильное свойство: T f → f (T f )
так что же всё-таки «термы» означают в λ-исчислении? какой смысл в применении функции к самой себе, как в f f? некоторый смысл есть для таких функций, как тождество λx.x или константная функция λx.y, но, в основном, это выглядит подозрительно
допустим, что у нас есть некий набор константных типов, например int и bool, и мы можем создавать из них новые типы, используя
в общем случае у нас может быть сколь угодно много конструкторов типов и любое количество констант, типы которых содержат эти конструкторы
мы думаем о типах, как о множествах, в которых объекты обозначаются термами, и t:σ читается как t∈σ - это система явных типов. однако предпочительнее использовать неявную типизацию, когда мы используем контекст Γ, который задаёт назначение типов для переменных и констант:
Γ |- t : σ
в типизированном λ-исчислении у любого типизируемого терма есть нормальная форма, и все последовательности редукций завершаются на нормальной форме. это свойство называется сильной нормализацией. это замечательно — любая программа завершается. однако, это означает, что мы не можем написать все вычислимые, или даже все интересные, функции. мы не можем определять произвольные рекурсивные функции, иначе мы смогли бы определить функцию, которая никогда не завершается
нормальный порядок редукции («вызов по имени») является наилучшей редукционной стратегией, потому что если хоть какая-то стратегия завершается, то эта тоже. однако, встаёт вопрос эффективности:
(λx. x + x + x) (10 + 5)
нормальный порядок редукции даст
(10 + 5) + (10 + 5) + (10 + 5)
и нам придётся три раза вычислять одно и тоже выражение! было бы эффективнее сначала вычислить аргумент 10 + 5. существует два решения проблемы, которые делят мир функционального программирования на части:
ленивое вычисление выполняет нормальный порядок редукции, но имеет хитрые способы совместного использования выражений, сохраняя их в виде графа (не)вычисленных термов. при таком способе выражения вычисляются только один раз и только когда это понадобится
энергичное вычисление просто вычисляет сперва аргументы («аппликативный порядок редукции»), и программист должен следить, чтобы не было зацикливаний
в некотором роде ленивое вычисление элегантнее и мощнее. однако, его не так просто реализовать
тестирование программ может быть полезным для демонстрации наличия ошибок, но показать их отсутствие оно в состоянии лишь в отдельных редких случаях. альтернатива тестированию это верификация, когда мы пытаемся доказать, что программа работает так, как требуется. для функциональных программ легче проводить формальное доказательство, потому что они напрямую соответствуют математическим функциям, которые они представляют, но надо помнить, что в основном функциональные программы это частичные функции - иногда требуется отдельное доказательство завершимости вычислений
Дмитрий Попов
возьмем логику высказываний и логическую связку ИЛИ (|) оттуда, дизъюнкцию. ее определением служат правила Intro и Elim
правила Intro:
если доказана достоверность высказывания А, то доказана и достоверность А|В
если доказано В, то также доказано А|В
правило Elim:
если доказаны импликации А=>C и В=>С и доказано А|В, то доказана достоверность С
очень похоже выглядит сумма двух типов в ЯП (в Хаскеле это Either a b
что можно с такими значениями делать, кроме как где-то хранить и куда-то передавать? можно только одно - использовать в выражении case
(и сводящемся к нему паттерн-матчинге)
конструкция case
берет по сути две функции:
обе они возвращают результат одного типа "с", этот тип становится типом всего выражения case
h :: Either Int String -> Float h x = case x of Left i -> fromIntegral i + 2.0 Right s -> read s + 3.0
сходство суммы типов и связки ИЛИ кристаллизуется в категорном определении суммы:
объект sum(А,В) называется суммой объектов А и В, если
"диаграмма коммутирует" означает, что если на ней между двумя точками (объектами) есть несколько различных путей, то неважно каким путем двигаться из первой точки во вторую, результат будет одинаковый. применим ли мы сразу fromIntegral i + 2.0
Left
, а затем разберем через case
и ту же функцию - результат один. воспользуемся ли сразу импликацией А => С
для вывода С из доказанного А или сперва выведем достоверность А|В
, а затем с помощью той же импликации и правила избавления от | выведем С, результат не изменится
если у нас есть объект sum(A,B), то что можно сказать о sum(B,A)?
это какой-то другой объект, но в него тоже есть стрелки из А и В, а значит должна быть стрелка из sum(A,B) в sum(B,A), этого требует определение. назовем ее f1. аналогично, должна быть и стрелка из sum(B,A) в sum(A,B), назовем ее f2. тогда их композиция f2 . f1
есть стрелка из sum(A,B) в sum(A,B)
в категории у каждого объекта есть стрелка id в самого себя, а поскольку обсуждаемые стрелки тут таковы, что получаемые диаграммы с ними должны коммутировать, то не важно, попадем мы из sum(A,B) в себя по стрелке id или по стрелке f2.f1, а значит f2.f1=id
обратная композиция, f1.f2 аналогично идет из sum(B,A) в sum(B,A) и по тем же соображениям f1.f2=id т.е. f1 и f2 - изоморфизмы, они делают объекты sum(A,B) и sum(A,B) изоморфными. для теории категорий такие объекты - близнецы-братья, т.к. все связи одного объекта автоматически есть и у другого, ибо определение категории требует наличие стрелки-композиции для каждой пары последовательных стрелок
мы только что показали коммутативность сложения: sum(A,B) == sum(В,А), где == означает изоморфность
в категории, где объекты - типы данных, а стрелки - функции, изоморфность означает не равенство типов, а эквивалентность в том, какую информацию значения этих типов содержат. изоморфность означает наличие стрелок-изоморфизмов, композиция которых равна id, а значит между такими типами должны существовать функции конверсии такие, что их композиция не теряет информации: сконвертив значение туда-обратно мы получим его же без изменений
мы выше определили, что right и left - это стрелки типов b -> sum(a,b)
и a -> sum(a,b)
тип f1: sum(a,b) -> sum(b,a)
соответственно, f1.f1
будет иметь тип sum(a,b) -> sum(a,b)
, а значит f1.f1=id
(диаграмма должна коммутировать), и f1 - морфизм, доказывающий изоморфность этих двух объектов
и при переводе на Хаскель это превращается в:
f1 :: Either a b -> Either b a f1 x = case x of Left a -> Right a Right b -> Left b
в логике высказываний таким объектом выступает особое высказывание ⊥ - "абсурд". его нельзя построить конструктивно (нет правила ввода), зато из него есть импликации во все возможные высказывания (из абсурда следует что угодно)
в теории типов это пустой тип ⊥
, у которого нет значений. у него нет особенных стрелок кроме универсального морфизма в каждый из объектов категории
тождественный морфизм, имеющийся у каждого объекта: I : a -> a
т.е. для любого объекта А есть стрелка из А в А. а по определению суммы, из А есть стрелка left в А+0. и поскольку эти стрелки таковы, что соответствующие диаграммы обязаны коммутировать, наличие стрелок из А в А+0 и обратно опять нам дает изоморфизм, поэтому А+0 == А (я для простоты буду писать А+В вместо sum(A,B)). значит, инициальный объект 0 - нейтральный элемент для сложения
в логике это превращается в знакомое правило P | False == P
в типах Either a ⊥ == a
(ведь значения типа слева всегда будут вида Left х
, ибо в Right нам подставить нечего)
соответственно, произведением объектов А и В называется такой объект prod(A,B), из которого есть стрелки в А и в В (назовем их fst и snd), и для любого похожего объекта С (из которого тоже есть стрелки в А и В) есть уникальная стрелка pair из С в prod(A,B):
опять, диаграмма должна коммутировать, т.е. fst.pair(f,g) = f и т.д.
ровно те же рассуждения что и с суммой позволяют показать коммутативность произведения
тип prod(a,b) -> prod(b,a)
служит изоморфизмом между А*В и В*А, доказывающим их изоморфность
в логике произведением служит связка И, в категории типов - тупл
в логике высказываний это особое высказывание "верно"
в ЯП это тип unit
(он же ()
), с единственным значением ()
. его построить можно из чего угодно, функция f x = ()
служит стрелкой из любого типа в ()
ее тип: a -> ()
как несложно догадаться, терминальный объект для произведения подобен инициальному для копроизведения - это нейтральный элемент, т.е. А*1 == А
выражение "pair(I, ())" имеет тип a -> prod(a,1)
, а fst дает обратную стрелку из prod(a,1) в a. композиции их дают стрелки из a в a и из prod(a,()) в prod(a,()), т.е. это изоморфизмы, и действительно А*1 == А
в категории с числами и делимостью 1 - это само число 1, на него делятся все натуральные числа. получаем знакомые соотношения
(a, ()) == a
P & True == Р
lcm(a, 1) = a
в логике это импликация (A => B) , в ЯП это функциональный тип (a -> b)
в категории с экспоненциалами можно доказать дистрибутивность умножения относительно сложения.
стрелка d1 типа sum (prod(a,b) , prod(a,c)) -> prod (a , sum(b,c))
, т.е. из
d1 :: Either (a,b) (a,c) -> (a, Either b c) d1 x = (a,b) where a = case x of Left p -> fst p ; Right p -> fst p b = case x of Left p -> (Left . snd) p ; Right p -> (Right . snd) p
а вот так можно определить обратную:
d2 :: (a, Either b c) -> Either (a,b) (a,c) d2 x = ((cs . snd) x) (fst x) where cs s = case s of Left b -> \a -> Left (a,b) Right c -> \a -> Right (a,c)
стрелка d2 типа prod (a , sum(b,c)) -> sum (prod(a,b) , prod(a,c))
, т.е. это стрелка из
вместе d1 и d2 служат изоморфизмами, доказывая A*(B+C) == A*B+A*C, дистрибутивность
конечно, d2 можно записать проще:
d2' :: (a, Either b c) -> Either (a,b) (a,c) d2' (a, e) = case e of Left b -> Left (a, b) Right c -> Right (a, c)
но загвоздка в том, что в категорном определении case он параметризуется стрелками (функциями): одна стрелка здесь должна уметь из значения "b" сделать Left(a,b), а вторая из "с" сделать Right(a,c), но где им для этого взять "а"? по сути, эти функции в d2' - замыкания, они берут значение "а" из окружения. приходится их реализовать более явно: не имея значения "а", мы возвращаем не Left(a,b), а функцию, которая из "a" сделает Left(a,b). аналогично с Right(a,c)
тип у этих двух возвращаемых функций одинаковый, и он становится типом всего выражения case. и возвращенная им функция уже применяется к параметру типа "а", взятому из исходной пары. именно поэтому нам потребовались экспоненциалы
раз уж у нас появился экспоненциал, докажем кое-какие его свойства
напомню, что exp(A,B) означает для ЯП тип функции А -> В
, для логики импликацию А => В
, но экспоненциалом называется в силу схожести с В^A - "В в степени А". от возведения в степень разумно ожидать, что А^1=A и 1^A=1 для любого А, т.е. exp(1,A) == А и exp(A,1) == 1
e1 имеет тип exp(1,a) -> a, т.е. дает нам стрелку из А^1 в A
e2 имеет тип a -> exp(b, prod(a,b)), для любых объектов А и В е2 дает стрелку из А в exp(B, A*B), в частности для В=1 это стрелка из А в (A*1)^1, а про А*1 мы уже знаем, что он изоморфен А. это вроде как доказывает(?) A^1==A.
выражение е3 имеет тип a -> exp(b,1) и для произвольных объектов A и B дает стрелку из A в 1^B, в частности из 1 в 1^B. ну а стрелка из 1^B в 1 всегда есть по определению 1 как терминального объекта. и опять в силу характера этих стрелок, наличие двух стрелок туда-обратно между объектами делает стрелки изоморфизмами, а объекты изоморфными. значит, 1^A == 1 для любого А
как следствие a -> () == () для типов и (P => True) == P для логических высказываний
итого, из категорных определений произведения, копроизведения, экспоненциала, инициального и терминального объектов мы вывели как следствия такие арифметические свойства:
a+b == b+a
a*b == b*a
a+0 == 0+a == a
a*1 == 1*a == a
a*(b+c) == a*b + a*c
a^1 == a
1^a == 1
и из этого набора можно получить другие следствия. например, обозначив 1+1 за 2, получим
a*2 == a*1 + a*1 == a + a
т.е. умножение (на натуральное число) выражается через сложение не только в привычной арифметике натуральных чисел, но и в арифметике типов
кроме того можно показать, что a^2 == a*a, т.е. возведение в натуральную степень выражается через произведение. необходимые изоморфизмы на хаскеле выглядят так:
type Two = Either () () p1 :: (a,a) -> (Two -> a) p1 (a,b) = \i -> case i of { Left _ -> a; Right _ -> b } p2 :: (Two -> a) -> (a,a) p2 f = (f (Left ()), f (Right ()))
вот такая вот арифметика
я всех обманул. я сказал, что если на коммутирующей диаграмме между двумя объектами есть стрелки туда-сюда, то они получаются изоморфизмами. однако ж нифига, и вот простой контрпример.
возьмем объект А и его произведение с самим собой АхА:
по определению произведения из АхА есть
pair(id,id)
имеет тип a -> prod(a,a)
, а fst
имеет тип prod(a,b) -> a
, и их композиция fst . pair(id,id)
равна id
, это нам дает определение произведения
но вот обратная композиция pair(id,id) . fst
нифига не равна id
, а значит, определение изоморфизма не выполнено, и А не изоморфен АхА, что и следовало ожидать. построение стрелок туда-сюда еще не доказывает изоморфность, нужно явно показать, что обе их композиции равны соответствующим id
упомянутые в прошлом изоморфизмы остаются в силе, просто обоснования там неполные, не хватает кое-каких доказательств
нужно иметь в уме, или перед глазами, определение изоморфности двух объектов в категории: для доказательства изоморфности нужно не только построить стрелки из одного объекта в другой и обратно, но и показать, что композиции стрелок, претендующих на роль изоморфизмов, действительно равны id
Idris:
interface Functor (f : Type -> Type) where map : (m : a -> b) -> f a -> f b
функтор - это особенный тип функций. это функция на алгебрах. говоря точнее, это функция, которая отображает одну алгебру на другую алгебру
то есть, однажды построив алгебру на типе А, с помощью функтора вы можете перенести ее на тип В
OCaml:
(* funct.ml *) module type Functor = sig type 'a t val map : ('a -> 'b) -> 'a t -> 'b t end module OptionF : Functor with type 'a t = 'a option = struct type 'a t = 'a option let map f = function | Some a -> Some (f a) | _ -> None end module IntToOpt (A: Functor) = struct let dblInt x = x * 2 let dblOpt x = A.map dblInt x end module D = IntToOpt (OptionF) ;; let t1 = D.dblOpt (Some 5) ;; let t2 = D.dblOpt None ;;
$> ocaml OCaml version 4.03.0 # #use "funct.ml";; module type Functor = sig type 'a t val map : ('a -> 'b) -> 'a t -> 'b t end module OptionF : sig type 'a t = 'a option val map : ('a -> 'b) -> 'a t -> 'b t end module IntToOpt : functor (A : Functor) -> sig val dblInt : int -> int val dblOpt : int A.t -> int A.t end module D : sig val dblint : int -> int val dblOpt : int OptionF.t -> int OptionF.t end val t1 : int OptionF.t = Some 10 val t2 : int OptionF.t = None
чтобы ваше отображение было функтором, необходимо соблюсти два условия:
второе условие иногда применяют непосредственно в коде и называют в этом случае fusion
резюмируя: функтором называется отображение одной категории в другую, сохраняющее структуру - "рисунок" стрелок. он всякому объекту из первой категории сопоставляет некоторый объект из второй, и стрелки переносит соответственно
конструкторы типов, вроде списка или дерева, - примеры функторов
функтор "список" ('a list
) отображает типы вроде int
и string
в типы вроде int list
и string list
,
а функции вроде int -> string
int list -> string list
все полиморфные функции, вроде head
и tail
для списков, fst
и snd
для туплов, - это естественные преобразования. они работают с формой структуры данных, не трогая ее наполнение, не зная конкретного её типа, т.е. превращают один функтор в другой
Дмитрий Попов
вот такая программа на Хаскеле вычисляет и выводит ответ на жизнь, вселенную и вообще:
import Control.Applicative main = print $ answer succ 0 where one = pure <*> (pure :: a -> b -> a) inc = (<*>) ((<*>) <$> pure) mul = (<*>) <$> pure h = mul <*> inc answer = h . h . h $ one
аппликативный функтор характеризуется наличием двух функций:
class Functor f => Applicative f where pure :: a -> f a (<*>) :: f (a -> b) -> f a -> f b
фишка в том, что для ((->) a) эти две функции - комбинаторы K и S
instance Applicative ((->) a) where pure = const (<*>) f (g x) = f x (g x)
мы знаем, что через S и K можно выразить любую лямбда-функцию. возьмем, например, функцию
h x = x * (x + 1)
задействуем числа Черча: число представляется функцией, которая берет другую функцию и ее аргумент, и применяет ту функцию n раз. так, единица применяет другую функцию f один раз:
one f x = f x
чтобы увеличить число n на 1, нужно применить f на один раз больше, чем это делает n:
inc n f x = f (n f x)
умножение a на b делается применением b a раз:
mul a b f x = a (b f) x
x тут можно "сократить" и не писать. тогда h будет выглядеть как
h x = mul x (inc x)
теперь возьмем комбинаторный базис:
s x y z = (x z) (y z) k x y = x
пользуясь простым алгоритмом конверсии, наши арифметические функции можно выразить через S и K:
one = s k k inc = s (s (k s) k) mul = s (k s) k h = s mul inc
теперь осталось лишь вспомнить, что
k = pure s = <*> pure x <*> y = x <$> y
подставив их вместо S и K, получим программу
представляете, какие открываются горизонты? я тоже нет. разве что обфускатор можно написать. :)
comments
одноточечный универсальный базис слабо =) ?
аппликативный функтор - это функтор, "переносящий" лямбда-исчисление из одной категории в другую, - так его определили
метод "переноса" заключается в том, что мы можем переписать лямбда-выражения через S и K комбинаторы и заменить их на <*> и pure
в исходной работе по аппликатианым функторам (“Applicative programming with effects”, Conor McBride, Ross Paterson) для <*> и pure используются обозначения \mathbb{S} и \mathbb{K}, и написано прямым текстом: «This class generalises S and K from threading an environment to threading an effect in general»
у аппликативных функторов возможен и _другой_ интерфейс, связь которого с комбинаторной логикой менее очевидна;
в той же работе объясняется, что аппликативный функтор - это strong lax monoidal functor, т.е. вместо S и K его можно снабжать тензорным произведением и тензорной силой, эффект будет тот же
можно кстати сделать интерфейс через одноточечный базис комбинаторной логики навроде X; но неудобно
с чего бы?
inc = S (S (K S) K)
mul = S (K S) K
я тоже как-то не мог понять, и в виде
зато раз x можно "сократить", то выходит
(даже больше:
полиморфизм!
Prelude> let h = inc inc
Prelude> (h . h . h $ one) (+1) 0
42
хотя типы ghci выводит разные для inc и s mul
если задать слишком строго (т.е. не сокращать x в типе), то хотя всё равно реализация
категория морфизмов, в которой id-морфизм является единичным элементом, а композиция морфизмов - бинарной операцией, является моноидом
категория, где все морфизмы обратимы, называется группоидом