История изменений
Исправление AndreyKl, (текущая версия) :
да сможет... как минимум можно завернуть в монады и передать в ран число заведомо большее чем нужно для завершения ф-ции, но это немножко чит.
Что до других способов, то их есть. Но это уже разбираться надо. Да и вопрос целесообразности.. вам зачем? доказать что завершается или написать исполняемый код который будет надёжным?
Если исполняемый, то есть смысл заморочиться с другими подходами, т.к. монады при экспорте кода в окамль (чтоб быстро работало в итоге) скорее всего дадут оверхед.
А если доказывать что то , то в монады завернуть да и дальше жить, всё типизируется, никуда не денется.
Исправление AndreyKl, :
да сможет... как минимум можно завернуть в монады и передать в ран число заведомо большее чем нужно для завершения ф-ции, но это немножко чит.
Что до других способов, то их есть. Но это уже разбираться надо. Да и вопрос целесообразности.. вам зачем? доказать что завершается или реально исполняемый код сделать надёжным?
Если исполняемый, то есть смысл заморочиться с другими подходами, т.к. монады при экспорте кода в окамль (чтоб быстро работало в итоге) скорее всего дадут оверхед.
А если доказывать что то , то в монады завернуть да и дальше жить, всё типизируется, никуда не денется.
Исходная версия AndreyKl, :
да сможет... как минимум можно завернуть в монады и передать в ран число заведомо большее чем нужно для завершения ф-ции, но это немножко чит.
Что до других способов, то их есть. Но это уже разбираться надо. Да и вопрос целесообразности.. вам зачем? доказать что завершается или реально исполняемый код?
Если исполняемый, то есть смысл заморочиться с другими подходами, т.к. монады при экспорте кода в окамль (чтоб быстро работало в итоге) скорее всего дадут оверхед.
А если доказывать что то , то в монады завернуть да и дальше жить, всё типизируется, никуда не денется.