VG
в F* можно чтобы у функции Bool -> Int -> String -> ? тип ? был или Int или String в зависимости от значения Bool?
Size: a a a
2020 May 03
G
в F* можно чтобы у функции Bool -> Int -> String -> ? тип ? был или Int или String в зависимости от значения Bool?
зависимый патмат
G
хз
G
в идрисе можно 100
VG
как я понял refinement types так не может
VG
зависимые типы могут
VG
F* also has dependent types ну значит должен смочь и на нем не провести сравнение
G
интересно зависимые пары там есть
VG
x:t[{phi}] * t это?
G
походу да
VG
https://rise4fun.com/fstar/tutorial отсюда если что
G
в идрисе
(t1 ** t2)G
где тип
t2 зависит от t1/¯
Короче я против выглядит сомнительно
Контракты и тесты тоже выглядят сомнительно, да?
/¯
Бизнес логику надо в прод хуячить и undefined is not a function в базу юзеру класть?
/¯
Оно хорошо хуячить на стадии PoC, не более
/¯
Или вот, tcl — никаких типов, только строки и блобы
/¯
Хорошо хуячить!
M
Контракты и тесты тоже выглядят сомнительно, да?
В с++ да
M
Хотя не странно а тупо криво