AZ
Для функции min например можно написать доказательство
Size: a a a
2020 January 19
A
Короче в общем случае статическая типизация все ошибки логики не ловит.
AZ
Короче в общем случае статическая типизация все ошибки логики не ловит.
ловит, вопрос в том, насколько сложные типы тебе описывать придется
AZ
скорее "есть некоторый логичный предел за которым типы становятся настолько сложными что их использования не оправдано"
AZ
но это разные вещи
DS
Короче в общем случае статическая типизация все ошибки логики не ловит.
Ловит, если это язык с зависимыми типами и ты сформулировал утверждение о корректности программы на уровне типов.
A
Ловит, если это язык с зависимыми типами и ты сформулировал утверждение о корректности программы на уровне типов.
много таких в проде сейчас?
А⚙
Какая?
Ну блин.
"Programming defeatism: no technique will eliminate all bugs, so let's go with what worked in 70s"
"Programming defeatism: no technique will eliminate all bugs, so let's go with what worked in 70s"
А⚙
Ну блин.
"Programming defeatism: no technique will eliminate all bugs, so let's go with what worked in 70s"
"Programming defeatism: no technique will eliminate all bugs, so let's go with what worked in 70s"
Немного переврал, но суть именно такая
А⚙
много таких в проде сейчас?
С натяжкой - Haskell. И не потому, что он в проде не используется, а потому, что завтипизированный язык из Haskell не очень
А⚙
Щас Доге будет за скалку топить
AZ
Ну блин.
"Programming defeatism: no technique will eliminate all bugs, so let's go with what worked in 70s"
"Programming defeatism: no technique will eliminate all bugs, so let's go with what worked in 70s"
а, точно
DS
много таких в проде сейчас?
Смотря что считать продом для этих языков.
Из мейнстрима зависимые типы хотя бы в теоретическом виде есть в скале.
Вне мейнстрима: coq (прувер, он реально используется для доказательств много где), агда (экспериментальный язык-прувер, но сообщество активное), идрис (скорее язык общего назначения, а не прувер, но зав типы там из коробки)
Из мейнстрима зависимые типы хотя бы в теоретическом виде есть в скале.
Вне мейнстрима: coq (прувер, он реально используется для доказательств много где), агда (экспериментальный язык-прувер, но сообщество активное), идрис (скорее язык общего назначения, а не прувер, но зав типы там из коробки)
G
Щас Доге будет за скалку топить
В dotty разве зав. типы полноценные есть?
DS
В dotty разве зав. типы полноценные есть?
Они и в скале есть, просто работать с ними не удобно.
А так, зависимую пару и зависимую функцию ты сможешь выразить, так что зав типы есть
А так, зависимую пару и зависимую функцию ты сможешь выразить, так что зав типы есть
G
Они и в скале есть, просто работать с ними не удобно.
А так, зависимую пару и зависимую функцию ты сможешь выразить, так что зав типы есть
А так, зависимую пару и зависимую функцию ты сможешь выразить, так что зав типы есть
Очень интересно
G
То есть как в Idris, только работать менее удобно с ними?
DS
Очень интересно
https://stackoverflow.com/questions/12935731/any-reason-why-scala-does-not-explicitly-support-dependent-types/12937819
Вот тут в ответе можешь посмотреть подробности об их энкодинге в скале
Вот тут в ответе можешь посмотреть подробности об их энкодинге в скале
DS
То есть как в Idris, только работать менее удобно с ними?
Нет, не как в идрисе или агде, т.к. просто поднять любую функцию на уровень типов не выйдет.
DS
Но основные конструкции зав типов выразить можно