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

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

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

Аналогия — для того, чтобы написать функцию, складывающую два числа, нам не нужно знать точные значения, которые будут в неё передаваться. Нам достаточно декларировать, что они оба являются числами. Так и здесь — для того, чтобы написать функцию склеивания двух списков, нам достаточно декларировать, что они имеют одинаковую длину. Если это не так (или компилятор не сможет доказать) — компиляция не пройдёт. Поэтому для общего случая эта функция работать не будет. Она будет работать только для случаев, когда у списков одинаковые длины.

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

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

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

Тут ещё не раз не показали как это можно сделать. А то, что зависимые типы сокращают и упрощают код было уже показано несколько раз.

VD>Но в таком виде функцию по сложнее уже будут воспринимать далеко не все.

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

P.S. Зависимые типы — это следующий шаг после Хиндли-Милнера, который есть следующий шаг после статической типизации

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>Это было бы и кратко, и понятно не посвященным.

Ты придираешься к конкретным вещам, упуская из виду общие.

То, о чём ты говоришь, навевает мысли о так называемом экстенсиональном равенстве. У нас списки имеют общие свойства (длины совпадают), типы связаны A -> B -> (A,B) и на всё остальное мы не смотрим. Такой вид рассуждений приводит к принципиально неразрешимому (undecidable) алгоритму проверки зависимых типов. Что приведёт к необходимости отключать части проверяющего алгоритма, чтобы он хоть как-то работал, и к возможности протянуть ошибку в рассуждениях.

Современные проверяльщики зависимых типов данных работают с интенсиональным равенством. Для них a+b не равно b+a.

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

Ситуация улучшается. Недавно придумали так называемое наблюдаемое (observational) равенство. Для него a+b равно b+a.

Я думаю, придумают и ещё что-то.

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

L>Есть разные способы, например, мы можем написать функцию, проверяющую — одинаковая ли длина у списков, и если одинаковая вызвать нашу функцию склейки. Компилятор это дело пропустит, т.к. в данном месте будет доказано, что у списков одинаковая длина.

То есть, мы усложняем код вводя дополнительные функции и проверки?

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

L>Тут ещё не раз не показали как это можно сделать. А то, что зависимые типы сокращают и упрощают код было уже показано несколько раз.

Где это было показан?

VD>>Но в таком виде функцию по сложнее уже будут воспринимать далеко не все.

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

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

L>P.S. Зависимые типы — это следующий шаг после Хиндли-Милнера, который есть следующий шаг после статической типизации

Хиндли-Милнера? Вы меня извините, но в этой системе типов нет ничего выдающегося. В чистом виде она не удобна и весьма убога. А зависимые типы по идее могут применяться с любой системой типов.

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

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

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

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

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

То есть верифицировать весь код и заставлять писать все проверки?

А не офигеш ли это делать?

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

Кто-нибудь проводил сравнение трудозатрат вызванных тестированием и вызванных тотальными проверками всех нюансов?

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

L>>Есть разные способы, например, мы можем написать функцию, проверяющую — одинаковая ли длина у списков, и если одинаковая вызвать нашу функцию склейки. Компилятор это дело пропустит, т.к. в данном месте будет доказано, что у списков одинаковая длина.

VD>То есть, мы усложняем код вводя дополнительные функции и проверки?

Нет, мы упрощаем код, вводя проверку всего один раз на самом верху (ну или в нужном, но одном месте).
В обычном случае нам приходится постоянно проверять на null, либо знать, что может вылететь NPE (это фактически встроенная та самая дополнительная функция с проверкой, которую ты упомянул), а тут проверку заставляет сделать компилятор, но всего один раз, а дальше мы уже знаем, что ссылка not null.
Это как пример.

Здравствуйте, 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.

Вот это уже конструктив! Я вообще, поражаюсь с умений некоторых наших завсегдатаев вместо объяснений разводить флуд.

Стало быть над аргументами типов можно производить вычисления?
Если так, то не приведет ли это к проблемам С++ когда систему типов нечнут использовать как мета-язык вместо того, чтобы использовать ее по назначению?

Еще вопрос...
Как будет выглядеть код с проверками. Скажем, что у нас и правда есть два файла и мы предполагаем, что в 99.999% случаев в них будет одинаковое количество элементов. Но файл может быть, скажем так, испорчен и потенциально длинна может оказаться разно.
Напиши гипотетический код который читает эти файлы и склеивает их результат (разумеется с проверками).

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

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

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

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

VE>Нет, мы упрощаем код, вводя проверку всего один раз на самом верху (ну или в нужном, но одном месте).
VE>В обычном случае нам приходится постоянно проверять на null, либо знать, что может вылететь NPE (это фактически встроенная та самая дополнительная функция с проверкой, которую ты упомянул), а тут проверку заставляет сделать компилятор, но всего один раз, а дальше мы уже знаем, что ссылка not null.
VE>Это как пример.

Я уверен, что зависимые типы ничем не могут помочь с NRE. Более того эта проблема легко решается (и, кстати сказать, отсуствует в ОКамле и Хаскеле) самой системой типов. Достаточно описать допускающие null типы и не допускающие, а так же описать возможность явного и/или не явного преобразования между ними. Далее для переменных не допускающих null типов компилятор должен требовать инициализацию.

Кстати, на мой взгляд проблема NRE создает куда больше проблем на практике. Вот ее бы решить в мэйнстриме!

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

VD>То есть, мы усложняем код вводя дополнительные функции и проверки?

Усложняем по сравнение с чем? Все эти дополнительные проверки мы пишем и с контрактами, только работать и ломаться код с контрактами будет в рантайме.
Вернёмся к рассматриваемому примеру — ты описал на контрактах функцию склеивающую два списка одной длины. И посмотри, что ты будешь делать с ней, когда списки получены динамически, может так тебе будет проще взглянуть на тот же пример со стороны ЗТ.

VD>>>Сложно. Много шума. Это видно очень отчетливо. Возможно все тоже самое можно было бы записать в несколько раз проще.
L>>Тут ещё не раз не показали как это можно сделать. А то, что зависимые типы сокращают и упрощают код было уже показано несколько раз.
VD>Где это было показан?

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

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

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

VD>Хиндли-Милнера? Вы меня извините, но в этой системе типов нет ничего выдающегося. В чистом виде она не удобна и весьма убога. А зависимые типы по идее могут применяться с любой системой типов.

Возможно. Я не очень близко знаком с зависимыми типами, для меня это лямбда-P из лямбда-куба. Т.е. её применение я пока вижу только в чистых системах типов (PTS).

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

VD>Я уверен, что зависимые типы ничем не могут помочь с NRE. Более того эта проблема легко решается (и, кстати сказать, отсуствует в ОКамле и Хаскеле) самой системой типов. Достаточно описать допускающие null типы и не допускающие, а так же описать возможность явного и/или не явного преобразования между ними. Далее для переменных не допускающих null типов компилятор должен требовать инициализацию.

Да, согласен, зависимые типы не очень-то нужны для решения NPE. С другой стороны есть схожие проблемы — например, работать с ресурсом, будучи уверенным, что он инициализирован и не освобождён, или уже приводившийся пример с решением проблемы дедлока. Ну и кучу всего можно придумать, где типы выгодно индексировать.

VD>Кстати, на мой взгляд проблема NRE создает куда больше проблем на практике. Вот ее бы решить в мэйнстриме!

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

VD>Я уверен, что зависимые типы ничем не могут помочь с NRE.
Ну почему же. Если обращение по ссылке (т.е. сама .) будет требовать доказательсвта ненулёвости, то выхода будет всего два:
1. Требовать такое док-во самому (т.е. указывать в декларации функции, что ты принимаешь только ненулевой указатель)
2. Делать проверку на null и обрабатывать ошибку. Разумеется, в кач-ве обработки можно кинуть исключение, но это уже не будет NRE, потому что если ты не знаешь, что делать с null — выбери пункт 1, а если знаешь, то обработка будет осмысленной.

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

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

L>Вернёмся к рассматриваемому примеру — ты описал на контрактах функцию склеивающую два списка одной длины. И посмотри, что ты будешь делать с ней, когда списки получены динамически, может так тебе будет проще взглянуть на тот же пример со стороны ЗТ.

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

L>>>Тут ещё не раз не показали как это можно сделать. А то, что зависимые типы сокращают и упрощают код было уже показано несколько раз.
VD>>Где это было показан?

L>Ну как же, одной строчкой заменяем кучу юнит тестов — сокращение. Простой и явной декларацией в типах заменяем мутные контракты, описывающие ограничения реализации — упрощение.

Да, ну. В юнит-тесте я убду проверять большой блок функциональности и при этом, возможно, не напишу кучи совершенно не нужных проверок (которые заставит меня написать система типов с зависимостями).

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

Что до надежности, то припоны которые начнет чинить компилятор (а программист именно так это будет воспринимать) начнут обходиться разными путями. Так что ошибки никуда не денутся. Да и ошибки бывают логичекими. Ну, не верный алгоритм. И что тут компилятор скажет? Он же не знает как надо? Для него верен тот алгоритм который может скомпилироваться.

L>Я что хочу сказать — нам не должно быть дело до того, чтобы написаное нами воспринималось всеми. Инструмент должен быть полезен, удобен, понятен в работе в первую очередь тому, кто будет писать и поддерживать код.

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

VD>>Хиндли-Милнера? Вы меня извините, но в этой системе типов нет ничего выдающегося. В чистом виде она не удобна и весьма убога. А зависимые типы по идее могут применяться с любой системой типов.

L>Возможно. Я не очень близко знаком с зависимыми типами, для меня это лямбда-P из лямбда-куба. Т.е. её применение я пока вижу только в чистых системах типов (PTS).

Я вижу, что зависимые типы спокойно прокатят и в номинальной системе типов с подтипами а-ля С++/Ява/дотнет.

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

VD>Стало быть над аргументами типов можно производить вычисления?
VD>Если так, то не приведет ли это к проблемам С++ когда систему типов нечнут использовать как мета-язык вместо того, чтобы использовать ее по назначению?

Так система типов — это та же лямбда! Почему бы над ней и не попроводить вычисления? Единственное отличие — язык системы типов должен быть тотальным.

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

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

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

Дык переменные типы можно описывать в скобках как в С++, Яве и дотнете. Выкидываем "forall{A B n} ->" и добавляем "zip<A, B, n>".

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

T>>Делаем проверку на равенство. Если равны, то можно zip. Не равны, отрежем кого. Или приклеим кому.
VD>То есть верифицировать весь код и заставлять писать все проверки?

Не больше, чем обычно.

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

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

VD>Кто-нибудь проводил сравнение трудозатрат вызванных тестированием и вызванных тотальными проверками всех нюансов?

Да нет же, тут в чём прикол — небольшой декларацией ты гарантируешь, что функция sortSomething вернёт отсортированную структуру, то же самое на более пузатых юнит-тестах ты просто не сделаешь, а контракты, которые не будут такими небольшими, смогут сработать только в рантайм. О каких трудозатратах идёт речь?

Ну и разумеется, почему это ЗТ должны заниматься тотальными проверками всех нюансов, а тестирование не всех? После этого просто нечестно сравнивать трудозатраты.

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


L>Так система типов — это та же лямбда! Почему бы над ней и не попроводить вычисления?

Потому, что результат печальный выходит. В коде могут разобраться 1-2 процента программистов, а остальные тихо ...
Для МП должны быть явные и простые средства. Система же типов должна уменьшать количество ошибок и предоставлять метаиформацию (рефлексия, интелисенс в IDE и т.п.).

L>Единственное отличие — язык системы типов должен быть тотальным.

Переведи.

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

VD>Дык переменные типы можно описывать в скобках как в С++, Яве и дотнете. Выкидываем "forall{A B n} ->" и добавляем "zip<A, B, n>".

А ты про это! Ну это уже вопрос синтаксиса, мне не очень интересно, если честно.

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

Грохнул весь ответ (много букв), так как важна только последняя мысль...

L>Ну и разумеется, почему это ЗТ должны заниматься тотальными проверками всех нюансов, а тестирование не всех? После этого просто нечестно сравнивать трудозатраты.

Да потому, что туча проверок по жизни не нужно. Потому, что программа спокойно может работать "недописанной". Я могу написать алгоритм для обычных условий, а проблемы отловят контракты. Что-то во время компиляции, что-то в рантайме. И меня это в большинстве случаев устроит.

Более того. Ну, представим компилятор заставил меня обрабатывать какие-то несоответствия. ОК. А как я их обработаю? Ну, не сошлась у меня длинна двух списков перед вызовом zip-а. И что мне делать? Исключения кидать? Дык, а зачем я тогда пишу код проверок? Пусть его кидает сам zip.
Писать какой-то код реакции? Дык это может резко увеличить объем работы и при этом один хрен многие схалтурят и напишут какую-нибудь ересь.

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

VD>Более того. Ну, представим компилятор заставил меня обрабатывать какие-то несоответствия. ОК. А как я их обработаю? Ну, не сошлась у меня длинна двух списков перед вызовом zip-а. И что мне делать? Исключения кидать? Дык, а зачем я тогда пишу код проверок? Пусть его кидает сам zip.
VD>Писать какой-то код реакции? Дык это может резко увеличить объем работы и при этом один хрен многие схалтурят и напишут какую-нибудь ересь.

Эм, а без зависимых типов ты как с такими бедами справляешься? Оставляешь на самотёк что ли?

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

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

Ну да, точно так же и с ЗТ. Зависит от ситуации, что именно ты будешь делать. Предложенное мной решение — всего лишь один из вариантов.

VD>Да, ну. В юнит-тесте я убду проверять большой блок функциональности и при этом, возможно, не напишу кучи совершенно не нужных проверок (которые заставит меня написать система типов с зависимостями).

Возможно, я где-то что-то упустил. Насколько я понимаю, идёт сравнение того, что и как выражается с помощью ЗТ и юнит-тестов? Если да, то зачем нам писать ненужные проверки при ЗТ и не писать при юнит-тестах?

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

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

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

Ну, тут ничто не поможет, давай всё таки сравнивать аналогичное.

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

Не понимаю аргументации. Я вот в vim-е пишу очень много кода. Это очень удобный инструмент. От него польза мне, а не обществу.
Если же ты имеешь в виду, что код с ЗТ писать медленнее, то могу поделиться только своим небогатым опытом. Индексированные типы и open functions (это "почти" ЗТ в Haskell) облегчают мне написание кода. Ощущение свободы больше, когда ограничения накладываются более явно.

VD>Я вижу, что зависимые типы спокойно прокатят и в номинальной системе типов с подтипами а-ля С++/Ява/дотнет.

Сорри, не компетентен я в этом, возможно, прокатят, я не вижу как.