dependent types

[gds]

(как бы разворачивая каменты из предыдущего поста

Comments

[udpn]

1. Dimensional analysis пишется просто как некий тип, параметризованый значением вектора заданной длины (или конечного отображения, или записи, по вкусу). Обычного вектора. Для этого не нужно писать изврат на шаблонах с MPL'ем. Сообщения об ошибках типизации адекватные. Кроме того, небольшие модификации позволяют в одной программе использовать несколько различных систем единиц (СИ, СГС, МКС, МКГСС) и переводить одни в другие без боли в заднице. Полезно не только в математике, но и практически во всех остальных областях знаний. Например, в тервере позволяет не путать ковариацию с коэфф. корреляции. "Какие-то утверждение в compile-time" это "любые утверждения в compile-time без необходимости переписывать весь код заново в синтаксисе другого вычислительного контекста того же языка". Это многого стоит

[gds]

благодарю за подробный ответ

[thedeemon]

Мое дилетантское видение

[nivanych]

Иначе говоря, надо развивать автоматическое доказательство, ну хоть бы и по мелочам.
В агде-2.2.6 оно было малопригодно (а может быть, я недостаточно попарился и не научился готовить).
Агду-2.3 надо смотреть, но я сомневаюсь, что в этом направлении что-то существенно изменилось.
Если пытаться использовать агду, как "обычный" язык с выводом типов, как хацкель, то отличие одно и существенное (и даже вовсе не в классах типов) - совершенно другой подход к работе с выводом типов (неявные параметры), и привыкать к нему непросто. Вроде, в новых агдах понаделали в этом направлении поболее, навроде таки попыток вывода, когда это возможно. Но всё равно, по-другому всё.

[udpn]

Дилетантское видение? Человека, который смог связать что-то сложнее хелловорлда на ATS'е? Ребе, да вам нужно памятник поставить за скромность.

>> которые нам кажутся очевидными
Ага, недавно читал статью о представлении чисел в зависимо типизированном языке. Там говорилось, что через несколько месяцев исследований автор узнал о числах намного больше, чем ожидал :)

[gds]

и чем закончилось "про числа"? или ему поля этого интернета показались слишком малы для дальнейших описаний?

[udpn]

Li Nuo. Representing numbers in Agda, кажется. У меня их тут несколько.

[thedeemon]

Конечно дилетантское. Я ж на Агде, Коке и прочих Идрисах не писал ничего, а в ATS они не совсем полноценные, как говорят.

[udpn]

*памятник*

[nivanych]

Это означает только бОльшую простоту программирования в агде ;-)
Я вот только смотрел исходники, но сам не пытался писать.
Тут же уже есть хоть какой-то опыт с пониманием.
Довольно согласующийся с тем, что я прикидывал.

[gds]

про "дилетантское" уже сказали, да

[thedeemon]

Верно, написание теорем требует времени и сил, много. Зато покрытие дает более полное, чем тесты. Такой вот выбор между уверенностью в корректности и быстротой написания.

Что касается человеческого фактора, то у меня пока такое ощущение сложилось, что он в случае снабжения кода теоремами/утверждениями сильно меньше, т.к. код и утверждения обязяны быть согласованы, чтобы это скомпилировалось, а допустить одну и ту же ошибку, да такую, которая не будет противоречить другим теориям, очень сложно. Если в простом коде или тесте легко написать глупость, то тут компилятор не даст ее так просто даже сформулировать. Конечно, еще остается возможность ошибки высокого уровня: когда предметная область понята неправильно и сформулированы и доказаны не те теоремы, код делает не то, хоть и делает это правильно. Тут да, исправление потребует бОльших усилий.

[nivanych]

> Такой вот выбор между уверенностью в корректности и быстротой написания.

Кроме того, с возможностью баллансировать сколько угодно.
Можно и просто список использовать с целыми числами, можно с типом-параметром, а можно ещё и с длиной, а можно и куда-то передать значение типа доказательств, что длина какая-нибудь (не) такая.

[udpn]

>> придётся и setsockopt() настраивать

[gds]

> Например, если нет куска кода, который устанавливает SO_ACCEPTCONN, сокет нельзя будет слушать.

ну так это можно закодировать и простым соответствием функций и утверждений:

module Sock
:
sig
type socket = Unix.file_descr;
type listening_socket;
value listen : socket -> backlog:int -> listening_socket;
value accept : listening_socket -> (socket * sock_addr);
end;если не вызвали listen -- не на чём будет вызвать accept

[thedeemon]

Насчет примера с сокетом меня в ATS порадовало применение линейных типов для утверждений. Они не только заботятся о том, чтобы не читать из не того сокета, они также не дадут забыть закрыть сокет, например. Открыли сокет/файл/вотева - получили доказательство этого факта, и за счет его линейности мы во-первых не можем его использовать повторно после того, как "потратили" (закрыв файл/сокет), а во-вторых мы обязаны его "потратить", иначе прога не компилируется. Но это вроде не относится напрямую именно к зависимым типам, это несколько другая фича.