Я закончил с контентом первого курса по гомотопической теории типов для программистов, остаётся теперь его вычитать и задеплоить на мою тайную учебную платформу, доступную только для умненьких.

В этом курсе теория в основном (которую мы моделируем на Python),
и ещё один курс для разбора теории потребуется. А потом буду делать курсы с акцентами на применение HoTT в конкретных тематических областях (от примитивных CRUD-проэктов и игровых движков до верификации и криптографии). Если в этом году получится закрыть теорию и сделать хотя бы парочку таких "прикладных полезненьких", буду жутко доволен 🙏

А на первом курсе в заключение пишем реалтаймовую Змейку полностью в топологический-ориентированном стиле, на нашем HoTT-движке.

Для моделирования топологии игрового поля используем n-мерный тор (n=2 :).
(автоматическое применение правил оборачивания границ, характерных для тора)
Для представления координат и состояний - Product-тип.
Для моделирования направлений и игровых событий - Sum-тип.
Для отслеживания движения и проверки столкновений - гомотопические пути (Path).
Для представления действий, не возвращающих значимых результатов, таких как пауза или сохранение игры - тип Unit.
Для функций обработки ввода/вывода -- Pi-тип
(зависимая типизация, где для каждого значения домена (нажатия клавиши) определяется функция, преобразующая игровое состояние с учетом текущего контекста).

Сама Змейка
- использует Sum для представления направления движения;
- возвращает Path для отслеживания траектории;
- хранит историю движений как последовательность путей;
- методы проверки коллизий возвращают Sum-типы.

В качестве домашнего задания можно будет например применить рекурсор n-тора для реализации специальных игровых механик, связанных с топологией игрового поля ("порталы", соединяющие различные участки поля по свойствам тора), или расширить использование Path для вычисления сложных траекторий движения (определение кратчайшего пути от головы змейки до еды) и т.п.

=

Какие мощные плюсы мы имеем уже даже на таком уровне в сравнении с ООП?

1. Точное моделирование пространственных отношений
(в нашем случае выход объекта за границы игрового поля).

2. Композиция и декомпозиция игрового состояния
(формальный механизм объединения и разделения различных аспектов игрового состояния, без мутабельности)

3. Типобезопасная обработка вариативных событий
(строгая типизация для представления направления движения, результатов столкновений) с гарантией обработки (на уровне системы типов проекта) всех возможных случаев.

4. Формальное представление траекторий и путей
(движения как математические объекты, которые можно комбинировать и анализировать без каких-либо дополнительных абстракций).

5. Строгое отображение между пользовательским вводом и трансформациями игрового состояния
(типы трансформаций могут зависеть от самого ввода с гарантиями типобезопасности, и никакой каши из условных операторов или паттерн-матчинга для связи между вводом и изменением состояния не требуется).

Бонус: AI очень даже хорошо рассуждает на таком уровне, поэтому потенциально вполне можно формализовать в ТОП и TDD, и BDD.