Кто нибудь может в пяти строчках кода и паре предложений выразить суть и основные бенефиты идеи?

Здравствуйте, dotneter, Вы писали:

D>Кто нибудь может в пяти строчках кода и паре предложений выразить суть и
Суть в том что с типом связываются значения времени исполнения.
Например:

data Vec (A : Set) : Nat -> Set where
  [] : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

В данном случае описывается список тип которого параметризован не только типом элементов содержащихся в списке но и длинной этого списка.
Первый конструктор создает пустой список с типом которого связано значение 0.
Второй конструктор интереснее.
Первый (неявный) аргумент это длинна исходного списка.
Второй элемент.
Третий исходный список с типом которого связанна длинна.
И с результатом связанна длинна исходного списка плюс один.

D>основные бенефиты идеи?
Например мы хотим написать функцию которая принимает два списка одинаковой длинны и возвращает список кортежей.
Сигнатуру функции можно описать так:

zip : {n : Nat} -> {A : Set} -> {B : Set} -> (l1 : Vec A n) -> (l2 : Vec B n) -> Vec (A, B) n

Теперь если компилятор не будет уверен что в эту функцию передают списки одинаковой длинны то программа не скомпилируется.
Если программа скомпилируется то Компилятор также будет в курсе что тот список что вернула данная функция равен по длине двум исходным.

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

Здравствуйте, WolfHound, Вы писали:

WH>Теперь если компилятор не будет уверен что в эту функцию передают списки одинаковой длинны то программа не скомпилируется.

... и процесс написания программы выглядит как сдача экзамена

компилятор: а это вы откуда вывели?
юзер: ну вот, если эпсилон равен гамме, то Юпитер в фазе Венеры..
компилятор: докажи!

Здравствуйте, WolfHound, Вы писали:

Тоесть, можно сказать что это есть контракты на уровне типов? Только как компилятор узнает
>значения времени исполнения
тривиальные случаи еще можно понять, но я так думаю ими дело не обходится?
Значительно ли это выигрывает какой нибудь анализ кода навроде контрактов в net 4.0?

Здравствуйте, BulatZiganshin, Вы писали:

WH>>Теперь если компилятор не будет уверен что в эту функцию передают списки одинаковой длинны то программа не скомпилируется.
BZ>... и процесс написания программы выглядит как сдача экзамена
И хорошо. Пусть у компилятора бошка болит на тему где еще соломку не подстелили.

BZ>компилятор: а это вы откуда вывели?
BZ>юзер: ну вот, если эпсилон равен гамме, то Юпитер в фазе Венеры..
BZ>компилятор: докажи!
И докажу. Особенно если мы говорим о практической реализации идеи, а не очередной исследовательской работе.
А если лень, трудно или невозможно что-то доказать всегда можно попросить компилятор сгенерировать проверку времени исполнения.
Например:

lameZip : {n m : Nat}{A B : Set} -> (v1 : Vec A n) -> (v2 : Vec B m) -> Vec (A, B) n
lameZip = zip v1 (v2 :> Vec B n)

Собственно привидение Vec B m к Vec B n вставляет проверку что n == m, а если нет то вылетает исключение.

Здравствуйте, dotneter, Вы писали:

D>Тоесть, можно сказать что это есть контракты на уровне типов?
Что-то типа того.

D>Только как компилятор узнает
>>значения времени исполнения
А ему не нужно их узнавать

D>тривиальные случаи еще можно понять, но я так думаю ими дело не обходится?
Не обходится.

D>Значительно ли это выигрывает какой нибудь анализ кода навроде контрактов в net 4.0?
Судя по той инфе что я нашол по контрактам в .NET4 думаю значительно.

Можешь начинать читать отсюда: http://wiki.portal.chalmers.se/agda/agda.php
Предупреждаю с непривычки выносит мозг. Но вынос мозга штука полезная...

Здравствуйте, dotneter, Вы писали:

D>Здравствуйте, WolfHound, Вы писали:

D>Тоесть, можно сказать что это есть контракты на уровне типов? Только как компилятор узнает
>>значения времени исполнения
D>тривиальные случаи еще можно понять, но я так думаю ими дело не обходится?

Создание XML, который не может нарушить заданную схему.

Гарантированно правильные интерпретаторы.

Строго типизированная рефлексия.

D>Значительно ли это выигрывает какой нибудь анализ кода навроде контрактов в net 4.0?

Для зависимых типов не нужен запуск программы. Для контрактов нужен.

Здравствуйте, thesz, Вы писали:

T>Для зависимых типов не нужен запуск программы. Для контрактов нужен.
У контрактов проверка может быть не только в рантайме.
Например

def test(x):
    requires(x > 0)

test(-10)

Выдаст предупреждение не запуская программу.
Но на этом строго типизированую рефлексию не построишь. Мне вообще сложно представить как это возможно ведь то что мы рефлексируем может быть чем угодно.

Здравствуйте, WolfHound, Вы писали:

WH>Здравствуйте, dotneter, Вы писали:

WH>

WH>data Vec (A : Set) : Nat -> Set where
WH>  [] : Vec A zero
WH>  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)
WH>

WH>В данном случае описывается список тип которого параметризован не только типом элементов содержащихся в списке но и длинной этого списка.
WH>Первый конструктор создает пустой список с типом которого связано значение 0.
WH>Второй конструктор интереснее.
WH>Первый (неявный) аргумент это длинна исходного списка.
WH>Второй элемент.
WH>Третий исходный список с типом которого связанна длинна.
WH>И с результатом связанна длинна исходного списка плюс один.

Мне кажеться или это чем-то похоже на

template <int v>
struct Int2Type
{
   enum { value = v; }
}

?

Здравствуйте, kmmbvnr, Вы писали:

K>Мне кажеться или это чем-то похоже на

K>?

Кажется.

Здравствуйте, dotneter, Вы писали:

D>Кто нибудь может в пяти строчках кода и паре предложений выразить суть и основные бенефиты идеи?
Вот здесь коннечно не в паре предложений, но суть понятна.
Еще много чего по теме можно найти по ссылкам вот отсюда

Здравствуйте, dotneter, Вы писали:

D>Здравствуйте, thesz, Вы писали:

T>>Для зависимых типов не нужен запуск программы. Для контрактов нужен.
D>У контрактов проверка может быть не только в рантайме.
D>Например
D>

D>def test(x):
D>    requires(x > 0)

D>test(-10)
D>

D>Выдаст предупреждение не запуская программу.

Проверка зависимых типов ведётся на этапе компиляции. Проверка некоторых контрактов ведётся на этапе компиляции.

Поэтому для некоторых контрактов не нужен запуск программы, а в общем случае нужен.

D>Но на этом строго типизированую рефлексию не построишь. Мне вообще сложно представить как это возможно ведь то что мы рефлексируем может быть чем угодно.

Типы имеют определённую структуру. Например, алгебраические типы могут быть представлены, как сумма произведений с оператором фиксированной точки.

На это можно смотреть, это можно преобразовывать.

Здравствуйте, WolfHound, Вы писали:

WH>

WH>zip : {n : Nat} -> {A : Set} -> {B : Set} -> (l1 : Vec A n) -> (l2 : Vec B n) -> Vec (A, B) n
WH>

WH>Как следствие если не лениться писать правильные типы то можно избавиться не только от кучи проверок в функции на тему, а не подсунули ли нам какую гадость и что делать если таки подсунули, но и юнит/интеграционных тестов ибо система типов их перекрывает с большим запасом.

Вопрос только в одном, на сколько это сложнее обычоного подхода. Судя по приведенной кракозябре, намного.

Здравствуйте, VladD2, Вы писали:


VD>Вопрос только в одном, на сколько это сложнее обычоного подхода. Судя по приведенной кракозябре, намного.
А что это за обычный подход который рубит половину багов на этапе компиляции?

Здравствуйте, dotneter, Вы писали:

VD>>Вопрос только в одном, на сколько это сложнее обычоного подхода. Судя по приведенной кракозябре, намного.
D>А что это за обычный подход который рубит половину багов на этапе компиляции?

Статическая верификация кода возможна и так. Вон в 4-ом фрэйворке вроде как будет поддерживаться для реальных систем.

Что до багов, то они никуда не исчезнут. В этом вопросе нет волшебной палочки. Баги сазажают люди. Если алгоритм крив, то никакая верификция или мощная система типов не спасет. Не надо обольщаться.

Основной причиной появления багов является сложность задачи. И если система которая должна уберечь от багов будет увеличивать эту самую сложность, то на практике будет ровно противоположенный ожидаемому результат.

Так что мощная система типов — это конечно хорошо, но только при том условии, что при этом она не усложнит решение задачи.
Ну, а то что мы тут увидели вряд ли можно назвать простым.

В прочем, возможно я "не догоняю".

Здравствуйте, VladD2, Вы писали:

VD>Здравствуйте, WolfHound, Вы писали:

WH>>

WH>>zip : {n : Nat} -> {A : Set} -> {B : Set} -> (l1 : Vec A n) -> (l2 : Vec B n) -> Vec (A, B) n
WH>>

WH>>Как следствие если не лениться писать правильные типы то можно избавиться не только от кучи проверок в функции на тему, а не подсунули ли нам какую гадость и что делать если таки подсунули, но и юнит/интеграционных тестов ибо система типов их перекрывает с большим запасом.

VD>Вопрос только в одном, на сколько это сложнее обычоного подхода. Судя по приведенной кракозябре, намного.

Это если считать обычным подходом код без модульных тестов и без проверок параметров функции. Если первое неплохо автоматизируется с помощью того же PEX (сам пока не пользовался, но допустим), то от второго, вроде как, никуда не денешься. Хотя, на первый взгляд, да, действительно громоздко.

Во всяком случае, без дополнительного изучения, так однозначно отвергать эту штуку не стоит, или за твоими словами кроется некий опыт использования/изучения этого подхода? В таком случае, было бы очень интересно услышать подробности.

Здравствуйте, VladD2, Вы писали:

VD>Статическая верификация кода возможна и так.
Имхо, основной вопрос в том насколько сложно реализовывать верификаторы, и насколько сложные задачи они могут решать.
Конечно если у нас есть мега интеллектуальная система которая выявляет любые ошибки, то нам не только не нужна мощная система типов, нам и сами типы нужны.

VD>Что до багов, то они никуда не исчезнут. В этом вопросе нет волшебной палочки.
Так я написал, что половину.

Здравствуйте, VladD2, Вы писали:

VD>Что до багов, то они никуда не исчезнут. В этом вопросе нет волшебной палочки. Баги сазажают люди. Если алгоритм крив, то никакая верификция или мощная система типов не спасет. Не надо обольщаться.

ты можешь *доказать*, что некая программа не содержит багов?

Здравствуйте, BulatZiganshin, Вы писали:

BZ>Здравствуйте, VladD2, Вы писали:

VD>>Что до багов, то они никуда не исчезнут. В этом вопросе нет волшебной палочки. Баги сазажают люди. Если алгоритм крив, то никакая верификция или мощная система типов не спасет. Не надо обольщаться.

BZ>ты можешь *доказать*, что некая программа не содержит багов?

В общем случае этого никто не может. Кстати, доказательства (особенно достаточно сложные) также могут содержать ошибки, так что даже наличие доказательства безошибочности программы отнюдь не гарантирует отсутсвие ошибок в этой программе.

Кроме того интересует насколько дорого обходится повышение качества программы посредством использования доказательств. Скажем, рассмотрим такой пример (все цифры взяты с потолка). Мы создаём некоторое ПО (не для управления ядерным реактором). Используя привычные средства повышения качества (модульные тесты, ревью кода) имеем 10 ошибок на 1000 строк кода (взято с потолка) и затрачиваем на это X ресурсов. Если мы воспользуемся зависимыми типами докажем, что у нас 0 ошибок на 1000 строк кода, но потратим на это 2X ресурсов, то зачем нам это доказательство?. ИМХО, гораздо интереснее узнать, как именно влияют зависимые типы на качество и стоимость ПО, нежели абстрактная возможность "доказать" отсутвие ошибок для некоторых программ.

Здравствуйте, VladD2, Вы писали:

VD>Вопрос только в одном, на сколько это сложнее обычоного подхода. Судя по приведенной кракозябре, намного.
Эту кракозябру можно написать немного короче:

zip : forall{A B n} -> (l1 : Vec A n) -> (l2 : Vec B n) -> Vec (A, B) n

теперь напишем тело этой кракозябры

zip []    []    = []
zip x::xs y::ys = (x, y) :: zip xs ys

Все. По другому хрен напишешь ибо компилятор надает по рукам.
Также уже доказано что другие варианты обрабатывать не надо. Они просто не пройдут проверку типов.

Теперь как это будет выглядеть на немерле

zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]

Различия только в том что в случае с зависимыми типами указана длинна списков.

{
| ([],    [])    => []
| (x::xs, y::ys) => (x, y) :: zip(xs, ys)
| _              => throw InvalidArgumentException()
}

те в результате мы и написали больше и переложили проверку с компилятора на рантайм.

И после этого ты говоришь что зависимые типы сложнее?