+ GC for HIT project

docs/projects/hitgc.md

@@ -5,3 +5,58 @@ tags:
 ---
 
 # Уборка мусора для высших индуктивных типов
+
+## Описание
+
+[Высшие индуктивные типы](https://ncatlab.org/nlab/show/higher+inductive+type)
+— особые типы данных: во-первых, они, как и другие индуктивные типы
+данных, позволяют задавать особым образом упорядоченные множества (например,
+множество выражений некоторого языка программирования можно представить в виде
+индуктивного типа данных). Во-вторых, они позволяют задавать дополнительные
+"склейки", отождествляющие произвольные элементы построенного множества.
+Ссылка выше содержит немного удалённые от каждодневного программирования
+примеры; более практически полезный тип данных можно найти в
+[стандартной библиотеке Arend](https://github.com/JetBrains/arend-lib/blob/master/src/Algebra/Ring/Poly.ard#L47):
+
+```
+\data Poly (R : AddPointed)
+  | pzero
+  | padd (Poly R) R
+  | peq : padd pzero 0 = pzero
+```
+
+Данный фрагмент кода действительно описывает многочлены. Смотрите: тип `Poly R`
+определён для любого `R`, где есть `0` (это определение типа `AddPointed`,
+который я здесь не привожу). Далее, у `Poly R` есть три конструктора:
+
+* `pzero` — для нулевого многочлена;
+* `padd p c` — для многочлена вида `c + x * p`;
+* `peq`, задающий склейку вида `0 + 0 = 0`.
+
+Без конструктора `peq`, в типе `Poly` содержались бы "лишние" конструкции с
+необрезанными нулями, например `x + 1` можно было бы представить как:
+
+1. `1 + x * (1 + x * 0)`;
+2. `1 + x * (1 + x * (0 + x * 0))`;
+3. `1 + x * (1 + x * (0 + x * (0 + x * 0)))`;
+4. ...
+
+Это хорошо известная проблема "ведущих нулей", от которых эффективные реализации
+многочленов избавляются. В данном случае, мы просто отождествляем их с наиболее
+компактной версией, что приводит к более общей и более простой реализации
+операций над многочленами.
+
+Данный пример хорош ещё и тем, что показывает пространство для оптимизации
+языков с высшими индуктивными типами: на этапе сборки мусора, оптимальный
+рантайм языка может автоматически упрощать многочлены, вырезая лишние
+конструкторы. (Конечно, правильная реализация сможет оптимизировать далеко не
+только многочлены.)
+
+Собственно, задачей в данном проекте является исследование возможностей для
+оптимизации сборки мусора в языках с высшими индуктивными типами данных с
+последующей proof-of-concept реализацией (например, для того же Arend).
+
+## Тестовое задание
+
+Нет такого. Чувствуете в себе амбицию поразбираться в сложной теме —
+приходите на собеседование, обсудим.