- Сейчас кто-то не проверяет boundaries и делитель на значение "нуль", в этом случае такие же кто-то не будут писать этих самых refined types с !=0 и malloc'и с проверкой длины массивов.
- А если скажем библиотечная функция требует в сигнатуре - хочешь не хочешь - а будешь писать.
В новой стандартной библиотеке (Std.Core) к OCaml народ от ненадежных (потому что всем лень проверять - и пишут, а потом на пустой список вылетают исключения) функций List.hd и List.tl взялись отучать очень простым способом - сделали hd
не
'a list -> 'a
а
'a list -> 'a option
(и tl аналогично)
А тут хочешь не хочешь - а проверять придется - либо что список непуст "до", либо что он был не пуст и потому результат Some 'a, а не None - "после"
PS: Boundaries при использовании функции с подобной сигнатурой не проверить просто не удастся - так или иначе но компилятор надо убедить уже во время компиляции что констрейнт соблюдается - иначе просто не откомпилится.
Самый тупой способ - явно проверить перед вызовом - но вообще-то говоря - это совершенно необязательно - в том и один из кайфов этого подхода, что эти свойства можно протаскивать автоматически очень далеко. А проверки вставлять только там где действительно появление свойства неочевидно.
Кстати тоже самое верно и в отношении язычка что по ссылке - там бы изврат с 'a option не нужен - просто в типе будет условие что список не пуст - а уж как именно убеждать в этом компилятор - вариантов весьма много (проверка - один из них)
