λO
А если бы ты не корректно указал ограничение?
Size: a a a
2018 February 26
AK
не понял
λO
ну ошибся в спеке refinement types твоих
Y
Ну если ты вместо юзернейма подал фамилию то это ошибка типизации. Если ты забыл проверить пароль то это логическая ошибка же
А если у нас есть тип "проверенный пароль"?
AP
Некоторые логические ошибки можно забороть достаточно выразительными типами
λO
А если у нас есть тип "проверенный пароль"?
Ну если его надо таскать как пруф с собой, то может конечно :)
λO
Некоторые логические ошибки можно забороть достаточно выразительными типами
многие можно забороть тупо newtype'ом
AP
именно
λO
А так-то и перепутать имя с фамилией не ошибка типизации, обе строки же :)
Они строками будут только когда парсишь
AK
какие логические ошибки *нельзя* забороть бесконечно выразительными типами?
по-моему, тут дихотомия уровня "если разрабу очевидно, что правильное поведение только одно, то допущение другого поведения — это ошибка типов. Если 'правильных' поведений может быть несколько и надо выбирать, а разраб выбрал неправильно, это логическая ошибка"
по-моему, тут дихотомия уровня "если разрабу очевидно, что правильное поведение только одно, то допущение другого поведения — это ошибка типов. Если 'правильных' поведений может быть несколько и надо выбирать, а разраб выбрал неправильно, это логическая ошибка"
λO
Зависит от реализации
ну вот реализовать так, что-бы перепутывание имени с фамилией были ошибками типизации, совсем не сложно
λO
какие логические ошибки *нельзя* забороть бесконечно выразительными типами?
по-моему, тут дихотомия уровня "если разрабу очевидно, что правильное поведение только одно, то допущение другого поведения — это ошибка типов. Если 'правильных' поведений может быть несколько и надо выбирать, а разраб выбрал неправильно, это логическая ошибка"
по-моему, тут дихотомия уровня "если разрабу очевидно, что правильное поведение только одно, то допущение другого поведения — это ошибка типов. Если 'правильных' поведений может быть несколько и надо выбирать, а разраб выбрал неправильно, это логическая ошибка"
А чем забарывать логические ошибки в описании типа?
AP
Тестами для типов :)
AK
объясняю
идеальный тайпчекер читает техзадание и проверяет, что программа ему соответствует
всё, все ошибки стали ошибками типов
(да, такой тайпчекер реализовать невозможно, пофиг)
идеальный тайпчекер читает техзадание и проверяет, что программа ему соответствует
всё, все ошибки стали ошибками типов
(да, такой тайпчекер реализовать невозможно, пофиг)
λO
Тестами для типов :)
зачёт
λO
объясняю
идеальный тайпчекер читает техзадание и проверяет, что программа ему соответствует
всё, все ошибки стали ошибками типов
(да, такой тайпчекер реализовать невозможно, пофиг)
идеальный тайпчекер читает техзадание и проверяет, что программа ему соответствует
всё, все ошибки стали ошибками типов
(да, такой тайпчекер реализовать невозможно, пофиг)
А техзадание надо писать на формальном языке, что-бы тайпчекер понял!