Перейти к содержанию

Уборка мусора для высших индуктивных типов

Описание

Высшие индуктивные типы — особые типы данных: во-первых, они, как и другие индуктивные типы данных, позволяют задавать особым образом упорядоченные множества (например, множество выражений некоторого языка программирования можно представить в виде индуктивного типа данных). Во-вторых, они позволяют задавать дополнительные "склейки", отождествляющие произвольные элементы построенного множества. Ссылка выше содержит немного удалённые от каждодневного программирования примеры; более практически полезный тип данных можно найти в стандартной библиотеке Arend:

Text Only
\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).

Тестовое задание

Нет такого. Чувствуете в себе амбицию поразбираться в сложной теме — приходите на собеседование, обсудим.