Comments 11
Из статьи абсолютно непонятно, что такое «зависимые типы», какие задачи они решают и зачем понадобилось делать целый язык для валидации.
Если я правильно понимаю, зависимый тип — это, например, "
Если я не прав, поправьте пожалуйста.
Если я правильно понимаю, зависимый тип — это, например, "
int в диапазоне от 0 до 10", или «некий объект, обладающий методом DoStuff()». С помощью таких ограничений можно статически анализировать динамически типизируемые языки, как например JS, и обнаруживать ошибки еще на этапе компиляции.Если я не прав, поправьте пожалуйста.
Существует структурная эквивалентность между программами и математическими доказательствами, которая формализуется в виде изоморфизма между типизированным исчислением и логическими системами (изоморфизм Карри-Говарда). Фактически можно построить тип, выражающий сложные математические свойства.
Логика высказываний соответствует простому типизированному лямбда-исчислению, исчисление предикатов — лямбда-исчислению с зависимыми типами и т.п.
Более подробно о теории типов можно почитать в великолепном учебнике «Типы в языках программирования» за авторством Б. Пирса.
Логика высказываний соответствует простому типизированному лямбда-исчислению, исчисление предикатов — лямбда-исчислению с зависимыми типами и т.п.
Более подробно о теории типов можно почитать в великолепном учебнике «Типы в языках программирования» за авторством Б. Пирса.
Ваш первый пример зависимого типа правильный, а второй — нет (второй пример ближе к структурным типам, как, например, интерфейсы в Go).
На самом деле, зависимые типы на самом верхнем уровне достаточно простая концепция. Пусть у вас есть тип
Теперь представьте, что вы параметризуете тип не другим типом, а каким-либо значением — числом 10, строкой
На самом деле, зависимые типы на самом верхнем уровне достаточно простая концепция. Пусть у вас есть тип
List<T>. В таком случае тип List можно рассматривать как функцию над типами (вы даёте List тип, например, String, и получаете обратно тоже тип, List<String>). Это типы, параметризованные типами — система \lambda \omega.Теперь представьте, что вы параметризуете тип не другим типом, а каким-либо значением — числом 10, строкой
"string", каким-нибудь объектом. Например, если Vector<N> обозначает список чего-то длиной N, где N — натуральное число: Vector<10>, то тип Vector является зависимым типом. Система типов для лямбда-исчисления, которая позволяет такое делать, и есть \lambda P.Для справки, третий вариант — значения, зависящие от типов — это просто полиморфизм. Лучше всего это продемонстрировать на языке типа хаскеля. Например, значение (вернее, не значение, а терм)
10 в зависимости от своего типа может быть разным. Например, 10 :: Int даёт целое число 10, 10 :: Double даёт число с плавающей точкой 10.0, 10 :: Complex Double может дать комплексное число 10 + 0i, 10 :: YourType может дать некоторое значение типа YourType, если для этого типа реализован класс типов Num. То есть, в зависимости от того, какой тип мы приписываем литералу (или другому терму, переменной, например), у него будет cвоё значение.
Я не пиарюсь, но вот статья на хабре. Может прояснится.
Честно говоря, вряд ли такие вещи будут использоваться повсеместно в реальных проектах, а тем более в Web.
Но вообще штука очень даже интересная.
Реальное для нее применение — автоматическая проверка доказательств — такое действительно часто встречается.
Честно говоря, вряд ли такие вещи будут использоваться повсеместно в реальных проектах, а тем более в Web.
Но вообще штука очень даже интересная.
Реальное для нее применение — автоматическая проверка доказательств — такое действительно часто встречается.
Видел вашу статью. Некоторое время назад, когда я начинал изучать зависимые типы и теорем-пруверы, выбирал между Agda и Coq. В итоге выбрал второе: есть как минимум два отличных учебника, плюс Coq более популярен, плюс написан на OCaml и умеет экстрактится в него.
Не, ну это холивар :-D
Agda лучше интегрируется с Haskell, чем Coq с OCaml.
Но плюс Coq'а действительно в учебниках и намного большей истории.
А предпочтения все же берут начало не со спора «Agda или Coq», а со спора «Haskell или OCaml», но это уже действительно холивар.
Agda лучше интегрируется с Haskell, чем Coq с OCaml.
Но плюс Coq'а действительно в учебниках и намного большей истории.
А предпочтения все же берут начало не со спора «Agda или Coq», а со спора «Haskell или OCaml», но это уже действительно холивар.
Дружище, а не перечислите ли названия этих учебников по Coq? Я пока что читаю Пирса, но не отказался бы от обзора альтернативных источников.
О, я тоже на этот топик только сейчас наткнулся — искал, что пишут на Хабре про Coq… Так вот, у автора этой записи ymn есть небольшой вводный тьюториал по Coq из нескольких записей. В конце первой есть ссылки на 2 книги: «Software Foundations» и «Certified Programming with Dependent Types» — я думаю, это и есть вышеупомянутые «два отличных учебника».
Sign up to leave a comment.
F* – новый язык с зависимыми типами для .Net