<aside> 💡 Алгебраические типы данных – это скрещивание enum’ов и структур из Си. (Из презы)

</aside>

<aside> 💡 Алгебраический тип данных — в информатике наиболее общий составной тип, представляющий собой тип-сумму из типов-произведений. Алгебраический тип имеет набор конструкторов, каждый из которых принимает на вход значения определённых типов и возвращает значение конструируемого типа. Конструктор представляет собой функцию, которая строит значение своего типа на основе входных значений. Для последующего извлечения этих значений из алгебраического типа используется сопоставление с образцом. (Из википедии)

</aside>

Пример:

Связный список — структура данных, представляет:

• ИЛИ ничего(NIL)
• ИЛИ элемент списка, который состоит из данных типа 'a И еще одного списка.

type 'a list = 
| Nil
| Cons of 'a * 'a list

Nil и Cons — конструкторы типа ‘a list.

• В чём их алгебраичность?

Аксиомы алгебраических типов:

• Доступ к аргументам (selection): существуют такие $s_i ^k$ , что $s^k_i (C_k (x_{k_1} , ..., x_{k_n} )) = x_{k_i}$

  • Pattern-matching

  let rec somefunc xs =
  	match xs with
  	| [] −>
  		(∗ no argument ∗)
  		...
  	| h :: tl −>
  		... h ... tl ... h ...
  

• Дизъюнктность (distinctness): если $j ≠ i$, то $C_j (x) \neq C_i (y)$

  • если значения начинаются с разных конструкторов, то они не равны

  let rec neq_lists xs ys =
  	match (xs, ys) with
  	| [], _::_ −> true
  	| _::_, [] −> true
  	| x::tl1, y::tl2 −> (x <> y) || neq_lists tl1 tl2
  	| [],[] −> false
  

• Инъективность (injectivity): если $C_{i} (x_1 , ..., x_{n} ) = C_{i} (y_1 , ..., y_{n} )$, то $x_k = y_k$

  • если значения равны, то начинаются с одного и того же конструктора, и аргументы равны попарно.

  let rec eq_lists xs ys =
  	match (xs,ys) with
  	| [],[] −> true
  	| [], _ :: _ −> false
  	| _ :: _, [] −> false
  	| x::tl1, y :: tl2 −> (x = y) && eq_lists tl1 tl2
  

• Полнота (exhaustiveness): если $\mathbb{X}$ представитель алгебраического типа, то $\exist i, n: \mathbb{X} = C_i (y_1 , ..., y_n )$

  • значения алгебраического типа всегда начинаются только с тех конструкторов, которые перечислены в типе

  let rec even_length xs =
  	match xs with
  	| [] -> true
  	| _ :: _ :: tl -> even_length tl
  (* Warning 8: this pattern-matching is not exhaustive.
  Here is an example of a case that is not matched: _::[] *)
  

  Boolean blindness

  Boolean blindness — по сути отсутствие конкретной семантики у Boolean типа. В ФП принято максимально передавать смысл/семантику программы через типы. Стоит отметить, что этот подход стоит по возможности соблюдать и в других языках. Для лучшей передачи смысла “флага”, “метки” и других полей выразимых как Boolean используем отдельный тип данных.

  Пример:

  Использовать вместо bool, такое:

  type color = Red | Black
  type filter = Keep | Remove
  

  Вывод zipper-ов для списков и деревьев.

  ---

  by Dabzelos

  Какаду в лекции говорит что зипер это по факту дифференциал от мощности типа. Это не доказанное (как я понял) свойство которое было получено просто наблюдением.

  Фактически вы берете мощность листа а это $1(Nil) + a` list$ и диффенциируете это, здесь а это мощность типа а, ну и снова лист. Дальше сами справитесь

  by Deepseek

  type 'a list =
    | Nil
    | Cons of 'a * 'a list
  

  Что такое α в уравнении L = 1 + α * L?

  α — это тип элемента списка. В контексте алгебраических типов данных (как в OCaml) α представляет собой "мощность" (количество возможных значений) типа элемента списка. Например:

  • Если α — это int, то мощность α равна количеству возможных целых чисел (например, 2³² для 32-битных целых).
  • Если α — это bool, то мощность α равна 2 (true и false).

  ---

  Уравнение списка

  Уравнение L = 1 + α * L описывает рекурсивную структуру списка. $L = 1 + \alpha L$ $L \cdot (1 - \alpha) = 1$ $L = \frac{1}{1 - \alpha}$

  ---

  В чём прикол взятия дифференциала по alpha?

  Мы “уничтожаем” какую-то единственную alpha. Пуф, её не существуют. Дырка. One-hole, payload - ключевые слова для поиска этой проблемы. Каков контекст того, что осталось, как собрать обратно, смотря с перспективы “уничтоженной” alpha?

  Дифференцирование уравнения

  Если взять производную обеих частей уравнения по $\alpha$, $L = 1 + \alpha \cdot L$, то получим: $\frac{dL}{d\alpha} = 0 + L + \alpha \cdot \frac{dL}{d\alpha} \quad$

  Переносим $\alpha \cdot \frac{dL}{d\alpha}$ в левую часть: $\frac{dL}{d\alpha} - \alpha \cdot \frac{dL}{d\alpha} = L$

  Выносим $\frac{dL}{d\alpha}$ за скобку: $\frac{dL}{d\alpha} \cdot (1 - \alpha) = L$

  Отсюда: $\frac{dL}{d\alpha} = \frac{L}{1 - \alpha}$

  Подставляем $L = \frac{1}{1 - \alpha}$ : $\frac{dL}{d\alpha} = \frac{\frac{1}{1 - \alpha}}{1 - \alpha} = \frac{1}{(1 - \alpha)^2} = L^2$

  ---

  Итог

  Производная $\frac{dL}{d\alpha} = L^2$ показывает, что зиппер для списка хранит один тип из двух списков: элементы до текущей позиции и элементы после. Держим в голове, что это типа если бы мы уничтожили один элемент alpha (например [1,2] [4,5])) , но ЭТО нам поможет РАЗГРАНИЧИТЬ наш тип данных, даже если бы мы его не уничтожали. Просто нам важен контекст того, как мы можем хранить всё, если мы находимся на одной из “уничтоженных” позиций. Это и есть ВЫВОД. Отсюда прямо идёт определение zipper’а:

  type 'a zipper = 'a list * 'a list
  

  ---

  Информация по zipper-ам из презы:

  

  

  

  List zipper: https://gist.github.com/NicolasT/1286763

  Tree zipper: TODO

  Какаду в презе давал ссылку на какого-то Хуета, который вот здесь написал про зиппер для деревьев https://www.st.cs.uni-saarland.de/edu/seminare/2005/advanced-fp/docs/huet-zipper.pdf

  https://speakerdeck.com/paperswelove/erik-hinton-on-the-derivative-of-a-regular-type-is-its-type-of-one-hole-contexts-by-conor-mcbride?slide=36

  ---

Tree zippersss @darknesssupremacy [WIP]

type 'a tree =
  | Leaf
  | Node of 'a tree * 'a * 'a tree

Производная типа для бинарного дерева вычисляется следующим образом:

Исходное уравнение типа: $T = 1 + \alpha \cdot T^2$

1 - это Leaf

a * T^2 - это ‘a * ‘a tree * ‘a tree