These are chat archives for groupoid/exe

6th
Apr 2016
Zeit Raffer
@zraffer
Apr 06 2016 09:40 UTC
Официально заявляю, что от Леан трудно добиться взаимности! Вчера весь день оно мне писало, что зацикливается из-за своего продвинутого алгоритма higher order unification. Т.е. тайпчекнуть не может, ни да, ни нет. Сегодня перепишу проблемную функцию, порезав ее на части.
Индуцируй с нами, индуцируй как мы, индуцируй лучше нас!
nponeccop
@nponeccop
Apr 06 2016 13:39 UTC
Беги повесил им?
Zeit Raffer
@zraffer
Apr 06 2016 14:16 UTC
Это фича в данном случае. Леан умеет быстро выводить типы и имплицитные параметры (по сравнению со всякой Агдой), но не всегда оно работает. Проблема в алгоритме. В таких случаях надо писать имплицитные параметры вручную, надо только понять какие.
nponeccop
@nponeccop
Apr 06 2016 14:36 UTC
а, то есть это эвристика эврицировала-эврицировала, да не выэврицировала? алгоритма ж не существует полного.. оно не циклится ж, а пишет ошибку?
Zeit Raffer
@zraffer
Apr 06 2016 15:11 UTC
да, оно пишет ошибку про ограничение алгоритма
nponeccop
@nponeccop
Apr 06 2016 15:27 UTC
Ну, если занудствовать - то это ограничение не алгоритма, а исходной задачи, которая semidecidable.
nponeccop
@nponeccop
Apr 06 2016 15:36 UTC
Я бы вообще не употреблял слово "проблема " в этом контексте. Это всё равно что компилятор С++ писал бы "извините, у нас тут проблема в компиляторе - мы не можем доказать, что сгенерированный код самый быстрый из возможных"
Zeit Raffer
@zraffer
Apr 06 2016 15:44 UTC
проблема в том, что он не может проверить типы ) но я уже переписал ему более понятно, прокатило.