HM.txt

Алгоритм устроен так, что место ошибки определить невозможно

хм строит систему из пицотыщ уравнений и потом начинает ее решать унификацией

то есть он берет какоето уравнение, подставляет туда абстрактный аргумент, 
по нему подставляет в другое у-е и т.д. - в каком-то у-е на аругмент накладывается ограничение, аргумент становится более конкретным
если где-то ошибка - то В НЕКОТОРОМ месте в графе возникнет противоречие - будет наложено ограничение, которому аргумент уже не может
удовлетворить (из-за другого ограничения, которое было наложено раньше, например сперва сказали, что должна быть строка, а потом - что
число, при этом неизвестно где именно ошибка - там где фиксирована строка, или там где фиксировано число, и в зависимости от хода 
реализации алгоритма он выведет ошибку или в том месте или в другом)

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

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

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

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

анальная акробатика на типах должна быть СЛОЖНОЙ И НЕУДОБНОЙ в реализации, для девелопера, но ПРОСТОЙ И УДОБНОЙ для пользователя

----------

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