А, об этом я тоже думал
Для проверки функции мы можем породить фейковый «тип», для которого заданные функции возвращают заданные значения.

Для этого придумали долговые расписки

Угу, только завтипы — это много головоломной теории, и потом часы обсуждений в чатиках «как доказать поворот матрицы». Я тупой. Я не хочу ничего доказывать.

Доказывают в чатиках лишь по той причине, что там хотят в типах энкодить утверждения о коде и их прувать.

Если это не нужно, то особых проблем с зав типами нет

Доказывают в чатиках лишь по той причине, что там хотят в типах энкодить утверждения о коде и их прувать.

Если это не нужно, то особых проблем с зав типами нет

И это ломает многие конструкции вроде ифа как специализации.

s/особых проблем с завтипами нет/завтипы не нужны/

Академия не просто так это изучает и она не просто так есть. Игнорировать её наработки - это дико тупо.

Я продолжаю размышлять над своей идеей про систему типов, которая на самом деле просто пачка const fn
Кажется, это позволяет реализовывать достаточно сложные фичи почти бесплатно
Она не даёт бесплатно зависимые типы и линейные/афинные/релевантные типы, но HKT, GAT, специализация идут бесплатно
Трейт — это просто функция

my_trait :: (Type, ...) -> Maybe (Type, ...)

(где (Type, ...) это «tuple из некоего количества элементов типа Type»)
Если трейт возвращает Just ..., то он реализован и внутренности Just — ассоциированные типы
Если Nothing, то трейт не реализован
При компиляции вместо сложной магии настоящих тайпчекеров, мы просто вызываем функцию и смотрим, что она вернёт
Специализация — это просто if внутри функции
Дженерик-типы — это функция, которая принимает тип и возвращает тип
HKT — это просто частично применённый дженерик-тип (и мы даже можем делать разные лейауты для разных аргументов дженерика, простым ифом)

У меня, правда, ощущение, что вывод типов это ломает напрочь, кроме самых тривиальных случаев. Фиг бы с тем, что тут очевидно получается Тьюринг-полный тайпчекинг, но для рабочего вывода типов тут потребуется реверсивно исполнять Тьюринг-полную программу что эээ немного невозможно. Вывод возвращаемого типа функции будет работать нормально, но вывод типов аргументов будет сломан на уровне «проще вообще его не делать». Возможно, конечно, эту боль можно как-то уменьшить с помощью простого синтаксиса для type ascription, но всё равно неприятно.

Ну, да, можно построить красивую систему типов на основе красивой математики. А можно использовать кривой, не идеальный костыль, который можно будет понять без красивой математики.

Было бы что особо понимать в зав типах. Там нет прям какой-то дикого мозголобия или особой математики