Чтобы на этот вопрос ответить, нужно иметь иметь опыт практического использования завтипов. Таких людей в мире примерно 2.7182818 человека, и все заняты созданием языков с завтипами. :)
Пока что у меня ощущение, что они используются там, где нужен не просто код, а код с доказательствами нужных свойств (вроде корректности преобразований компилятора или отсутствия определенных косяков в ядре ОС), либо просто доказательства сами по себе (формализация чистой математики).
ну нет же, по моим данным должно быть по крайней мере 3.1416! :]
Вот, про подобные изобретения (языков с зависимыми типами) тоже думал. И, главное, думал -- "а зачем оно мне?". Я не разбираюсь в буддизме/даосизме, но откуда-то оттуда знаю принцип недеяния, который формулирую для себя через двойное отрицание: "если не можешь не делать -- делай". И вот, как использование готовых реализаций, так и выкатывание какой-то очередной, говённой, новой, -- всё это пока не попадает под "не можешь не делать". Вот я и ищу причины, по которым захотел бы это делать.
А так -- мнение учёл. Доказательства кода -- важны, и даже очень. Но редко. Но, всё же, очень важны. Но это не настолько связано с зависимыми типами -- скорее, там просто "модель" такая, где живут вместе и типы, и значения, и сами зависимые типы там всего лишь частный случай. Ещё бы, когда такие громадины доступны для работы (я про coq/agda) -- можно и зависимые типы оформить, раз плюнуть.
1. Dimensional analysis пишется просто как некий тип, параметризованый значением вектора заданной длины (или конечного отображения, или записи, по вкусу). Обычного вектора. Для этого не нужно писать изврат на шаблонах с MPL'ем. Сообщения об ошибках типизации адекватные. Кроме того, небольшие модификации позволяют в одной программе использовать несколько различных систем единиц (СИ, СГС, МКС, МКГСС) и переводить одни в другие без боли в заднице. Полезно не только в математике, но и практически во всех остальных областях знаний. Например, в тервере позволяет не путать ковариацию с коэфф. корреляции. "Какие-то утверждение в compile-time" это "любые утверждения в compile-time без необходимости переписывать весь код заново в синтаксисе другого вычислительного контекста того же языка". Это многого стоит
( ... )
Иначе говоря, надо развивать автоматическое доказательство, ну хоть бы и по мелочам. В агде-2.2.6 оно было малопригодно (а может быть, я недостаточно попарился и не научился готовить). Агду-2.3 надо смотреть, но я сомневаюсь, что в этом направлении что-то существенно изменилось. Если пытаться использовать агду, как "обычный" язык с выводом типов, как хацкель, то отличие одно и существенное (и даже вовсе не в классах типов) - совершенно другой подход к работе с выводом типов (неявные параметры), и привыкать к нему непросто. Вроде, в новых агдах понаделали в этом направлении поболее, навроде таки попыток вывода, когда это возможно. Но всё равно, по-другому всё.
У Edwin Brady, одного из 2.71828 людей, использующих зависимые типы, на сайте есть несколько расширенных практических примеров, [1], [2] о полезности всей этой затеи.
Пользуясь случаем, задам вопрос не по теме. Overbld сейчас называет себя Ocaml 3.13. Как я понимаю, это пропатченный 3.12.0. А что за патч, в чем отличие?
чуть по-другому: это svn trunk, взятый где-то в июле, что ли, 2011г. То есть, как было в транке, так он себя и называет. Разве что я иногда довожу девелоперские версии до "чистых" версий наподобие "3.11.2" (вроде для оазиса это надо было когда-то
( ... )
Зависимые типы можно использовать не только для доказательств, но и для generic-программирования. Вот тут www.seas.upenn.edu/~sweirich/ssgip/ серия презентаций, где показана Agda, используемая как язык программирования, а не пруф-ассистент ( --type-in-type, --no-termination-check, --no-positivity-check).
Comments 37
Пока что у меня ощущение, что они используются там, где нужен не просто код, а код с доказательствами нужных свойств (вроде корректности преобразований компилятора или отсутствия определенных косяков в ядре ОС), либо просто доказательства сами по себе (формализация чистой математики).
Reply
Вот, про подобные изобретения (языков с зависимыми типами) тоже думал. И, главное, думал -- "а зачем оно мне?". Я не разбираюсь в буддизме/даосизме, но откуда-то оттуда знаю принцип недеяния, который формулирую для себя через двойное отрицание: "если не можешь не делать -- делай". И вот, как использование готовых реализаций, так и выкатывание какой-то очередной, говённой, новой, -- всё это пока не попадает под "не можешь не делать". Вот я и ищу причины, по которым захотел бы это делать.
А так -- мнение учёл. Доказательства кода -- важны, и даже очень. Но редко. Но, всё же, очень важны. Но это не настолько связано с зависимыми типами -- скорее, там просто "модель" такая, где живут вместе и типы, и значения, и сами зависимые типы там всего лишь частный случай. Ещё бы, когда такие громадины доступны для работы (я про coq/agda) -- можно и зависимые типы оформить, раз плюнуть.
Reply
Reply
Reply
Reply
В агде-2.2.6 оно было малопригодно (а может быть, я недостаточно попарился и не научился готовить).
Агду-2.3 надо смотреть, но я сомневаюсь, что в этом направлении что-то существенно изменилось.
Если пытаться использовать агду, как "обычный" язык с выводом типов, как хацкель, то отличие одно и существенное (и даже вовсе не в классах типов) - совершенно другой подход к работе с выводом типов (неявные параметры), и привыкать к нему непросто. Вроде, в новых агдах понаделали в этом направлении поболее, навроде таки попыток вывода, когда это возможно. Но всё равно, по-другому всё.
Reply
Reply
Буду читать по ссылкам.
Reply
Overbld сейчас называет себя Ocaml 3.13. Как я понимаю, это пропатченный 3.12.0. А что за патч, в чем отличие?
Reply
Reply
Reply
Reply
Leave a comment