VS
Я так понимаю, он руки отрезает значительно жёстче, чем f#
Size: a a a
2018 June 13
AH
Намертво, не пришить.
AH
Но в нём конечно тайп инфиренс ядерный
из этого кода
let rec factorial n =
if n = 0 then 1 else n * (factorial (n - 1))
оно выводит такой тип:
val factorial: x:int{x>=0} -> Tot int
т.е. поняло что >=0 и что на выходе Tot int, тотальная функция
из этого кода
let rec factorial n =
if n = 0 then 1 else n * (factorial (n - 1))
оно выводит такой тип:
val factorial: x:int{x>=0} -> Tot int
т.е. поняло что >=0 и что на выходе Tot int, тотальная функция
VS
Кстати, неясно,как вывели
АУ
Можно экстрактить код в OCaml или C.
То есть ты на F* верифицируешь, а потом генеришь соответствующий код, который потом работает?
VS
Что >=0
RM
Что >=0
ну по коду ясно же
VS
Неясно
АУ
ну по коду ясно же
вроде же можно отрицательный x передать, ичо
VS
вроде же можно отрицательный x передать, ичо
Вот и я о том
RM
при нуле - ноль, меньше нуля - уход в бесконеность - больше все сходится к инту
AH
стоп, я прогнал
RM
при нуле - ноль, меньше нуля - уход в бесконеность - больше все сходится к инту
а бесконечность приведет к стековерфлоу
AH
VS
Ну дык -2 можно подсунуть
VS
Там ещё is_positive
VS
В теории 😉
AH
оно не так работает
For a recursive function, without further annotation, F* attempts to automatically prove that the recursion always terminates. In the case of factorial above, F* attempts to prove that it has type int -> Tot int, and fails to do so because, factorial is actually not a total function on arbitrary integers! Think about factorial -1.
For a recursive function, without further annotation, F* attempts to automatically prove that the recursion always terminates. In the case of factorial above, F* attempts to prove that it has type int -> Tot int, and fails to do so because, factorial is actually not a total function on arbitrary integers! Think about factorial -1.
АУ
x>=0 это может оно и есть? Условия, при которых работает и тотальное?
AH
The factorial function is, however, a total function on non-negative integers. We can ask F* to check that this is indeed the case by writing:
val factorial: x:int{x>=0} -> Tot int
val factorial: x:int{x>=0} -> Tot int