ооп и функциональщина кратко, внятно.

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

Свойства конкретных программ нам на практике не нужны.

А я как-то привык ориентироваться на свойства. Ну типа — открываешь man/документацию, читаешь про свойства :) Смотришь нетривиальные (и не очень) свойства программ/алгоритмов/конкретных структур данных/интерфейсов с помощью тех или иных формальных моделей.

Не обязана. Но если она этого не делает - то она не нужна.

Я сказал зачем нужна — статический анализ и оптимизации конкретных программ.

Ты сам себе противоречишь

То есть ты пишешь программу на си с ошибками, потом пишешь к ней propositions для желаемых свойств с ошибками, потом долго и упорно доказываешь на Coq в модельном окружении что программа с ошибками удовлетворяет этим утверждениям с ошибками, и у тебя даже получается это доказать? Не верю :)

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

Ну обычный компилятор не проверяет то что проверяет Frama-C/Jessie, поэтому второй это _строго дополнительное_ средство, иначе бы смысла не было.

В разработке новых через формализацию они как раз бесполезны, т.к. тогда точно никаких новых свойств не будет.

И не надо, если язык разрабатывают люди которые таки _знают_ теории и разные модели (для примера — Маккарти, Бэкус, Томпсон, SPJ, Одерски, Степанов, а в качестве бэкграунда явно прослеживается Чёрч, Пост, Тьюринг, Гёдель, Хомский, Клини, Скотт, Рабин, Хоар, Милнер, Гирард, Рейнольдс, Пирс, Кардели, Адаби, Могги ..., а у Степанова вообще забавно), так что ничего не связывает их в реализации языка с такими свойствами, которые нужны для нужд диктуемых его подразумеваемыми применениями.

комплексные числа

Да ну ради бога, пусть они где-то локально очень редко применяются 3.5 анонимусами

Как интересно.

Зависимые типы - это просто ненужное усложнение концепций, которым уже 50 лет.

Сколько лет ∀ и ∃? Посмотри Sheaves in Geometry and Logic на тему зависимых типов. То есть тупо ∀(x : T). P[x] в логике, что в языке со статической типизацией? Очевидно, функция (x : T) -> U[x], только вместо термов-утверждения будут типы, даже C++ так умеет, ну а в пределе мы хотим типы экспрессивные не менее самих термов (если std::array<T, n + m> — то n + m это, очевидно, терм, и вообще туда подразумевается впиливать любой терм, то есть любые вычисления (и в C++ с constexpr функциями это даже можно делать — рекурсия, тернарный оператор, Тьюринг-полнота)). Аналогично ∃(x : T). P[x], в ЯП должен быть несколько более конструктивен — не просто «существует», а что и сколько, то есть фактически нужно декартово произведение, то есть кортеж struct { T x; U[x] y }; — такого пока ещё не особо заметно в распространённых языках.

В программирование их тащить нельзя, потому что не нужно.

Ну так тащут же. Ещё раз — если тащить статическую типизация как таковую, то всё — зависимые типы это must have, и в C++ они есть (пойти, штоле, попробовать доказать какую-нибудь теоремку на шаблонах, а то кроме 2+2=4 ничего толком ещё не пробовал :)).

Ну типа — открываешь man/документацию, читаешь про свойства

Ну так это не те, что получаются из формализации.

Я сказал зачем нужна — статический анализ и оптимизации конкретных программ.

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

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

При чем в proposition ошибок почти всегда будет больше, чем в самой программе, не забывай :)

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

Именно так.

и у тебя даже получается это доказать? Не верю :)

Смотри, на самом деле ты делаешь следующее:

1. Пишешь программу на языке X с ошибками

2. Пишешь программу на языке Y с ошибками.

При чем языки X и Y близки семантически и далеки синтаксически. Компилятор пытается доказать, что обе программы делают одно и то же. Да, вполне возможна ситуация, при которой ты сделал _одинаковые_ ошибки. Но это маловероятно, конечно же. То есть все, что придумали CS-теоретики - это просто писать одну программу два раза (обычный raid 1 такой, только руками :)). Коненчо, идея тривиальная, да и если ты предложишь человеку прямо «пиши программу дважды», то он тебя нахуй пошлет. По-этому CS-теоретики все это обвязывают ненужно усложненной терминологией и прячут, таким образом, лес за деревьями :)

Ну обычный компилятор не проверяет то что проверяет Frama-C/Jessie, поэтому второй это _строго дополнительное_ средство, иначе бы смысла не было.

Не понял как это связано с тем, что я писал.

отсутствие композабельности

Например?

Если речь про вещи типа попыток ∀ {x y} → x ≡ y → y ≡ x отождествить с id, то тут как — выглядит оно как id, то есть один refl переводит в другой refl, но это разные refl у них разные типы — x ≡ y и y ≡ x, а у id тип ∀ {A} → A → A, то есть совсем (definitional/computational) одинаковые A. Вот в случае 1 + 1 ≡ 1 + 1 → 2 ≡ 2 — пожалуйста, можно id, если computational работает.

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

Пока теоретизируешь ты — вот если бы конкретно сказал, «вот, мол, взял я Frama-C, написал такую программу, написал ей такие свойства, сделал это и то и получилась у меня в итоге такая-то нехорошая ситуация». А вот обломаться об свойства написав некорректную программу как раз можно — авторы этого добра на реальном коде и CVE проверяли.

Как интересно.

при чем тут комплексные числа, янепонел. Это ты их приплел, а у нас речь шла про октанионы, если не ошибаюсь.

Сколько лет ∀ и ∃?

Не знаю, если честно. Но я думал, достаточно много. И Аристотелевы силлогизмы эквивалентны логике первого порядка или нет? Я вот не в курсе. Интуитивно - вроде эквивалентны.

Аналогично ∃(x : T). P[x], в ЯП должен быть несколько более конструктивен — не просто «существует», а что и сколько, то есть фактически нужно декартово произведение, то есть кортеж struct { T x; U[x] y }; — такого пока ещё не особо заметно в распространённых языках.

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

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

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

Ну так тащут же.

Ну да, единицы - пишут. Как 50 лет назад писали, так и сейчас пишут, И через 50/100/200 лет так же эти же программы (единицы) будут писать с доказательством корректности :)

Ещё раз — если тащить статическую типизация как таковую, то всё — зависимые типы это must have

Нет, они лишние, абсолютно. Они мешают, при чем _сильно_ мешают. Очень далеко за пределами «ненужности».

и в C++ они есть

Нет, нету.

Например?

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

Пока теоретизируешь ты — вот если бы конкретно сказал, «вот, мол, взял я Frama-C, написал такую программу, написал ей такие свойства, сделал это и то и получилась у меня в итоге такая-то нехорошая ситуация».

Так я же сказал - хоть и можно, но маловероятно (хоть гарантий и нет, можно и одну ошибку два раза посадить). Мои претензии к тому, что все это обвязывается ненужной терминологией и тщательно скрывается, вместо того, чтобы честно сказать: «ребята, мы написали для вашего языка альтернативный синтаксис и проверяльщик эквивалентности программ на оригинальном синтаксисе и на новом, теперь вы пишете программу два раза, и пока проверяльщик не покажет, что программы одинаковые - оно не компилируется».

Ну так это не те, что получаются из формализации.

Сигнатуры типов. Цепи Маркова, автоматы, FSM, ER, EBNF и т.п. Или посмотри документацию на Erlang, например — какие там описания используются. Ну или тот же UML. Плюс предметная область может располагать.

(хоть гарантий и нет, можно и одну ошибку два раза посадить)

Хотя если семантику отдалить, то можно, наверное, и исключить этот вариант. Не видел эту Frama-C, а вот в том же JML влегкую такой пример (с повторной ошибкой) пишется.

Сигнатуры типов. Цепи Маркова, автоматы, FSM, ER, EBNF и т.п.

Что-то ты все уже в одну кучу намешал. Не надо так.

Ну или тот же UML.

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

Плюс предметная область может располагать.

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

при чем тут комплексные числа, янепонел. Это ты их приплел, а у нас речь шла про октанионы, если не ошибаюсь.

Ну ты отвечал на «как все три используются ...», а их всего три (четыре с R), больше нет. Так что... Это ж вещи одного порядка — http://en.wikipedia.org/wiki/Hypersphere#Specific_spheres, то есть вопрос тут пригодятся ли спиноры высшего порядка или нет.

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

И Аристотелевы силлогизмы эквивалентны логике первого порядка или нет?

Главное, что оно там есть.

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

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

А так — да, http://en.wikipedia.org/wiki/Proof_assistant#Comparison_of_systems.

Как и

Мои претензии к тому, что все это обвязывается ненужной терминологией и тщательно скрывается, вместо того, чтобы честно сказать: «ребята, мы написали для вашего языка альтернативный синтаксис и проверяльщик эквивалентности программ на оригинальном синтаксисе и на новом, теперь вы пишете программу два раза, и пока проверяльщик не покажет, что программы одинаковые - оно не компилируется».

Внезапно — http://frama-c.com/what_is.html, это до тезисов и статей нужно добираться, а то они тщательно скрываются :)

В языке вообще никаких типов не обязательно.

Ну да, единицы - пишут.

Единицы — на языках со статической типизацией %)

Нет, нету.

Есть, но не всё и не правильно (то есть нужно следить за вещами как тому школьнику в совершенстве владеющему FOL).

Нельзя использовать сторонние библиотеки

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

Что-то ты все уже в одну кучу намешал.

Это первые попавшиеся примеры того, что можно встретить в документации.

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

Да ну.

Ну вот когда предметная область ребует корректности

Как-то ты всё на корректность съезжаешь, формализация != корректность. Написал EBNF для внутреннего язычка — вот формализация, или обратный разбор — регулярки, LALR, никаких корректностей. Или представил кусок программы как FSM или КА и формального его описал — опять. Или если предметная область требует кластеризации данных, например (формализации во все поля). То есть к этому уже можно (но реедко) применять model cheching какой-нибудь, но модель самоценна — просто так, конвенции, представление (в дополнение к естественному языку).

теперь вы пишете программу два раза

На самом деле не два, а один на си и дописываем то что нельзя написать в типах си на ACSL и проверяем соответствие одного другому на Coq (etc., а ещё там есть автоматические semidecidable чекеры).

«Сиплюсплюсик» удобен прежде всего шаблонами. В C есть решение на препроцессоре, но с такими костылями в приличный проект я бы не сунулся, да и кто пустит.

Это ж вещи одного порядка

Нет, не одного.

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

И чем это плохо?

Главное, что оно там есть.

Где есть? Что есть?

Квантификация в типах? Ну пусть есть, и дальше что? Это не повод делать из языка говно и добавлять к нему зависимые типы, потому что там и кроме зависимых типов еще МНОГО ЧЕГО ЕСТЬ.

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

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

Внезапно — http://frama-c.com/what_is.html

Прекрасная иллюстрация моего тезиса- вметсо того, чтобы по-честному сказать «пишите код дважды, блжад!» - куча витиеватых слов :)

Единицы — на языках со статической типизацией

Ты читать разучился?

Есть, но не всё и не правильно

Тут не бывает «не все и неправильно». Либо зависимые типы есть (все и правильно), либо их нету (никак нету).

(то есть нужно следить за вещами как тому школьнику в совершенстве владеющему FOL)

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

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

На самом деле не два, а один на си и дописываем то что нельзя написать в типах си на ACSL и проверяем соответствие одного другому на Coq (etc., а ещё там есть автоматические semidecidable чекеры).

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

Чем менее точно указаны типы - тем меньше дублирования, ну и в результате raid 1 получается неполный - то есть в любом месте, где тип не покрыл, спеки может быть ошибка.

Это первые попавшиеся примеры того, что можно встретить в документации.

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

Как-то ты всё на корректность съезжаешь, формализация != корректность.

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

Написал EBNF для внутреннего язычка — вот формализация, или обратный разбор — регулярки, LALR, никаких корректностей.

Это запись в формальной нотации, а не формализация. Это два _существенно_ разных понятия, не надо их путать. EBNF не является объектом сама по себе, а формализация - является.

но модель самоценна

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

Нормальных ЯП общего назначения с зависимыми типами вообще нет

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

А так я не знаю о каких проблемах ты говоришь.

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

Нет, не одного.

Normed division algebra — четыре штуки (класса), разного порядка (order). Но ты же понимаешь, о чём я говорю?

И чем это плохо?

Это не плохо, но можно лучше.

Где есть? Что есть?

All и Some у Аристотеля.

В итоге все сводится к доказательству школьника.

Ну agda-stdlib — ~26KLOC, categories — ~13KLOC, equality — ~16KLOC. Теперь разработки школьников в студию :)

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

Всё относительно же. Школьнику может и сложно.

пишите код дважды, блжад!

ооп и функциональщина кратко, внятно. (комментарий)

Ты читать разучился?

Вот:

Есть, но не всё и не правильно

Тут не бывает «не все и неправильно».

С++ — есть элементы зависимых типов и всё тут. Если у меня тип параметризирован, то он таков, если он индексирован термами — аналогично, если тип аргумента _зависит_ от терма в шаблоне то у меня, натурально, pi-type, если я делаю fin-type через такое-то место, то опять — у меня fin-type. Если я делаю identity-type... Ну и т.д. http://en.cppreference.com/w/cpp/header/type_traits, http://www.boost.org/doc/libs/1_54_0/libs/mpl/doc/index.html.

тебе тоже надо будет за всем следить руками

«следить за вещами» в С++ это значит не ломать систему типов, то есть не натыкаться на противоречия и неправильности. Как и в хаскеле (http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.pdf). А правильность и (конструктивная? идеологическая?) непротиворечивость избавляет от необходимости следить за вещами таким образом (типа как статическая система типов позволяет не путать вещи, хотя, опять же, в границах отсутствия небезопасных операций вроде кастов).

Мы обсуждали формализацию в контексте зависимых типов

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

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

И это тоже.

И только если модель дает какие-то конкретные профиты ... она имеет право на существование

Пожалуй. Но ты, например, не видишь профитов от статической типизации. Или от теории доменов. Или от зависимых типов. Или от статического анализа и абстрактной интерпретации (?). Так что возможны разночтения. Я говорю, очевидно, о формализациях (и формальных нотациях!) и моделях которые нашли полезными те кто их придумал / применил готовые.

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

Ты тут смешиваешь Frama-C и зависимые типы, они никак явно не связаны. http://toccata.lri.fr/gallery/InsertionSortACSL.en.html (The proof is automatic with any SMT solver) и http://toccata.lri.fr/gallery/MyCosineACSL.en.html (Verification conditions are proved by a combination of automated provers (SMT solvers and Gappa and the Coq proof assistant) — для примера. Во втором случае используется Coq для доказательства одной леммы, первый разрешается автоматически. Где тут двойная реализация? Оно вообще ортогонально — написали код (синтаксис основного ЯП), вытащили его модель (полнота и правильность, желательно), добавили свойств (синтаксис для свойств, ACSL там), проводим их проверку, то есть свойств над моделью, автоматически или руками в чём угодно (зависимые там типы, или HOL).

Представь себе - у нас есть десяток библиотек, в каждой - определяется какая-то коллекция и функции для работы с ней, при этом любая коллекция может быть отсортирована.

Но зачем?

Вообще что-то странное говоришь — в примитивных случаях голая коллекция и её свойства распадаются (в dependent pattern matching) как элементы кортежа, свойство можно выкинуть и спокойно использовать голую коллекцию, верифицуруемая по части свойств функция просто добавляет свойств в свой аргумент (типа sort : Seq -> SeqSorted), причём их можно потаскать и потом стереть при компиляции. А сложные свойства требуют модификации самих типов контейнеров (как в GADTs) для облегчения доказательств свойств функций, но всё тоже волне стирается.

Для примера — безопасная индексация к std::array<T, n> x, то есть гарантия при size_t i; x[i]; что i < n может делаться как operator[](size_t i){i < n} что заставит везде проверять if (i < n) в dependent-if для неявной передачи свойства в operator[], такое свойство легко стирается при компиляции после проверки.

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

Какой код? Всё равно не знаю о каких проблемах ты говоришь :)

Можешь доказать что std::copy (<algorithm>) для упорядоченного итератора даст упорядоченный итератор, std::vector со свойством sorted превратится в std::list, свойство (итератора, а значит и контейнера) сохранится.

Но ты же понимаешь, о чём я говорю?

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

но можно лучше.

Чем лучше? А может хуже?

All и Some у Аристотеля.

Есть (возможно, ограниченно - силлогизмы ведь строятся по определенным правилам), ну и что?

Теперь разработки школьников в студию :)

А «школьники» спокойно пишут софт для атомных реакторов и не парятся вашими агдами :)

ооп и функциональщина кратко, внятно. (комментарий)

См. ниже

Вот:

Что «вот:»?

С++ — есть элементы зависимых типов и всё тут.

Ну охуеть теперь. Для начала ввиди свою собственную систему типов, назови ее «моя система типов имени quasimoto с элементами зависимых типов» и потом после выхода десятка пейперов на тему будем говорить про элементы зависимых типов. А пока что я в душе неебу, что это такое - «элементы зависимых типов». Для одного оно элементы, для другого - не элементы, очевидно же. Давай без этой субъективщины.

Если у меня тип параметризирован, то он таков, если он индексирован термами — аналогично, если тип аргумента _зависит_ от терма в шаблоне то у меня

То у тебя, блять, как и в любой макросистеме. Которая берет, блять, терм, и делает из него кусок программы. И если этот кусок программы - тип, то получается, блять, отображение из термов в типы. И теперь, охуеть, лябая схема имеет зависимые типы. Не, блять, «элементы зависимых типов», вот!

«следить за вещами» в С++ это значит не ломать систему типов, то есть не натыкаться на противоречия и неправильности.

При чем тут вообще с++? Берешь и пишешь доказательство в прувере FOL, который проверяет, чего ты там надоказывал. Для любого языка, вообще.

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

Я прекрасно объяснил, почему, и даже это математически доказал. А потом на зависимые типы перешли. Или ты о них не говорил?

И это тоже.

Ну вот для реализации этой функции она нахуй не нужна, как выясняется. Прувер в руки - и иди спокойно доказывай себе, безо всяких формализаций.

Но ты, например, не видишь профитов от статической типизации.

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

Или от теории доменов. Или от зависимых типов.

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

Я говорю, очевидно, о формализациях (и формальных нотациях!) и моделях которые нашли полезными те кто их придумал

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

Ты тут смешиваешь Frama-C и зависимые типы, они никак явно не связаны.

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

Кстати, вот твоя Frama-c - как раз обычный кондовый FOL, и никаких формализаций с агдами, теоркатами и зависимыми типами не требуется.

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

Но зачем?

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

Вообще что-то странное говоришь — в примитивных случаях голая коллекция и её свойства

Это вообще просто пример общей ситуации, которая будет встречаться повсеместно (семантически совпадающие, но не эквивалентные типы/предикаты).

как элементы кортежа, свойство можно выкинуть и спокойно использовать голую коллекцию

У нас функции требуют отсортированных коллекций, но, вот беда, в каждой библиотеки предикаты сортировки свои. По-этому ты не уберешь сортировку, она нужна. Но тебе всякий раз придется доказывать эквивалентность предикатов.

верифицуруемая по части свойств функция просто добавляет свойств в свой аргумент (типа sort : Seq -> SeqSorted)

И для каждой библиотеки у тебя будет своя руками передоказанная SeqSorted. Круто, чо.

Можешь доказать что std::copy (<algorithm>) для упорядоченного итератора даст упорядоченный итератор, std::vector со свойством sorted превратится в std::list, свойство (итератора, а значит и контейнера) сохранится.

Да у тебя нет никакого такого в зависимых типах «упорядоченного итератора». У тебя есть какое-то свойство, которое ты так обозвал. А у другого человека в его библиотеке то же самое свойство есть, но обозвано по-другому. А хотя может и также - но это же тебе ничего не дает, ведь откуда ты знаешь, можешь он так же другое свойство обозвал?

И чтобы можно было считать это свойство одним и тем же, надо доказать эквивалентность. В реальной жизни у тебя таких свойств, эквивалентность которых надо доказывать, будет пиздец как дохуя, причем они будут не такими тривиальными, как «отсортированный итератор». С итератором-то прувер и автоматом сможет справиться, скорее всего (да и вообще там определение вполне может сопадать).

Размерность чтоли?

Да.

И до этого ты говорил, что они одного порядка.

man разговорная речь. http://en.wikipedia.org/wiki/Hurwitz's_theorem_(normed_division_algebras).

ну и что?

И ничего. Выяснили возраст квантификации.

А пока что я в душе неебу

Так это твои проблемы.

как и в любой макросистеме

Нет. Проведи ревизию — почитай TAPL/ATTAPL, посмотри на обычные шаблонные функции и структуры в нынешнем C++, прикинь. Это статическая система типов с параметризацией (по type) и индексацией (по term) функций и структур в шаблонах, с type -> type, type -> term, term -> type в type-level, с возможностью зависимости параметризированных и индексированных конструкторов типов от типов и значений которыми параметрезированны и индексированы функции и структур в шаблонах (то есть связываем имена template <... тут ...> ...(и используем их аргументами конструкторов типов тут вот так: C<... тут имена ...>)).

При чем тут вообще с++?

Ну ты держи в памяти нить обсуждения.

и даже это математически доказал.

O_o у себя там?

А потом на зависимые типы перешли. Или ты о них не говорил?

ооп и функциональщина кратко, внятно. (комментарий)

которые найдут нужными кроме автора еще сотня/другая упоротых

EBNF с FSM-то?

Кстати, вот твоя Frama-c - как раз обычный кондовый FOL, и никаких формализаций с агдами, теоркатами и зависимыми типами не требуется.

Ну и отлично.

Да у тебя нет никакого такого в зависимых типах «упорядоченного итератора». У тебя есть какое-то свойство, которое ты так обозвал. А у другого человека в его библиотеке то же самое свойство есть, но обозвано по-другому.

Я думаю, если библиотеки никак не связанные и свойства их никак не связанны (не абстрактно а в реализации), то какой-то магии ожидать глупо. Если взять обобщённые интерфейсы и алгоритмы (http://www.cplusplus.com/reference/iterator/, http://www.cplusplus.com/reference/algorithm/), то их свойства можно уже будет распостранять на пользователей (кстати, у Степанова есть книжка EoP в которой изучаются разные свойства — так и формулируются и доказываются в виде теорем). Ну и как бы — никто ж не заставляет всё это делать, зависимые типы не значит => все побежали сортировать свои контейнеры и объявлять sorted, sorted, sorted повсюду, можно извлекать выгоду локально (но ты всё равно при мнении, так что ладно :)).

И для каждой библиотеки у тебя будет своя руками передоказанная SeqSorted.

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

man разговорная речь.

О хоспаде, то ты сперва говоришь «вещи одного порядка» в разговорном смысле (и я так и понял в разговоре), а потом сходу про «разного порядка» в алгебраическом смысле еще и с многозначительным «нутыменяпонел». Хрен тебя поймешь :)

http://en.wikipedia.org/wiki/Hurwitz's_theorem_(normed_division_algebras).

А чего не обобщенная теорема Фробениуса? :)

Так это твои проблемы.

Да нет, то, что я не знаю каких-то твоих собственно придуманных заморочек - это совсем не мои проблемы.

Нет.

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

Проведи ревизию — почитай TAPL/ATTAPL, посмотри на обычные шаблонные функции и структуры в нынешнем C++, прикинь. Это статическая система типов с параметризацией (по type) и индексацией (по term) функций и структур в шаблонах, с type -> type, type -> term, term -> type в type-level, с возможностью зависимости параметризированных и индексированных конструкторов типов от типов и значений которыми параметрезированны и индексированы функции и структур в шаблонах (то есть связываем имена template <... тут ...> ...(и используем их аргументами конструкторов типов тут вот так: C<... тут имена ...>)).

Как и любая макросистема. Просто потому, что, блять, плюсовые шаблоны - это ни что иное, как тривиальная макроподстановка. И чекаются типы, внезапно, уже после макроподстановки. Ты только забыл еще, что term->type для зависимых типов должна быть _тотальной_. Именно это отличает типизацию с зависимыми типами и полиморфными - в случае полиморфизма мы _тоже_ имеем отображение term->type (т.к. любой тип является термом, очевидно), но _нетотальное_. Как и в плюсах. В случае зависимых типов как раз и добавляется условие «любой терм является типом», что делает отображение тотальным.

O_o у себя там?

Зачем у себя? Я о вложении Set_ в CPO.

EBNF с FSM-то?

Ты надоел уже с подменой понятий. При чем тут EBNF с FSM, если речь про зависимые типы и домены? Из того, что EBNF - удобная нотация, никак не следует, что домены - нужная формализация.

Ну и отлично.

Ну так и сразу тогда вопрос - нахрена ж ваши формализации сдались? :)

Если вот ты даже сам пример приводишь, который их не использует.

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

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

то их свойства можно уже будет распостранять на пользователей

Это для «общепринятых» алгоритмов и структур. Ну по сути будет библиотека свойств. Но, очевидно, 99% свойств эта библиотека не покроет. И она только снизит размер пиздеца, причем снизит не качественно.

зависимые типы не значит => все побежали сортировать свои контейнеры и объявлять sorted, sorted, sorted повсюду

Ну так пистаь на языке с зависимыми типами будут же те кому они прям нужны (иначе нахрена брать такой язык?) и потом это просто будет «нормальной практикой». И пиздец неминуем.

Ну ты держи в памяти нить обсуждения.

Я помню, я имел ввиду, что вообще не важно, какой там у тебя язык.

Выяснили возраст квантификации.

ну замечательно, квнатификация была давно. Что из этого следует? Зачем выясняли ее возраст? :)

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

И достаточно выразительным, чтобы задать любую вычислимую функцию.

А чего не обобщенная теорема Фробениуса?

Это которая про ассоциативные? Вообще вот — http://math.ucr.edu/home/baez/octonions/oct.pdf. Хотя я с тем же успехом мог сказать «кватернионы» — всё равно плохое сравнение.

там точно то же самое, что ты описал в плюсах на шаблонах.

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

term->type для зависимых типов должна быть _тотальной_

Ну делаем тотальной и она будет тотальной.

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

Насчёт «моих» заморочек, вот:

http://en.wikipedia.org/wiki/Dependent_type#Systems_of_the_lambda_cube

The system of pure first order dependent types, corresponding to the logical framework LF, is obtained by generalising the function space type of the simply typed lambda calculus to the dependent product type.

Вполне элемент:

// P(a : A). B[a]
template <A a> f(B<a>);

Никто не говорит, что в C++ прям исчисление конструкций на шаблонах.

Это которая про ассоциативные?

Это в обычной, в обобщенной - альтернативные.

http://math.ucr.edu/home/baez/octonions/oct.pdf.

Ааа, Баец. Ну ожидаемо, да. По кому еще может фанатеть категорщик? :)

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

Может и другую. Но что это меняет? Так и шаблоны плюсовые они вообще для эмуляции полиморфизма. Уточняю - для _эмуляции_. Даже полиморфизм у них не настоящий, т.к. макроподстановка. Чего уж говорить о зависимых типах? :)

А на счет развалиться - ну то есть берем обычную типизированную лямбду+макросы тогда. И по-твоему сразу получается CoC.

Ну делаем тотальной и она будет тотальной.

Ну чтобы сделать тотальной то как раз и будут зависимые типы, но в сишке-то нифига не тотальное. Хотя вообще я не слишком верно выразился, тотальным должен быть quote, причем должно быть (quote x ~ quote y) <=> (x ~ y). ну и выразительность системы уже надо допиливать правилами типизации.

Вполне элемент:

Ну и с какого перепугу эта запись невозможна в простой полиморфной лямбде?

Ты надоел уже с подменой понятий.

А я не пойму чем домены-то провинились, то есть чем они хуже всего остального. Кстати, если я сейчас проведу подмену понятий:

Ну так и сразу тогда вопрос - нахрена ж ваши формализации сдались?

Какие «наши»? http://www.lri.fr/~marche/moy09phd.pdf — абстрактные домены и интерпретация. Есть там формализации? Это что стоит за Jessie от Frama-C.

Это для «общепринятых» алгоритмов и структур.

На самом деле — «у меня есть стандартная библиотека, свои плюхи и third-party, мне твои несовместимые эквивалентность-не-доказанные плюхи и свойства на хрен не нужны», никаких проблем :)

И она только снизит размер пиздеца, причем снизит не качественно.

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

А я не пойму чем домены-то провинились

Тем, что они ненужны. Лишняя сущность. Сегодня ты изучаешь домены, а завтра начнешь молиться, поститься и слушать радио радонеж.

Какие «наши»? http://www.lri.fr/~marche/moy09phd.pdf — абстрактные домены и интерпретация. Есть там формализации? Это что стоит за Jessie от Frama-C.

Вот смотрю: http://toccata.lri.fr/gallery/InsertionSortACSL.en.html

И не вижу там никаких абстрактных доменов и интерпретаций. Обычная FOL - есть предикаты, правила вывода, применяем к ним прувер/SMT - получаем результат. Ну все как у того школьника.

На самом деле — «у меня есть стандартная библиотека, свои плюхи и third-party, мне твои несовместимые эквивалентность-не-доказанные плюхи и свойства на хрен не нужны», никаких проблем :)

Писать без библиотек, кроме стандартной? Замечательный подход :)

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

А что странного в том, что из-за изменений возникает северный зверек?

Вот с человеком, допустим, все нормально было, потом дырку в черепе проделали, и северный зверек возник. Удивительно?

И по-твоему сразу получается CoC

Нет же. Ни черта не работает, разваливается и заказывает пицу. Пока ты не напишешь чекер, компилятор, etc. CoC на этих макросах.

Хотя вообще я не слишком верно выразился, тотальным должен быть quote

А quote откуда? Чтобы в C++ делать term -> type нужно делать

template <A> struct MyTermToType;
template <> struct MyTermToType<a> { typedef SomeType result; };
// ...
// until total

// MyTermToType<x>::result

можно рекурсивно — вычислительная стать есть.

Нет же. Ни черта не работает, разваливается и заказывает пицу.

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

А quote откуда?

Ну ниоткуда, просто должен быть. Не обязательно как существующая програмная сущность - просто для терма должно существовать его «представление» на уровне типов.

Чтобы в C++ делать term -> type нужно делать

И чо это? Херня какая-то. В плюсах нельзя сделать term->type просто потому, что в качестве полиморфного аргумента можно подставлять только очень ограниченный набор термов.

Кстати в маакрами поверх типизированной лямбды такой проблемы нет - то есть как раз получается настоящее CoC.

И не вижу там никаких абстрактных доменов и интерпретаций.

А авторы продукта видят.

Писать без библиотек, кроме стандартной?

у меня есть стандартная библиотека, свои плюхи и third-party

Знаешь что такое third-party? Я к тому, что это статическая типизация — если функция принимает std::vector, то всё, она принимает именно его. Если это будет std::sorted_vector то всё так же, никаких other_man::sorted_vector. Можно ещё замутить ООП / интерфейсов, то есть хотеть принимать итератор или SeqI / SortedSeqI, это называется «теория», то есть обобщение интерфейса (набор простых сигнатур) это теория (набор простых сигнатур и сигнатур-свойств с зависимостями на эти обычные, описывающих их свойства), а реализации — модель. В это случае поставляем себе вместо теории в функцию любую её модель — std::sorted_vector или other_man::sorted_vector (и тут вопрос — зачем нам два). Соответственно, все общие свойства теорий для моделей даются for free как только доказано что они модели. В тех клоках кода на агде всё это активно используется (то есть records для теорий, их объекты для моделей).

А что странного в том, что из-за изменений возникает северный зверек?

Ну вот выше пример изменения:

Ну и с какого перепугу эта запись невозможна в простой полиморфной лямбде?

Это как? В Haskell 2010 невозможна.

Или ещё пример изменения — предикаты на числа, то есть борьба со integer overflow и bounds checking статическими регионами. Это потребует продвинуть пример с dependent product до f(A a)<P[a]> и ввести dependent-if, ну и как-то предикаты ввести (вообще, понятно как).

И чо это?

Как type traits (http://www.cantrip.org/traits.html, http://accu.org/index.php/journals/442, http://www.cplusplus.com/reference/type_traits/) только наоборот — можно делать выбор типа по значению.

нельзя сделать term->type

Пример? Чего нельзя? При условии, что значение известно во время компиляции (в рантайме же типов у него нет).

маакрами поверх типизированной лямбды такой проблемы нет - то есть как раз получается настоящее CoC

Вообще кайф :) Ладно, я в маакрасах-двудольных-графах не разбираюсь.

А авторы продукта видят.

Ну пусть видят. Только если человек видит то, чего нет, то надо обратиться к специалисту.

Знаешь что такое third-party? Я к тому, что это статическая типизация — если функция принимает std::vector, то всё, она принимает именно его. Если это будет std::sorted_vector то всё так же, никаких other_man::sorted_vector.

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

Ну вот выше пример изменения:

Где? обычная полиморфная лямбда с ограниченной квантификацией. haskell 98 шире.

Это как? В Haskell 2010 невозможна.

Это с какого перепугу? Даже в haskell 98 возможна. bind у монад, например, использует все то, что в твоем примере. Ничего кроме стандартного полиморфизма ты не показал (это и логично - ведь по определению шаблоны плюсов не могут делать ничего, чего не может полиморфизм).

Или ещё пример изменения — предикаты на числа, то есть борьба со integer overflow и bounds checking статическими регионами.

Ну да, а потом можно посмотреть на тот же код из frama-c где аннотаций больше чем собственно самого кода. И это для тривиальных вещей, заметим.