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

Вдогонку.

То, что делает здоровенный код на Си, легко и кратко выражается спецификацией на языке Хаскель. Из которого код на Си и создаётся.

Не надо сбрасывать со счётов уровень языка.

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

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

D>>Мечта — это чтобы программы сами писались?
D>>Зависимые типы позволяют довольно удобно записывать широкий класс спецификаций. Например, отсортированный список на Агде можно описать так:
D>>

D>>data OList : Nat -> Set where 
D>>  Nil  : {b : Nat} -> OList b 
D>>  Cons : {b : Nat} -> (x : Nat) -> (b ≤ x) -> OList x -> OList b
D>>

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

Set, грубо говоря, тип всех типов. Если мы хотим сказать, что идентификатор A — это тип, мы пишем A : Set. Nat — это натуральные числа, определенные в стандартной библиотеке так

data Nat : Set where
 zero : Nat
 suc  : Nat -> Nat

Дальше над ними определяется сложение (подчеркивания — плэйсхолдеры для аргументов оператора)

_+_ : Nat -> Nat -> Nat
 zero  + m = m
 suc n + m = suc (n + m)

умножение и т.д. Определения строятся на паттерн матчинге.

Тип натуральных чисел идеален для индексирований, в том числе и на уровне типов. Например, обычный список мы бы определили в Агде так

data List (a : Set) : Set where
 []   : List a 
 _::_ : a -> List a -> List a

А список, индексированный длиной, можно определить так

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

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

VD>Проблема в том, что описание получилось в несколько раз сложнее самой функции.
Чё там сложное? Там все максимально просто и полностью декларативно.

VD>ОК. А что мы контролировали? И нельзя ли выразить это более просто?
Что длины входищих и исходящего списков идентичны.

VD>Я бы так не сказал. В немероловм варианте есть простор для фантазии
Ага. Для багов.

VD>(так как реализация не приведена).
А строчкой ниже что?

VD>Списки могут различаться по длине и при этом реализация может реагировать по разному:
VD>1. Выдать исключение.
VD>2. Отбросить "лишние" элементы из более длинного списка.
VD>По жизни второй вариант будет более востребован, хотя потребоваться могут оба.
Нахрена?
ИМХО единственный разумный вариант в случае списков разной длинны это ошибка времени компиляции.

VD>Код который нужно добавить, чтобы получить п. 1. не сложен:
VD>

VD>zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
VD>  requires l1.Lenght == l2.Lenght
VD>  ensures  value.Lenght == l1.Lenght
VD>

Это блин называется не сложный... ты на оригинал еще раз посмотри да.
Там все полностью декларативно.

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

VD>Как эти проблемы решаются в Агде?
Какие проблемы?

VD>Я повторюсь, но мне не понятно, как компилятор сможет проверить работу со списками большая часть которых получается динамически?
VD>Или мы будем работать отдельно с динамическими списками (и при этом все проверки пойдут на смарку), и отдельно со статическими?
Ты точно не понял что к чему.

VD>Я пока ничего не говорю. Я просто констатирую факт, что то что ты привел — это весьма туманно, сложно и при этом не понятно решает ли исходные задачи.
Непривычно? Да.
Сложно? Нет.
Решает.

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

VD>Многословность != непонятность. Сравним два варианта:
VD>

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

VD>и
VD>

VD>zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
VD>  requires l1.Lenght == l2.Lenght
VD>  ensures  value.Lenght == l1.Lenght
VD>

Сравнил. Мне первый понятнее.
Более того он формален в доску чего не скажешь о костылях во втором случае.

VD>Приведенный тобой пример описания типа функции в двое длиннее тела функции и в 10 раз не понятнее (на мой взгляд).
Ну давай запишем это в более привычном тебе виде:

zip{A, B, n}(l1 : Vec A n, l2 : Vec B n) : Vec (A * B) n

С синтаксисом можно обходится весьма вольно.

VD>Кучу ли?
Ага.

VD>Что у нас с динамическими списками? Что у нас с вводом / выводом?
А что с ними?

VD>Что, наконец с логикой? Как в систему типов загнать информацию о поведении не тривиального кода?
Берешь и загоняешь. Декомпозицию никто не отменял.

VD>Я не заметил чего-то выносящего мозг. Видимо по второму разу данная трава уже не так выносит .
VD>Я заметил "много букв" при не вполне понятном результате.
Много букв это у тебя. И результат не понятен опять таки тебе.

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

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

VD>>Как эти проблемы решаются в Агде?
WH>Какие проблемы?

Наверное имелось в виду

listA = getListA (void -> Vec A n)
listB = getListB (void -> Vec B n)

zip listA listB // как тут компилятор понимает какой длинны listA и listB

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

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

VD>>>Как эти проблемы решаются в Агде?
WH>>Какие проблемы?

D>Наверное имелось в виду
D>

D>listA = getListA (void -> Vec A n)
D>listB = getListB (void -> Vec B n)

D>zip listA listB // как тут компилятор понимает какой длинны listA и listB
D>

Делаем проверку на равенство. Если равны, то можно zip. Не равны, отрежем кого. Или приклеим кому.

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

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

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

G>>>Ты видимо не понял. Если можно написать спецификацию поведения некоторого объекта, то эта спецификация будет не проще самого кода объекта, вероятнее всего гораздо сложнее. Как потом доказать что спецификация написана без ошибок?
VE>>Это чисто интуитивная мысль, или есть какие-то подтверждения?
G>Интуитивная.

А желательно бы иметь опыт. Тем более, что в этом нет ничего сложного.

VE>>Спецификация отсортированного списка, как было видно на примере, на порядки проще сортировки. Так что "вероятнее всего" стоит здесь вероятнее всего не к месту.
G>Спецификация списка != спецификация алгоритма сортировки.
G>В любом случае полная (а иначе она нам не поможет) спецификация поведения кода будет не меньше (и не проще) самого кода.

Во-первых, можно приближаться к полной спецификации сколь угодно близко исходя из текущих надобностей. Во-вторых, Why dependent types matter, стр 9 и стр 21. Сортировка векторов слиянием, сама функция слияния с доказательством сохранения размера и с доказательством получения упорядоченного вектора. От самого алгоритма слияния отличается только наличием типов. Как и было сказано выше, большинство действий определяются небольшим количество информации из внешней спецификации.

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

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

T>Делаем проверку на равенство. Если равны, то можно zip. Не равны, отрежем кого. Или приклеим кому.
Непонимать. Еще раз

listA = getListA (void -> Vec A n) //читает список из файла listA.txt
listB = getListB (void -> Vec B n) //читает список из файла listB.txt

zip listA listB // как тут компилятор понимает какой длинны listA и listB

(Вместо чтения из файла может быть все что угодно)

Делаем равное количетсво записей в listA.txt и listB.txt программа копилируется,
меняем на не равное, не компилируется, так?

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

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

D>Непонимать. Еще раз

listA = getListA (void -> Vec A n)
listB = getListB (void -> Vec B n)

zip listA listB // как тут компилятор понимает какой длинны listA и listB

D>(Вместо чтения из файла может быть все что угодно)

D>Делаем равное количетсво записей в listA.txt и listB.txt программа копилируется,
D>меняем на не равное, не компилируется, так?

Во-первых, код будет выглядеть скорее так:

do
  listA <- getListA : IO (Vec A n) //побочные эффекты в IO
  listB <- getListB : IO (Vec B n) //

  ... zip listA listB ... // и что-то с этим результатом будем ещё делать

Откуда взялась переменная n? Если она уже определена выше, и строчки с listA и listB скомпилировались, то компилятор уже знает, что listA и listB имеют одинаковую длину.

Если имеется ввиду, что getListA имеет тип IO (Vec A n), то это сокращённая запись для {forall A n}(IO (Vec A n)), то есть getListA обещает вернуть список любой длины и любого типа, который нужен. Естественно, чтение из файла такого типа иметь не будет. А будет оно иметь тип

IO {exists n}(Vec A n)
IO {exists n}(Vec B n)

То есть возвращается список некоторой натуральной длины. Естественно, эти n могут быть разными.

Но нам ничто не мешает написать функцию

zip' : (Vec A n) -> (Vec B m) -> (Vec (A,B) (min n m))

которая соответствует второму варианту VladD2.

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

D>Наверное имелось в виду
D>

D>listA = getListA (void -> Vec A n)
D>listB = getListB (void -> Vec B n)

D>zip listA listB // как тут компилятор понимает какой длинны listA и listB
D>

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

Короче как ни крутись, а проверка ввода нужна всегда.

А вот после того как ввод проверен уже никакие проверки не нужны.

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

AR>Если имеется ввиду, что getListA имеет тип IO (Vec A n), то это сокращённая запись для {forall A n}(IO (Vec A n)), то есть getListA обещает вернуть список любой длины и любого типа, который нужен. Естественно, чтение из файла такого типа иметь не будет. А будет оно иметь тип
AR>

AR>IO {exists n}(Vec A n)
AR>IO {exists n}(Vec B n)
AR>

AR>То есть возвращается список некоторой натуральной длины. Естественно, эти n могут быть разными.

AR>Но нам ничто не мешает написать функцию
AR>

AR>zip' : (Vec A n) -> (Vec B m) -> (Vec (A,B) (min n m))
AR>

AR>которая соответствует второму варианту VladD2.
Нам то ничего не мешает написать все что угодно, но поинт то был в том что бы zip принимал только списки одинаковой длинны и ругался при компиляции если это не так.

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

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

AR>>Но нам ничто не мешает написать функцию
AR>>

AR>>zip' : (Vec A n) -> (Vec B m) -> (Vec (A,B) (min n m))
AR>>

AR>>которая соответствует второму варианту VladD2.
D>Нам то ничего не мешает написать все что угодно, но поинт то был в том что бы zip принимал только списки одинаковой длинны и ругался при компиляции если это не так.

Ну именно так всё и есть. Ты не можешь встроить вызов zip в то место, где нет статической гарантии "равнодлинности" векторов-параметров. Если их нет, то ты либо должен обеспечить такие гарантии ручками (скажем, обеспечив механизм параллельного чтения элементов списка из файлов, по построению гарантирующего равную длину векторов), либо пользоваться версией zip', которая игнорирует хвост длиннейшего.

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

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

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

AR>>>Но нам ничто не мешает написать функцию
AR>>>

AR>>>zip' : (Vec A n) -> (Vec B m) -> (Vec (A,B) (min n m))
AR>>>

AR>>>которая соответствует второму варианту VladD2.
D>>Нам то ничего не мешает написать все что угодно, но поинт то был в том что бы zip принимал только списки одинаковой длинны и ругался при компиляции если это не так.

D>Ну именно так всё и есть. Ты не можешь встроить вызов zip в то место, где нет статической гарантии "равнодлинности" векторов-параметров. Если их нет, то ты либо должен обеспечить такие гарантии ручками (скажем, обеспечив механизм параллельного чтения элементов списка из файлов, по построению гарантирующего равную длину векторов), либо пользоваться версией zip', которая игнорирует хвост длиннейшего.

Именно.

AR>>Но нам ничто не мешает написать функцию
AR>>

AR>>zip' : (Vec A n) -> (Vec B m) -> (Vec (A,B) (min n m))
AR>>

AR>>которая соответствует второму варианту VladD2.
D>Нам то ничего не мешает написать все что угодно, но поинт то был в том что бы zip принимал только списки одинаковой длинны и ругался при компиляции если это не так.

http://thesz.livejournal.com/860912.html?thread=6304240#t6304240

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

T>>Перечисли, пожалуйста, что же можно проверить контектом.
G>Много чего, только не получится расширить существующие типы для обеспечения проверок. Поэтому упорядоченность списка не получится прверить.

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

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

WH>>

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

VD>Кстати, так уже намного лучше. Это гипотетический синтаксис или Агда?

VD>Не ясно только зачем нужен "forall{A B n} -> ". Это объявление явно лишнее и сбивает с толку.

Ну, вот видишь Vec, он с внешнего контекста, т.е. определён где-то снаружи, а forall говорит, что типы A,B,n искать снаружи не надо — это типы-переменные. Пример — В Haskell forall не пишется потому, что типы-переменные выделяются синтаксически — у них первая буква строчная. Т.е. это вопрос синтаксиса. Вполне возможен синтаксис, когда forall писать не обязательно — нашёл снаружи тип с таким именем — значит, это конкретный тип, не нашёл — тип-переменная. Но по вполне понятным причинам такой синтаксис нам не нужен :-)

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

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

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

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

VD>>Я повторюсь, но мне не понятно, как компилятор сможет проверить работу со списками большая часть которых получается динамически?
VD>>Или мы будем работать отдельно с динамическими списками (и при этом все проверки пойдут на смарку), и отдельно со статическими?
WH>Ты точно не понял что к чему.

Ну, так поясни, а не декларируй никому не интересные вещи о моем понимании.

WH>Непривычно? Да.
WH>Сложно? Нет.

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

WH>Решает.

Пока что видны только декларации. Ты так и не рассказал как будет осуществляться контроль времени компиляции, если в функцию передать аргументы полученные динамически.

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

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

VD>>Многословность != непонятность. Сравним два варианта:
VD>>

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

VD>>и
VD>>

VD>>zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
VD>>  requires l1.Lenght == l2.Lenght
VD>>  ensures  value.Lenght == l1.Lenght
VD>>

WH>Сравнил. Мне первый понятнее.

Ну, что же. Можешь радоваться, так как ты вместе с еще 3 человеками сможешь в этом во всем разбираться.
Лично я очень не хотел бы по пол часа въезжать в объявление примитивной функции. Все же граничные условия — это дело десятое. Контролировать их конечно полезно, но знать о них чтобы программировать не обязательн.

WH>Более того он формален в доску чего не скажешь о костылях во втором случае.

Формальность — это хорошо для компьютера, или для писателя компилятора. А вот для человека важна простата понимания.

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

VD>>Приведенный тобой пример описания типа функции в двое длиннее тела функции и в 10 раз не понятнее (на мой взгляд).
WH>Ну давай запишем это в более привычном тебе виде:
WH>

WH>zip{A, B, n}(l1 : Vec A n, l2 : Vec B n) : Vec (A * B) n
WH>

WH>С синтаксисом можно обходится весьма вольно.

Я не сказал бы, что приведенный пример привычен, но он куда короче и понятнее (но без домысливания не обойтись). Отличие B от n без пояснений не видать. Плюс не ясно, что такое Vec? Ну, и синтаксис тоже весьма привычный.
Возможно как-то так было бы понятнее:

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

В прочем — это тоже довольно громоздко.

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

VD>>Что у нас с динамическими списками? Что у нас с вводом / выводом?
WH>А что с ними?

Это бы вопрос к тебе. Ты упорно обходишь ответ на него.

VD>>Что, наконец с логикой? Как в систему типов загнать информацию о поведении не тривиального кода?
WH>Берешь и загоняешь. Декомпозицию никто не отменял.

Я не вижу в твоих примерах декомпозиции.

Вот если бы эти зависимости можно было выражать как-то по другому...
Например, при описании списка мы указываем, что у него есть один неявный параметр типам целочисленного типа, и что он связан со значением свойства Length. Тогда приведенный пример можно было бы описать очень просто и изящно:

zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
  types invariant l1.Lenght = l2.Lenght = result.Lenght
{
  ...
}

Это было бы и кратко, и понятно не посвященным.

VD>>Я не заметил чего-то выносящего мозг. Видимо по второму разу данная трава уже не так выносит .
VD>>Я заметил "много букв" при не вполне понятном результате.
WH>Много букв это у тебя. И результат не понятен опять таки тебе.

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

WH>С синтаксисом можно сделать все что угодно. И ты не хуже меня жто знаешь.

Дык очень важно найти оптимальный синтаксис. Иначе это так и останется академической игрушкой.

WH>А возможности у этой механики очень большие.

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

GetData[int, n : int]() : list[int, n]

и есть твой Zip:

Zip[A, B, len : int](l1 : list[A, len], l2 : list[B, len]) : list[A * B, len]

И мы пишем:

def res = Zip(GetData(), GetData());
WriteLine(res);

Как на это отреагирует компилятор?
Если не даст скомпилировать, то как нам написать рабочий вариант?

ЗЫ

Кстати, идея PRG-парсера умерла так и не родившись?

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

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

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

VD>>>Многословность != непонятность. Сравним два варианта:
VD>>>

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

VD>>>и
VD>>>

VD>>>zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
VD>>>  requires l1.Lenght == l2.Lenght
VD>>>  ensures  value.Lenght == l1.Lenght
VD>>>

WH>>Сравнил. Мне первый понятнее.

VD>Ну, что же. Можешь радоваться, так как ты вместе с еще 3 человеками сможешь в этом во всем разбираться.
VD>Лично я очень не хотел бы по пол часа въезжать в объявление примитивной функции. Все же граничные условия — это дело десятое. Контролировать их конечно полезно, но знать о них чтобы программировать не обязательн.

WH>>Более того он формален в доску чего не скажешь о костылях во втором случае.

VD>Формальность — это хорошо для компьютера, или для писателя компилятора. А вот для человека важна простата понимания.

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

Синтаксис этот скорее непривычный, чем сложный.

В первом случае мы имеем просто тип. Во втором -- тип отдельно, условия отдельно.

VD>>>Приведенный тобой пример описания типа функции в двое длиннее тела функции и в 10 раз не понятнее (на мой взгляд).
WH>>Ну давай запишем это в более привычном тебе виде:
WH>>

WH>>zip{A, B, n}(l1 : Vec A n, l2 : Vec B n) : Vec (A * B) n
WH>>

WH>>С синтаксисом можно обходится весьма вольно.

VD>Я не сказал бы, что приведенный пример привычен, но он куда короче и понятнее (но без домысливания не обойтись). Отличие B от n без пояснений не видать. Плюс не ясно, что такое Vec? Ну, и синтаксис тоже весьма привычный.
VD>Возможно как-то так было бы понятнее:
VD>

VD>zip[A, B, len : int](l1 : list[A, len], l2 : list[B, len]) : list[A * B, len]
VD>

VD>В прочем — это тоже довольно громоздко.

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

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

Type вместо агдовского Set. int тут тоже в общем-то не при деле, поскольку списков с отрицательной длиной не бывает -- но это ладно. Единственная причина, по которой в C#/Nemerle/Haskell не нужно указывать, что A и B типы -- это отсутствие других возможностей. Можно попробовать грязный хак вроде "все параметры функции или типа, тип которых не указан, имеют тип Type", но идея так себе.

VD>Ну и вопрос о то, что будет в случае динамического формирования списка так же остается открытым. Как проверить тело по сигнатуре в обще ясно, но как проверить все вызовы этого метода?

VD>Например, при описании списка мы указываем, что у него есть один неявный параметр типам целочисленного типа, и что он связан со значением свойства Length. Тогда приведенный пример можно было бы описать очень просто и изящно:
VD>

VD>zip[A, B](l1 : list[A], l2 : list[B]) : list[A * B]
VD>  types invariant l1.Lenght = l2.Lenght = result.Lenght
VD>{
VD>  ...
VD>}
VD>

VD>Это было бы и кратко, и понятно не посвященным.
В "инвариантах" может быть далеко не только равенство, а любые условия. Так что скорее инвариант должен выглядеть как

l1.Length == l2.Length, l1.Length == result.Length

Уже хуже.

Неявные параметры для типов -- это понятно непосвящённым? Почему неявный параметр -- именно длина, а не (например) первый элемент списка? Мне не хотелось бы каждый раз раз лезть в определение списка и выяснять, какие свойства можно использовать в инвариантах, а какие -- нет.

Давай ещё сделаем A и B неявными:
zip(l1 : list, l2 : list) : list
types invariant l1.Length == l2.Length, l1.Length == result.Length,
value.Type == l1.Type * l2.Type
{
...
}
[/c#]
По-моему, это не стало ни понятнее, ни короче. Точно так же вариант с длиной как неявным параметром мне не нравится.

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

GetData[int, n : int]() : list[int, n]

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

GetData() : (n : int) * list(int, n)

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

VD>и есть твой Zip:
VD>

Zip[A, B, len : int](l1 : list[A, len], l2 : list[B, len]) : list[A * B, len]

VD>И мы пишем:
VD>

VD>def res = Zip(GetData(), GetData());
VD>WriteLine(res);
VD>

VD>Как на это отреагирует компилятор?

С твоим вариантом GetData? Это зависит от того, есть ли правила для значений неявных параметров по умолчанию, когда их не удаётся вывести. Если да, то он выведет неявные параметры так:

def res : list[int * int, 0] = Zip[int, int, 0](GetData[0](), GetData[0]());
WriteLine(res);

Если нет, то выдаст ошибку из-за невозможности вывода длины.

С нормальным GetData -- нужно сначала исправить программу. В частности, если используем выриант

def (n,data1) = GetData(); // data1 : list(int, n)
def (m,data2) = GetData(); // data2 : list(int, m)
def res = Zip(GetData(), GetData());
WriteLine(res);

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

VD>Если не даст скомпилировать, то как нам написать рабочий вариант?

А для этого нужно решить, что считать рабочим вариантом. Как эта функция должна себя вести, если списки имеют разную длину?

1. Выдать исключение.
2. Отбросить "лишние" элементы из более длинного списка.

Скажем, второй.

Zip1[A : Type, B : Type, n : int, m : int](l1 : list[A, n], l2 : list[B, m])
{
  def k = min(n, m);
  def l1' = Take(l1, k);
  def l2' = Take(l2, k);
  return Zip(l1', l2');
}

Main() : void
{
  def (_,data1) = GetData();
  def (_,data2) = GetData();
  def res = Zip1(GetData(), GetData());
  WriteLine(res);
}

Это проходит проверку типов: в Zip1 компилятор знает, статически, что: k <= n, k <= m, l1' и l2' имеют длину k и поэтому к ним можно применить Zip; в Main компилятор знает, что Zip1 применимо к любым спискам.

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

VD>А вот для человека важна простата понимания.

Анатомические открытия на rsdn.ru!
(простите, не удержался)