Исправление no-such-file, (текущая версия) :
Я ещё раз повторяю: то что проверено в типах проверять смысла нет
А я ещё раз повторю: когда ты проверяешь логику тестами, ты проверяешь и типы (неявно), поэтому отдельно (явно) проверять типы смысла нет.
Это область компилятора.
И не нужно усложнять компилятор. И синтаксис.
И если более-менее осмысленная программа на хаскеле скомпилировалась, это часто значит что она работает корректно
Нет, это ничего не значит, кроме того, что она синтаксически правильная. В частности это значит, что в нашу функцию c_to_f всегда передаётся вещественное число. Но это не значит, что данное число - то, которое нужно.
тесты могут проверить лишь некоторое ограниченное число тестовых примеров.
А в программе и требуется проверить только ограниченное количество случаев использования в конкретном контексте. Доказывать корректность функции в алгебраическом смысле на практике не требуется. Ну кроме тех случаев, когда программа, как есть, сама является разновидностью алгебраического выражения. Все эти ML-и в таком виде и задумывались, но это отдельная тема.
Исходная версия no-such-file, :
Я ещё раз повторяю: то что проверено в типах проверять смысла нет
А я ещё раз повторю: когда ты проверяешь логику тестами, ты проверяешь и типы (неявно), поэтому отдельно (явно) проверять типы смысла нет.
Это область компилятора.
И не нужно усложнять компилятор. И синтаксис.
И если более-менее осмысленная программа на хаскеле скомпилировалась, это часто значит что она работает корректно
Нет, это ничего не значит, кроме того, что она синтаксически правильная. В частности это значит, что в нашу функцию c_to_f всегда передаётся вещественное число. Но это не значит, что данное число - то, которое нужно.
тесты могут проверить лишь некоторое ограниченное число тестовых примеров.
А в программе и требуется проверить только ограниченное количество случаев использования в конкретном контексте. Доказывать корректность функции в алгебраическом смысле на практике не требуется. Ну кроме тех случаев, когда программа, как есть, сама является разновидностью алгебраического выражения. Все эти ML-и в таком виде и задумывались.