Дао функционального программирования
В этом разделе приведены решения упражнений из книги Бартоша Милевски "Дао функционального программирования".
Упражнение 2.1.1.
Предположим, имеются стрелки, \(f : a \to b\) и \(g : b \to c\). Их композиция \(g \circ f\) индуцирует отображение стрелок \(((g \circ f) \circ -)\). Покажите, что результат будет таким же, если сначала применить \((f \circ -)\), а затем \((g \circ -)\). Формально: \(((g \circ f) \circ -) = (g \circ −) \circ (f \circ −)\)
Подсказка: выберите произвольный объект x и стрелку \(h : x \to a\), и посмотрите, получится ли один и тот же результат. Обратите внимание, что \(\circ\) здесь перегружен. Это означает регулярную функциональную композицию, когда она помещается между двумя посткомпозициями.
Композиция \(g \circ f\) отображает стрелки идущие к a на стрелки идущие к c (\(g \circ f : a \to b \to c\)). \((f \circ -)\) отображает стрелки идущие к a на стрелки идущие к b. \((g \circ -)\) отображает стрелки идущие к b на стрелки идущие к c.
Возьмем произвольный объект x и стрелку \(h : x \to a\).
Применим \(((g \circ f) \circ h)\) к x: \((g \circ f)(h(x)) = (g \circ f)(a) = c\).
Применим \((f \circ -)\), а затем \((g \circ -)\) к x: \(((g \circ −) \circ (f \circ −)(h(x))) = (g \circ −)(f(a)) = g(b) = c\)
Упражнение 2.1.2.
Проверьте, что композиция из предыдущего упражнения ассоциативна. Подсказка: начните с трех композируемых стрелок.
Предположим, имеются стрелки, \(f : a \to b\), \(g : b \to c\) и \(h : c \to d\). Докажем, что \((h \circ g) \circ f = h \circ (g \circ f)\). Композиция \(h \circ g\) отображает стрелки идущие к b на стрелки идущие к d, а композиция \(g \circ f\) отображает стрелки идущие к a на стрелки идущие к c.
Возьмем произвольный объект x и стрелку \(j : x \to a\).
Применим \((h \circ g) \circ f\) к x: \(((h \circ g) \circ f)(j(x)) = ((h \circ g)(f(a))) = ((h \circ g)(b)) = d\).
Применим \(h \circ (g \circ f)\) к x: \(h \circ (g \circ f)(j(x)) = h \circ (g \circ f)(a) = h(c) = d\).
Заметим, что ассоциативность композиции одной (строго говоря это не композиция) и двух стрелок очевидна.
Предположим, что доказана ассоциативность композиции n - 1 стрелок, где n > 3. Докажем, что композиция n стрелок тоже ассоциативна.
Рассмотрим первую стрелку в композиции - f. При расстановке скобок f может применяться либо в последнюю очередь, либо НЕ в последнюю очередь. Если f применяется в последнюю очередь, то композиция всех предыдущих стрелок является композицией n - 1 стрелок, а значит - ассоциативна. Т.о. не имеет значения в каком порядке мы будем компоновать стрелки, результат всегда будет одинаков. Назовем этот результат стрелкой Res.
Если f применяется не в последнюю очередь, а, скажем, в очередь k, где 1 <= k < n, то тогда разобьем композицию на три группы: композиция A, состоящая из k - 1 элемента, выполняющаяся в первую очередь, затем композиция Б, состоящая только из f и композиция В, состоящая из n - k элементов. Каждая из них ассоциативна, а значит, порядок выполнения стрелок внутри группы не имеет значения. А значит итоговая композиция равна: \((В \circ (А \circ Б))\). Но эта композиция в точности равна композиции \(((В \circ А) \circ Б)\) из-за ассоциативности трех компонуемых стрелок. Но последняя композиция соответствует одной из композиций, где f применяется в последнюю очередь - т.е. равна Res.
Получается, что композиция n стрелок ассоциативна, потому что все комбинации дают результат Res.
Упражнение 2.1.3.
Покажите, что пред-композиция \((− \circ f)\) компонуема, но порядок композиции является обратным: \((− \circ (g \circ f)) = (− \circ f) \circ (− \circ g)\)
Если применить \((− \circ (g \circ f))\) к стрелкам, исходящим из c, например, к стрелке \(h : c \to x\), направленную в произвольный элемент x, то эта стрелка сопоставляется со стрелкой \(a \to x\), потому что \(g \circ f: a \to c\), но это тоже самое, если вначале применить \((− \circ g)\) - смещение фокуса с c на b, а затем - \((− \circ f)\) - смещение фокуса с b на a. Получается та же стрелка \(a \to x\).
Упражнение 2.3.1.
Что делает \((id_{a} \circ −)\) со стрелками, оканчивающимися на a? Что делает \((− \circ id_{a})\) со стрелками, исходящими из a?
\((id_{a} \circ −)\) оставляет стрелки, оканчивающиеся на a, неизменными. Если взять произвольный элемент x и стрелку \(f : x \to a\), то тогда получим, что \((id_{a} \circ f = f)\). Аналогично со стрелками, исходящими из a - \((− \circ id_{a})\) оставляет их неизменными.
Упражнение 3.1.1.
Приведите аргумент, что существует биекция между стрелками, исходящими из двух изоморфных объектов. Изобразите соответствующие схемы.
Биекция между исходящими стрелками определяется как \((- \circ f)\) или \((- \circ f^{-1})\).
Упражнение 3.1.2.
Докажите, что каждый объект изоморфен самому себе.
Тождественная стрелка обратна сама себе, поэтому является изоморфизмом.
Упражнения 3.1.3-4.
Если имеются два терминальных объекта, покажите, что они изоморфны.
Покажите, что изоморфизм из предыдущего упражнения единственен.
Предположим, что \(i_{1}\) и \(i_{2}\) — терминальные объекты в одной и той же категории. Поскольку \(i_{1}\) терминальный, то существует единственный морфизм f от \(i_{2}\) к \(i_{1}\). Аналогично, поскольку \(i_{2}\) терминальный, то существует единственный морфизм g от \(i_{1}\) к \(i_{2}\). Композиция \(g \circ f\) должна быть морфизмом от \(i_{2}\) к \(i_{2}\). Но \(i_{2}\) является терминальным объектом, так что существует ровно один морфизм от \(i_{2}\) к \(i_{2}\) и, поскольку начало и конец стрелки совпадают, эта вакансия уже занята тождественным морфизмом. Следовательно, они должны совпадать: морфизм \(g \circ f\) является тождественным. Аналогично, морфизм \(f \circ g\) также совпадает с тождественным, поскольку может быть всего один морфизм от \(i_{1}\) к \(i_{1}\). Таким образом, f и g взаимнообратны, а два терминальных объекта изоморфны.
Упражнение 3.2.1.
Покажите, что обе части условия естественности для \(f^{−1}\), при воздействии на h, сводятся к: \(b \overset{f^{-1}}{\rightarrow} a \overset{h}{\rightarrow} x \overset{g}{\rightarrow} y\)
\((− \circ f^{−1}) \circ (g \circ −) = f^{−1} \circ g \circ (a \to x) = f^{−1} \circ (a \to y) = b \to y\)
\((g \circ −) \circ (− \circ f^{−1}) = (g \circ −) \circ (h \circ f^{−1}) = (g \circ −) \circ (h \circ (b \to a)) = (g \circ −) \circ (b \to x) = b \to y\)
Упражнение 3.3.1.
Используйте трюк с тождественным морфизмом, чтобы восстановить \(f^{−1}\) из семейства отображений \(\beta\).
???
Упражнение 3.3.2.
Используя \(f^{−1}\) из предыдущего упражнения, оцените \(\beta_{y} \circ g\) для произвольного объекта y и произвольной стрелки \(g : a \to y\).
???
Упражнение 4.1.1.
Составьте реализации трех других функций Bool -> Bool.
enum Bool:
case True, False
def alwaysTrue(b: Bool): Bool = Bool.True
def alwaysFalse(b: Bool): Bool = Bool.False
def same(b: Bool): Bool = b
def not(b: Bool): Bool =
b match
case Bool.True => Bool.False
case Bool.False => Bool.TrueУпражнение 4.4.1.
Реализуйте на Haskell две функции, образующие изоморфизм между Either + Void и a.
Реализация на Scala:
final abstract class Void()
def f[A](either: Either[Void, A]): A =
either match
case Left(value) => ??? // imposible
case Right(a) => a
def fReverse[A](a: A): Either[Void, A] = Right(a)Упражнение 4.4.2.
Покажите, что определенная выше биекция естественна. Подсказка: и f, и g, меняют фокус пост-композицией с \(k : x \to y\).
???
Упражнение 4.4.3.
Реализуйте на Haskell функцию, свидетельствующую об изоморфизме между Either a b и Either b a. Обратите внимание, что эта функция является обратной самой себе.
def f[A, B](either: Either[A, B]): Either[B, A] =
either match
case Left(a) => Right(a)
case Right(b) => Left(b)Упражнение 4.4.4.
Покажите, что функториальность сохраняет композицию.
Подсказка: возьмите две компонуемые стрелки, \(g : b \to b'\) и \(g': b' → b''\), и покажите, что применение \(g' \circ g\) дает тот же результат, что и первое применение \(g\) для преобразования \(a + b\) в \(a + b'\), а затем применяя \(g'\) для преобразования \(a + b'\) к \(a + b''\).
Применение \((g \circ g')\) к \(\textrm{Left(a)}\) приводит к \(\textrm{Left(a)}\) в тип-сумме \(a + b''\). Аналогично последовательное применение \(g\) и \(g'\) к \(\textrm{Left(a)}\) вначале приводит к \(\textrm{Left(a)}\) в тип-сумме \(a + b'\), затем - к \(\textrm{Left(a)}\) в тип-сумме \(a + b''\).
Применение \((g \circ g')\) к \(\textrm{Right(b)}\) приводит к \(\textrm{Right(b'')}\) в тип-сумме \(a + b''\). Аналогично последовательное применение \(g\) и \(g'\) к \(\textrm{Right(b)}\) вначале приводит к \(\textrm{Right(b')}\) в тип-сумме \(a + b'\), затем - к \(\textrm{Right(b'')}\) в тип-сумме \(a + b''\).
Упражнение 4.4.5.
Покажите, что функториальность сохраняет тождественность. Подсказка: используйте \(id_{b}\) и покажите, что она отображается к \(id_{a+b}\).
Если в качестве преобразования взять \(f = id_{a}, g = id_{b}\), то тогда пара стрелок \((Left \circ id_{a}, Right \circ id_{b})\) будет отображать \((a \to a, b \to b)\), т.е. будет определять тождественную стрелку \(id_{a+b}: (a \to a, b \to b)\).
Упражнение 5.1.1.
Покажите, что биекция в доказательстве левой единицы естественна. Подсказка: смените фокус с помощью стрелки \(g : a \to b\).
???
Упражнение 5.1.2.
Постройте стрелку \(h : b + a \times b \to (1 + a) \times b\). Эта стрелка единственная? Подсказка: это отображение-внутрь произведения, поэтому оно задается парой стрелок. Эти стрелки, в свою очередь, отображаютвне сумму, каждая из которых задается, поэтому, парой стрелок. Подсказка: отображение \(b \to 1 + a\) задается как \((Left \circ !)\)
???
Упражнение 5.1.3.
Повторите предыдущее упражнение, рассматривая, на этот раз, h как отображение-вне суммы.
???
Упражнение 5.1.4.
Реализуйте Haskell-функцию maybeAB :: Either b (a, b) -> (Maybe a, b). Является ли эта функция однозначно определенной сигнатурой своего типа или есть некоторая свобода действий?
def maybeAB[A, B](either: Either[B, (A, B)]): (Option[A], B) =
either match
case Left(b) => (None, b)
case Right((a, b)) => (Some(a), b)Да, функция однозначно задается своей сигнатурой.
Упражнение 6.3.1.
Покажите, что: \(2 \times a \cong a + a\), где 2 — логический тип. Сначала проведите доказательство схематически, а затем реализуйте две Haskell-функции, свидетельствующие об изоморфизме.
def toSum[A](product: (Boolean, A)): Either[A, A] =
if product._1 then Left(product._2)
else Right(product._2)
def toProduct[A](either: Either[A, A]): (Boolean, A) =
either match
case Left(a) => (true, a)
case Right(a) => (false, a)Упражнение 7.1.1.
Реализуйте каррированную версию сложения как отображение-вне N в функциональный объект \(N^{N}\) . Подсказка: используйте следующие типы в рекурсоре: init :: Nat -> Nat step :: (Nat -> Nat) -> (Nat -> Nat)
enum Nat:
case Zero
case Succ(n: Nat)
import Nat.*
val one = Succ(Zero)
val two = Succ(one)
val three = Succ(two)
def rec[A](init: A, step: A => A, n: Nat): A =
n match
case Zero => init
case Succ(m) => step(rec(init, step, m))
rec(two, Succ(_), three) // 5
val plusTwo: Nat => Nat = n => rec(two, Succ(_), n)
plusTwo(three) // 5
val curryInit: Nat => Nat = n => n
val curryStep: (Nat => Nat) => (Nat => Nat) = f => k => Succ(f(k))
val curry: Nat => Nat => Nat = n => rec[Nat => Nat](curryInit, curryStep, n)
curry(Zero)(two) // 2
curry(three)(two) // 5Упражнение 7.2.1.
Подумайте, что произойдет, если заменить a в определении списка терминальным объектом. Подсказка: что такое кодирование натуральных чисел по основанию один?
???
Упражнение 7.2.2.
Сколько существует отображений \(h : L_{a} → 1 + a\)? Можно ли получить их все, используя рекурсор списка? Что можно сказать насчет Haskell-функций сигнатуры: \(h :: [a] -> Maybe a\)
???
Упражнение 7.2.3.
Реализуйте функцию, извлекающую третий элемент из списка, если список достаточно длинный. Подсказка: используйте Maybe a для типа результата.
def get[A](list: List[A], n: Int): Option[A] =
list match
case Nil => None
case head :: next =>
if n == 0 then Some(head)
else get(next, n - 1)
get(List(1, 2, 3, 4, 5), 2)
// Some(3)Упражнение 8.2.1.
Опишите функтор, источником которого является категория «шагающая стрелка». Это категория фигурок с двумя объектами и одной стрелкой между ними (плюс обязательные тождественные стрелки).
???
Упражнение 8.2.2.
Категория «ходячий изо» аналогична категории «шагающая стрелка», плюс еще одна стрелка, идущая обратно от b к а. Покажите, что функтор из этой категории всегда выбирает изоморфизм в целевой категории.
???
Упражнение 8.3.1.
Покажите, что WithInt является функтором data WithInt a = WithInt a Int
???
Упражнение 8.3.2.
Покажите, что Id есть Functor. Подсказка: реализуйте для него экземпляр Functor.
trait Functor[F[_]]:
extension [A](fa: F[A])
def map[B](f: A => B): F[B]
case class Id[A](value: A)
given idFunctor: Functor[Id] with
extension [A](as: Id[A])
override def map[B](f: A => B): Id[B] = Id(f(as.value))Упражнение 8.3.3.
Покажите, что (Const c) есть Functor. Подсказка: Конструктор типа принимает два аргумента, но здесь он частично применяется к первому аргументу. Он функториален по второму аргументу.
trait Functor[F[_]]:
extension [A](fa: F[A]) def map[B](f: A => B): F[B]
case class Const[C, A](c: C)
given constFunctor[C]: Functor[[X] =>> Const[C, X]] with
extension [A](as: Const[C, A])
override def map[B](f: A => B): Const[C, B] = Const[C, B](as.c)Упражнение 8.3.4.
Покажите, что MoreThanA является бифунктором. data MoreThanA a b = More a (Maybe b)
???
Упражнение 8.5.1.
Определите композицию «Functor после Contravariant» Подсказка: вы можете повторно использовать Compose, но указав объявление другого экземпляра.
???
Упражнение 9.3.1.
Докажите условие естественности композиции естественных преобразований: \(\gamma_{y} \circ \mathit{Ff} = \mathit{Hf} \circ \gamma_{x}\) Подсказка: используйте определение \(\gamma\) и условия естественности для \(\alpha\) и \(\beta\).
???
Упражнение 9.3.2.
Реализуйте две версии горизонтальной композиции safeHead после reverse. Сравните их результаты, действующие на различные аргументы.
???
Упражнение 9.3.3.
Сделайте то же самое с горизонтальной композицией reverse после safeHead.
???
Ссылки:
- The Dao of Functional Programming - Bartosz Milewski: