These are chat archives for groupoid/exe

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