Архитектура системы верификации кода драйверов Linux

раз его скастовали сюда, наверно можно и второй раз скастовать

а вообще я сомневаюсь, что тут на лоре кроме тебя кто-то из драйверописателей интересуется формальной верификацией

Насколько я понял, это средство не только для драйверописателей.

насколько я понимаю, да

ладно, я прекращаю выступать в роли К.О., интересней почитать, че они там накрутили

я интересуюсь

раз такое дело, сделал опрос: www.linux.org.ru/polls/polls/7001001

[вброс]

Как мне кажется, все эти версификаторы направлены на компенсацию убогости С\С++

[/вброс]

> Как мне кажется, все эти версификаторы направлены на компенсацию убогости С\С++

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

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

хотя, тут, не все так просто

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

> Как мне кажется, все эти версификаторы направлены на компенсацию убогости С\С++

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

> все эти версификаторы направлены на компенсацию убогости

Скомпенсируй свою убогость - научись читать.

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

Внезапно: ходил по ссылкам в теме, почитал их сайт. Они там нечто похожее на юнит-тесты на libc написали. Цирк.

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

Какие? Вызов метода/функции xxx обязательно делать только после вызова метода/функции yyy или метода/функции ййй? :)

>> Все равно такие фичи должны быть встроены в язык.

Какие? Вызов метода/функции xxx обязательно делать только после вызова метода/функции yyy или метода/функции ййй? :)

Почему нет?

> Внезапно: ходил по ссылкам в теме, почитал их сайт. Они там нечто похожее на юнит-тесты на libc написали. Цирк.

Походу, ты не совсем врубаешься. Юнит тесты - это ЧАСТЬ кода, работающая в коде предназначеном для тестирования.

Здесь ВЕСЬ код драйверов прокручивается на поиск противоречий в специальной среде, эти противоречия выявляющей.

>>> Все равно такие фичи должны быть встроены в язык.

Какие? Вызов метода/функции xxx обязательно делать только после вызова метода/функции yyy или метода/функции ййй? :)

Почему нет?

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

Не, мы про спецификации разного уровня говорим. Я вот высмеиваю верификаторы низкоуровневых спецификаций, вроде запрета на выход за границы массива.

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

При чём здесь формальный верификатор? Проверку инварианта на выход за границы массива должен делать компилятор. А если корректность инварианта зависит от среды исполнения, т.е. это нельзя доказать статически, то и рантаймовую проверку выкидывать нельзя.

> Не, мы про спецификации разного уровня говорим. Я вот высмеиваю верификаторы низкоуровневых спецификаций, вроде запрета на выход за границы массива.

В одних языках надо одно проверять. В других - другое. В общем объеме необходимых проверок - это ничего не значащая величина.

> то и рантаймовую проверку выкидывать нельзя.

Вообще-то, если среда не меняется в процессе работы, то можно. Вынести эти проверки на этап инициализации...

>> то и рантаймовую проверку выкидывать нельзя.

Вообще-то, если среда не меняется в процессе работы, то можно. Вынести эти проверки на этап инициализации...

От выноса проверки из цикла быть рантаймовой она не перестанет.

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

>>> то и рантаймовую проверку выкидывать нельзя.

Вообще-то, если среда не меняется в процессе работы, то можно. Вынести эти проверки на этап инициализации...

От выноса проверки из цикла быть рантаймовой она не перестанет.

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

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

Вот внимательность программиста и проверяется.

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

Особенно убедительно выглядит про «внимательного программиста».

При чём здесь формальные верификаторы мне не понятно.

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

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

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

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

Вот внимательность программиста и проверяется.

Вы про что? Кем проверяется? И на каком этапе - статически или в рантайме?

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

Согласен. Более того, этот «верификатор»-компилятор сам стремится исправить код на более оптимальный. Но в такой формулировке верификаторами пользуются все, кто компилирует с ключом -O, отличным от нуля. Речь ведь изначально шла про верификацию во время исполнения кода, а не статическими средствами, не?

> в такой формулировке верификаторами пользуются все, кто компилирует с ключом -O, отличным от нуля

Простым, нерасширяемым верификатором.

Речь ведь изначально шла про верификацию во время исполнения кода

Видимо, я пропустил момент, когда разговор о статической верификации перешел в разговор о динамической (более того, я впервые слышу о «динамической верификации» %)).

>> в такой формулировке верификаторами пользуются все, кто компилирует с ключом -O, отличным от нуля

Простым, нерасширяемым верификатором.

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

> вот насчет нерасширяемости - теперь не верно.

Всё еще верно.

Теперь же можно скрипты на питоне писать для gcc

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

> Видимо, я пропустил момент, когда разговор о статической верификации перешел в разговор о динамической (более того, я впервые слышу о «динамической верификации» %)).

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

Поправьте, что не так.

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

некоторые?

отключать надо не некоторые, а только те, что доказано не нужны

третий раз повторять не буду

> Код драйвера «чистится» от «ядерных» особенностей, инструментируется проверками на блокировки/разблокировки/что ещё они там проверяют

Да.

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

Нет.

Раз код (пусть и модифицированный) запускается

Он не запускается. В статье говорится, что инструментированный текст передается чисто статическим чекерам (собственно, запуск драйверного кода невозможен без устройства). Может, там в роли «запуска» выступает абстрактная интерпретация (это объяснило бы время, затрачиваемое на проверку), но это всё равно не является реальным запуском кода.

>> вот насчет нерасширяемости - теперь не верно.

Всё еще верно.

Почему?

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

> Речь ведь изначально шла про верификацию во время исполнения кода, а не статическими средствами, не?

основной пойнт как раз на статической верификации

и «верификация во время исполнения кода» режет слух

> Он не запускается. В статье говорится, что инструментированный текст передается чисто статическим чекерам (собственно, запуск драйверного кода невозможен без устройства). Может, там в роли «запуска» выступает абстрактная интерпретация (это объяснило бы время, затрачиваемое на проверку), но это всё равно не является реальным запуском кода.

Ну я и написал, что он вроде как после преобразования в промежуточное представление чистится LDV от взаимодействия с ядром и железом. То есть, получается обычная самодостаточная программка с по-умному понатыканными LDV и BLAST-ом ассёртами, принимающая в качестве аргумента снова же абстрагированную последовательность событий/состояний железа/mutexов/переменных/итд, на которой вполне реально прогоняется. И так на всех последовательностях, которые LDV/BLAST считают достаточными для заключения о корректности работы. Собственно, я это и писал:

инструментированный драйвер (т.е. уже по сути дела не драйвер, а инструментированный чекер с идентичной структурой кода) запускается на всех этих тестах

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

> запуск «выпотрошенного»

Еще раз - там нет запуска.

> Может, там в роли «запуска» выступает абстрактная интерпретация (это объяснило бы время, затрачиваемое на проверку)

бласт в качестве результата может выдать:

1. инвариант доказан

2. инваринат нарушается вот в таком execution path

3. работаю... вот такие-то execution path вроде бы дают нарушение инварианта, но х.з.

в п.3 он может работать бесконечно

> проверки определяются не во входном языке, который воспринимается компилятором, а в чекере

Что понимается под чекером? Если проверки на возможность проведения каких-то оптимизаций (о чём разговор шёл изначально, если я ещё правильно это помню), это делается в миддл-энде. Согласно http://gcc.gnu.org/onlinedocs/gccint/Plugins.html я понял, плагины в миддл-энд вставлять можно, т.е. как раз можно иметь возможность щупать внутреннее представление и делать на основании этого какие-то заключения. Правда, на C, насчёт Питона не знаю.

> Что понимается под чекером? Если проверки на возможность проведения каких-то оптимизаций (о чём разговор шёл изначально, если я ещё правильно это помню), это делается в миддл-энде

*тебе* наверно легче всего забыть про то, что я сказал про оптимизации — тогда будет понятнее

рассмотри просто проверку правильности программы

> Что понимается под чекером?

Код, проверяющий свойства программы.

> Все равно такие фичи должны быть встроены в язык.

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

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

ну и наличие в компиляторе SMT-решателя тоже немного необычно

> но это всё равно не является реальным запуском кода.

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

> Еще раз - там нет запуска.

Открываем статью с их сайта (http://www.sosy-lab.org/~dbeyer/Publications/2007-STTT.The_Software_Model_Che...), смотрим рис. 12. Анализатор Blasta анализирует код и выплёвывает набор входных векторов, которых по его мнению должно быть достаточно для вынесения вердикта о корректности программы. Затем эти вектора скармливаются изначальному коду, и происходит тестирование. В каком виде происходит тестирование методом прогона всех сгенерированных входов на исходной программе - на уровне абстрактного дерева или в бинарном виде - там я не нашёл, но нашёл это в статьего одного из (видимо) разработчиков http://goto.ucsd.edu/~rjhala/papers/jhala-thesis.pdf

The test-driver generator takes as input the original program and instruments it at the source-code level to create a test driver containing the following components: (1) a wrapping function, (2) a test-feeding function, and (3) a modied version of the original program. The test driver can then be compiled and run to examine the behavior of the original program on the test suite. It can be run on each individual test vector and the user can study the resulting dynamic behavior as she pleases, by using a debugger for example.

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

Где ошибаюсь?

> абстрактному дереву

абстрактному представлению

> Анализатор Blasta анализирует код и выплёвывает набор входных векторов

Да, BLAST умеет генерировать тесты. Что дальше?

Где ошибаюсь?

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

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

В настоящее время для целей тестирования и демонстрации возможностей

реализованы 2 обертки соответственно для верификаторов достижимости BLAST и CPAchecker.

То есть, если из LDV зовётся BLAST, то бласт релевантен. Если бласт релевантен, то моё предыдущее сообщение о том, что Blast «внутри себя» всё-таки (по крайней мере, согласно приведённой мной статье) исполняет бинарное представление кода (пусть и модифицированного) драйвера, также релевантно и доказывает правоту утверждения, что код в конечном счёте (внимание!) всё-таки исполняется. А в самой статье вообще мало чего говорится о внутренней структуре реализованной системы, там только общие слова.

говориться

говорится

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

> Если бласт релевантен, то моё предыдущее сообщение о том, что Blast «внутри себя» всё-таки (по крайней мере, согласно приведённой мной статье) исполняет бинарное представление кода (пусть и модифицированного) драйвера, также релевантно

О как. Может, еще скажешь, как именно BLAST умудряется исполнять бинарный код драйвера устройства, не имея под собой устройства? %)

> О как. Может, еще скажешь, как именно BLAST умудряется исполнять бинарный код драйвера устройства, не имея под собой устройства? %)

Уже несколько раз сказал - исполнение _модифицированного_ кода в _модифицированном_ окружении. Уже без обращений к самому устройству. Да, и если ты до сих пор думаешь, что проверяется интерфейс доступа к самому физическому устройству - посмотри на список найденных с помощью тула багов и проверки, описанные в статье - там идёт исключительно работа с памятью, mutex-ы, проверки на несрабатывание assert-ов. То есть, чисто программные вещи. То, что драйвер это или нет - уже мало принципиально. Главная сложность - то, как очистить код от системной «шелухи».

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

> и если ты до сих пор думаешь, что проверяется интерфейс доступа к самому физическому устройству

Я так не думаю сейчас и не думал раньше.

А вообще посты ты не читаешь, позицию не аргументируешь,

Я внимательно читал твои посты и объяснял свою позицию, пока не понял, что столкнулся с уверенным в себе профаном.

пишешь мусор

Хотел сказать, что мусор у тебя в голове, но там пусто. Даже мусора нет.

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

Что должен сделать язык со входными данными выходящими за диапазон? И устроит ли тебя его решение.

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

>Язык должен предоставить возможность написать пред-условие, ну и гарантировать его выполнение.

Так уже есть давно, но не в питоне с жабой. Комбинация операторов if then begin end goto творит чудеса логики и обрабатывает любое количество условий и просто в коде и во вложенных циклах.

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

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

>> Комбинация операторов if then begin end goto творит чудеса логики и обрабатывает любое количество условий

Ну я это юзаю как могу

Херасе.

Не ну не конкретно с goto, но да, предусловия очень часто пишу.

A 3.6 Rule Instrumentor (LLVM)?

> A 3.6 Rule Instrumentor (LLVM)?

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

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

Runtime верификацией всё же называют подходы, когда целевой (или анализируемый) код исполняется на процессоре, возможно, виртуальном. Абстрактную интерпретацию обычно относят к методам статического анализа. В BLAST и CPAchecker же основную роль играют методы анализа моделей (model checking) на основе автоматического инкрементального уточнения моделей, а абстрактная интерпретация используется для решения вспомогательных задач.

Кстати, у нас в Центре верификации ведутся работы как по статическому анализу модулей ядра, так и по динамическому. Недавно мы опубликовали слайды с LinuxCon Europe 2011 по этим проектам: http://linuxtesting.ru/linuxcon2011

«Для выполнения всего процесса инструментирования в целом в настоящее время используется набор инструментов LLVM [27]. Непосредственно для препроцессирования, разбора файлов с исходным кодом и одновременно выполняемого инструментирования на основе аспектных файлов используется LLVM GCC Front End, ввиду того, что GCC является основным для сборки ядра под ОС Linux.»

Что на это скажете?

> Что на это скажете?

Я скажу, что если ты не веришь Хорошилову, то мне и подавно не поверишь %)

Это и была его цитата.

Дело тут не в вере - просто хочется понять как работает эта штука.

>> если ты не веришь Хорошилову, то мне и подавно не поверишь %)

Это и была его цитата.

Архитектура системы верификации кода драйверов Linux (комментарий)

Runtime верификацией всё же называют подходы, когда целевой (или анализируемый) код исполняется на процессоре, возможно, виртуальном. Абстрактную интерпретацию обычно относят к методам статического анализа. В BLAST и CPAchecker же основную роль играют методы анализа моделей (model checking) на основе автоматического инкрементального уточнения моделей, а абстрактная интерпретация используется для решения вспомогательных задач.

просто хочется понять как работает эта штука.

Именно «эта штука» принципиально не сложная (хотя и большая), а для понимания BLAST и прочего лучше читать первоисточники.

Как мне кажется, все эти версификаторы направлены на компенсацию убогости С\С++

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

Да, но в языках с зависимыми типами такого рода проверки by design будут в compile time (в системе типов). Так что в этой фразе про убогость (бедность) С и С++ есть доля истины - взять тот же cyclone (там не зависимые, а субструктурные типы) где типы решают часть проблем которые в С решаются только внешним статическим анализом.

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

я не думаю, что «зависимые типы требуют слишком большого внимания к себе»; кстати — субструктурные это про что?

насчет костылей — все сложно

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

if (!(card2 = icn_initcard(port, id2))) {
        printk(KERN_INFO
               "icn: (%s) half ICN-4B, port 0x%x added\n",
               card2->interface.id, port);
        return 0;
}

с другой — возможно, что костыли это как раз паттерн матчинг

рассмотрим мой пример:

int f(int* a, int* b, int* c, int* d)
{
  int x = g();

  switch( !!a + !!b + !!c + !!d ) {
    case 0: return x;
    case 1: return f1(x, a, b, c, d);
    case 2: return f2(x, a, b, c, d);
    case 3: return f3(x, a, b, c, d);
    case 4: return x + *a + *b + *c + *d;
  }
}

имеем простой и ясный код (f1, f2 и f3 могут принимать нулевые указатели), а теперь во что это выльется с паттерн матчингом? в спагетти из 16 вариантов, я так понимаю

не знаю, может ли бласт верифицировать такое, но если не может, то думаю не трудно его доделать

примерно такую мысль высказывал tailgunner, хотя пример для иллюстрации я придумал сам

я кстати тогда с ним резко не согласился

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

Ну, если выбирать их как дисциплину программирования, то да. Если человек берёт agda/coq/twelf, он, видимо, знает чего хочет. Просто иногда, бывает, человек берёт haskell и начинает недоумевать по поводу всей этой капризности компилятора по отношению к типам.

кстати — субструктурные это про что?

Это линейные (linear) и упорядоченные (ordered). И те и другие - сужение unrestricted системы типов (unrestricted <- (affine, relevant) <- linear <- ordered, такое вложение). Первые подходят для рассуждений (система типов = логика) о выделении и освобождении объектов в куче (например, линейным программам не нужны ни ручное управление памятью, ни GC), вторые - на стеке. В первой главе ATTAPL об этом есть.

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

icn_initcard возвращает указатель на структуру, этот указатель присваивается card2, и если этот указатель не NULL, то пишем что-то? Ну в типах это будет:

Maybe   : forall (a : Type). a -> Type
nothing : forall (a : Type). Maybe a
just    : forall (a : Type). a -> Maybe a

и код будет писаться как-то так:

card <- initcard port id
case card of
  nothing -> do printk ...
                return ...
  just x  -> do ...

Либо, если нужны именно плоская память (или куча) и указатели, то они должны быть представлены в алгебраических зависимых типах тоже (как inductive families), тогда логика работы с памятью, арифметика указателей и тому подобные вещи будет частью системы типов (на эту тему можно посмотреть публикации Wouter Swierstra). Вообще, все типы должны быть алгебраическими, если хочется тотальности.

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

Структурные типы (типы произведения) представляются в памяти так же как и сишные struct, а вариантные типы (типы суммы) - как сишные union с тайптегом (без тайптега делать case, который в рантайме, проблематично, case времени компиляции это на тему generic интерфейсов в духе классов типов хаскеля, но это работает только для выводимых типов, фишка вариантных типов в том, что вариант становится известен только в рантайме, это, фактически, динамическая диспетчеризация). Паттерн-матчинг (nested pattern matching) это сахар для (компилируется в) case, который сахар для набора примитивов case_n и get_m (n, m = 1, 2, ...), при этом примитивы case_n работают точно также как сишный switch по тайптегу, а get_m точно также как сишный struct->field.

Как бы, какая разница, делаем мы if (!ptr) ... или case ... of nothing/just...

рассмотрим мой пример

может ли бласт верифицировать такое

Не совсем понял этот пример (что мы тут верифицируем?). Но в свете того что код ADT и PM переписывается механически в код со структурами, объединениями и switch (и обратно), это не важно. Т.е. паттерн-матчинг это не та фишка из систем типов (это, вообще говоря, и не фишка систем типов) которую нужно рассматривать при разговоре о системах типах как средстве верификации.

Я имел ввиду прежде всего, что та логика которую пытаются привязать к программам внешние верификаторы имеется из коробки в мощных системах типов (не будем забывать про изоморфизм Карри-Говарда) - субструктурных типов достаточно для доказательств того, что программа не портит память, зависимые типы могут выводить длинны используемых массивов и, тем самым, не давать индексам выскочить за их границы (если только это не случайный индекс, но он не может быть случайным, по крайней мере вне IO), типы Хоара могут использоваться для рассуждений об I/O, типы пи-исчесления - для рассуждений о процессах и сообщениях ну и т.п.

рассмотрим мой пример

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

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, TypeSynonymInstances #-}

import Data.Word

-- -----------------------------------------------------------------------------
-- * Primitive types.

-- | Natural numbers.
type N = Integer -- KLUDGE: haskell has no algebraic integers.

-- | Boolean numbers.
type B = Bool

-- | Machine word.
type W = Word -- ui32 or ui64. KLUDGE: not an algebraic type.

-- -----------------------------------------------------------------------------
-- * sizeOf and maxOf.

-- | The size of objects in a flat memory.
class SizeOf t where
  -- | Object size in bytes. Compile-time method.
  sizeOf :: t -> W
  -- | Use it for pointers and fixnums.
  maxOf  :: t -> N
  maxOf x = floor $ 2 ^^ (sizeOf x * 8) - 1

instance SizeOf W where
  sizeOf _ = 4 -- When configured for x86.

-- | The @Word@ type itself, use it in type-level.
word = undefined :: W

-- -----------------------------------------------------------------------------
-- * Pointers in a flat memory.

-- wtf? where is my segments and paging? ;-)

-- | Bad or good pointer.
data Ptr = Null | Ptr N -- isomorphic to (Maybe N)
  -- deriving ( Show, Read, Eq, Ord, Enum, Num, Functor, Applicative, Monad, Binary, etc. )

-- | Pointer arithmetic.
class PtrArith t where
  -- | The sum of two pointers.
  (+.) :: t -> t -> t
  -- | Etc.
  -- ...

instance PtrArith Ptr where
  Null  +. Null  = Null
  Null  +. Ptr y = Ptr y
  Ptr x +. Null  = Ptr x
  Ptr x +. Ptr y
    | x + y < maxOf word = Ptr $ x + y
    | otherwise          = Null

-- -----------------------------------------------------------------------------
-- * Casting.

-- | A casting functor (yeah, really functor).
class Cast a b | a -> b where
  -- | Cast type @a@ to type @b@ when it makes sense.
  cast :: a -> b

-- Forgetful functor.
instance Cast Ptr B where
  cast Null    = False
  cast (Ptr _) = True

-- Just a functor.
instance Cast B W where
  cast False = 0
  cast True  = 1

-- W to B? Yes, if W is an algebraic type.

Тогда этот код так и будет выглядеть:

argh :: Ptr -> W
argh = (cast :: B -> W) . (cast :: Ptr -> B)

test a b c d =
  let x = Ptr 777 in
  case argh a + argh b + argh c + argh d of
    0 -> x
    1 -> x -- f1 ...
    2 -> x -- f2 ...
    3 -> x -- f3 ...
    4 -> x +. a +. b +. c +. d

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

> switch( !!a + !!b + !!c + !!d ) {

имеем простой и ясный код (f1, f2 и f3 могут принимать нулевые указатели)

Вот лично я не понял, что проверяет эта «простая и ясная» проверка.

Чего вы прицепились к проверке указателя на NULL? Это банальщина. Изобразите хотя бы проверку захвата мютекса (пример есть в статье); изобразите запрет использования kmalloc(*, GFP_KERNEL) из прерывания; выразите условие «при доступе к переменной p->x необходимо захватить спинлок p->y» - короче, что-нибудь менее банальное, но полезное на практике.

Чего вы прицепились к проверке указателя на NULL?

Там не NULL, там !!a + !!b + !!c + !!d. Т.е. ptr -(неявно)-> int -(неявно)-> bool -(logical not)-> bool -(logical not)-> bool -(неявно)-> int (что редуцируется в явные ptr -> bool -> int). Итого, в зависимости от того сколько NULL-pointer-ов среди a, b, c, d, - делаем разные действия.

что-нибудь менее банальное, но полезное на практике.

На код-базе дефолт-ядра? Это никак нельзя (нет, ну можно, конечно, как в сабже).

Как пример верификации чего-то более полезного на практике с использование теории типов можно привести верификацию STM. И как реализацию - монаду STM из GHC с compile-time гарантией атомичности и изолированности транзакций.

запрет использования kmalloc(*, GFP_KERNEL) из прерывания

Вот как раз, два параметрических типа IO и STM с линейными монадическими интерфейсами не могут смешиваться (нельзя делать IO в STM и тем самым разрушить гарантии STM), и этот запрет - следствие правил типизации (довольно простых, причём). Это, конечно, так потому что об этом подумали и сделали именно так - потому что система типов позволяет так делать. У си не позволяет, по чисто историческим причинам (теоретически, нет причин по которым си не мог бы быть безопасным и иметь мощные типы).

> Чего вы прицепились к проверке указателя на NULL? Это банальщина.

потому и прицепился, что это банальщина, епрст! разве не понятно?!

*даже* для этой банальщины выдумывают паттерн матчинг и специальный синтаксис для него

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

Изобразите

кое-что я могу изобразить с помощью зависимых типов, а вот насчет запрета kmalloc(*, GFP_KERNEL) надо подумать

>> switch( !!a + !!b + !!c + !!d )

Вот лично я не понял, что проверяет эта «простая и ясная» проверка.

код *считает* количество ненулевых указателей среди a b c d, и в зависимости от этого выполняет одну из веток свича

корректность/проверка этого кода состоит в том, что

1. в любой ветке не разыменовываются нулевые указатели

2. при всех вариантах нулевых и не-нулевых указателей функция таки возвратит целое (т.е. все варианты рассмотрены)

ыыы! твои простыни невозможно читать

у меня конкретный вопрос: можно ли как-то сделать, чтобы в паттерн-матчинге было не 16 веток, а 5 как у меня?

но я все же почитаю и выскажусь

у меня конкретный вопрос: можно ли как-то сделать, чтобы в паттерн-матчинге было не 16 веток, а 5 как у меня?

Во-первых, да. Смотри пост, там где test a b c d = ... Похоже на сишный же код? Во-вторых, и тут простыня про паттерн-матчинг и его незначительную роль, а ну я об этом писал уже :)

*даже* для этой банальщины выдумывают паттерн матчинг и специальный синтаксис для него

а что будет, если продолжить *этот* подход дальше?

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

Я тут подумал, что это за эмоция у меня возникает глядя на такое непонимание со стороны людей, которые, вроде бы, любят и статические системы типов и верификацию времени компиляции? Не иначе как facepalm :)

Не совсем понял этот пример (что мы тут верифицируем?).

1. в любой ветке не разыменовываются нулевые указатели

2. при всех вариантах нулевых и не-нулевых указателей функция таки возвратит целое (т.е. все варианты рассмотрены)

и еще желательно

3. тут нет unreachable code

в качестве аналога, видимо, предлагается намного более простая вещь чем у тебя — пусть у нас вместо возможно-нулевых-указателей есть объекты класс Option[int] (если мы рассматриваем скалу) или MayBe Int (если хаскель)

задача: у нас есть 4 объекта АлгТД MayBe Int

нам надо сделать разные действия в зависимости от количества среди них Nothing (или Just, не важно)

при этом 1, 2, 3 должно проверяться компилятором

допустим, что is_just проверяет на то, что у нас Just, и выдает целое 0 или целое 1

тогда написать

case is_just(a) + is_just(b) + is_just(c) + is_just(d) of
    0 -> x
    1 -> x -- f1 ...
    2 -> x -- f2 ...
    3 -> x -- f3 ...
    4 -> x +. a +. b +. c +. d

мы, как я понимаю, не можем, т.к. x +. a +. b +. c +. d будет типа MayBe Int, так?

з.ы. если бы у нас были шаблоны в хаскеле, то is_just мог бы выдавть MySuperBoolean<1>, дальше сумма объектов MySuperBoolean<3> и MySuperBoolean<1> имела бы тип MySuperBoolean<3+1>, и мы бы поимели полноту матчинга — но заданный чуть выше вопрос это не снимает

> Не иначе как facepalm :)

не все так просто

> Не иначе как facepalm :)

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

s/MayBe/Maybe/

надеюсь, все равно всем понятно

1. в любой ветке не разыменовываются нулевые указатели

Указатели как maybe-подобный тип + тотальные функции = нулевые указатели никогда не разыменовываются.

2. при всех вариантах нулевых и не-нулевых указателей функция таки возвратит целое (т.е. все варианты рассмотрены)

И GHC и agda умеют выводить тотальность. GHC кидает ворнинги (при -Wall), а agda вообще запрещает частичные функции.

3. тут нет unreachable code

В аппликативном программировании нет unreachable code как класса.

предлагается намного более простая вещь чем у тебя ... MayBe Int

У меня как раз это (там есть комментарий про изоморфизм с Maybe Integer, лишняя специфичность тут не помешает).

тогда написать

Лучше так:

countNull :: [Ptr] -> W
countNull = sum . map fn
  where
    fn :: Ptr -> W
    fn = (cast :: B -> W) . (cast :: Ptr -> B)

test a b c d =
  let x = Ptr 777 in
  case countNull [a, b, c, d] of
    0 -> x
    1 -> x
    2 -> x
    3 -> x
    4 -> x +. a +. b +. c +. d

мы, как я понимаю, не можем, т.к. x +. a +. b +. c +. d будет типа MayBe Int, так?

Как я это написал - определил операцию (+.) для типа Ptr. Но не очень думал - какова семантика bad_pointer + (good_pointer x)?

А вообще, смысл конструкции (a + b), где a и b - указатели на int в студию. Я понимаю там сдвиг указателя данное количество байт вверх/вниз, но это.

-- | Pointer arithmetic.
class PtrArith t where
  -- | Shift of a pointer.
  (+.) :: t -> N -> t
  -- | Etc.
  -- ...

instance PtrArith Ptr where
  Null  +. _ = Null
  Ptr x +. y
    | x + y < maxOf word = Ptr $ x + y
    | otherwise          = Null

если бы у нас были шаблоны в хаскеле

Зачем в хаскеле шаблоны? Параметрический полиморфизм, ad-hoc полиморфизм, макросы - всё это покрывается естественными для хаскеля средствами.

как у тебя получается убрать MayBe

Убрать maybe? В смысле. В том коде Prt ~ Maybe Integer.

> Как я это написал - определил операцию (+.) для типа Ptr. Но не очень думал - какова семантика bad_pointer + (good_pointer x)?

это ключевой момент (и не нужно простыней, да)

дело в том, что когда у нас is_just(a) + is_just(b) + is_just(c) + is_just(d) == 4, то тогда *все* они хорошие указатели, и *каждый* из них можно превратить в int — bad_pointer-ов вообще нет

вопрос только в том, как ты это объяснишь компилятору хаскеля

не все так просто

Тут всё весьма просто.

а еще посмотри внимательно — у меня х это не указатель, а целое

В аппликативном программировании нет unreachable code как класса.

бугага

case x*x `mod` 4 of
  0 -> ...
  1 -> ...
  2 -> unreachable code
  3 -> unreachable code

это ключевой момент (и не нужно простыней, да)

Ну так какой ответ на цитируемый вопрос?

Если в сишке можно писать { int *a, *b; a + b } это не значит, что у этого a + b есть нормальная семантика. Я могу себе представить такие хорошие функции:

+ : Prt → ℤ → Ptr   -- shift
- : Ptr → Ptr → ℤ   -- offset

и всё.

дело в том, что когда у нас is_just(a) + is_just(b) + is_just(c) + is_just(d) == 4 то тогда *все* они хорошие указатели

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

sum : {n m : ℕ} → Vec Bool n → (m ≤ n)

бугага

Ах в этом смысле.

if (нашёл целые корни уравнения (x^n + y^n = z^n)) {
    ...
} else {
    ...
}

и давай теперь требуй инструмент статического анализа, который отсечёт unreachable code ;)

а еще посмотри внимательно — у меня х это не указатель, а целое

Это я понимаю (shift указателя), но не a + b + c + d. Смысл?

> Ах в этом смысле.

и давай теперь требуй инструмент статического анализа, который отсечёт unreachable code ;)

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

Может пояснишь, какие другие смыслы есть?

Я подумал было на требование от функций быть тотальными. Т.е. покрытие кодом всех вариантов у данного вариантного типа. Ну и невозможность написать код который бы не был аппликацией/абстракцией/локальной специальной формой.

> Я подумал было на требование от функций быть тотальными. Т.е. покрытие кодом всех вариантов у данного вариантного типа. Ну и невозможность написать код который бы не был аппликацией/абстракцией/локальной специальной формой.

Т.е. покрытие кодом всех вариантов у данного вариантного типа.

Опиши, что ты имел ввиду, на примере функции «const» в прелюдии хаскеля

Что я имел ввиду не имеет отношения к unreachable code, т.е. = моя тупость, в данном случае.

>> запрет использования kmalloc(*, GFP_KERNEL) из прерывания

Вот как раз, два параметрических типа IO и STM с линейными монадическими интерфейсами не могут смешиваться

Ты знаешь много умных слов, браво. Именно поэтому я просил тебя _изобразить_ решения задач, а не сказать «в Хаскелле это как два байта переслать».

У си не позволяет, по чисто историческим причинам (теоретически, нет причин по которым си не мог бы быть безопасным и иметь мощные типы).

Естественно, ты можешь придумать маленькое расширение Си или правило верификации (см. статью).

теоретически, нет причин по которым си не мог бы быть безопасным и иметь мощные типы

*короткая презрительная ругань* Когда уже кто-нибудь из теоретиков спустится с небес и хотя бы попробует сделать юзабельный безопасный Си?

> код *считает* количество ненулевых указателей среди a b c d, и в зависимости от этого выполняет одну из веток свича

Это как раз понятно (и случаи 0 и 4 тоже понятны). Но в 3 из 5 веток нельзя сделать никакого полезного вывода о поступивших аргументах.

Чего вы прицепились к проверке указателя на NULL? Это банальщина.

потому и прицепился, что это банальщина, епрст! разве не понятно?!

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

*даже* для этой банальщины выдумывают паттерн матчинг и специальный синтаксис для него

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

кое-что я могу изобразить с помощью зависимых типов,

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

> Это как раз понятно (и случаи 0 и 4 тоже понятны). Но в 3 из 5 веток нельзя сделать никакого полезного вывода о поступивших аргументах.

пусть нулевые указатели означают отсутствие экспериментальных данных, а ненулевые — их наличие (и само данное)

дальше, в зависимости от количества экспериментальных данных, мы, с должным запасом в сторону надежности, вычисляем *a+*b+*c+*d

например, если известно всего одно из них, скажем с, то надежно (надежно с точки зрения дальнейшего применения) можно считать, что сумма по крайней мере не меньше чем *с/10 + *с/5 + *с + *с/5

и так далее — т.е. каждая из функций f1, f2, f3 это такая приличная портянка с разбором случаев и комментариями, почему мы так решили, поэтому нам желательно сделать одну функцию f (в моем примере), которая будет наглядно отсылать к ним

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

*даже* для этой банальщины выдумывают паттерн матчинг и специальный синтаксис для него

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

1. я там недалеко упомянул про пафос и натяжки

2. «не для этого» — да, и это заставляет меня иметь пока не окончательное мнение

3. АлгТД недалеко ушли от этого узкого частного случая

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

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

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

1. не скатывается — квазимото известен тем, что постит простыни, когда надо задать вопрос, но это терпимо

2. изображать надо на чем-то; в с++ нет зависимых типов, но если (... простынка...) то можно считать, что они есть (компилятор будет это проверять, ... опять длинная простынка ...)

изобразать видимо надо, причем несколькими способами, только я это буду делать медленно и задумчиво

Это я понимаю (shift указателя), но не a + b + c + d. Смысл?

а ты си знаешь?

у меня там было сложение не указателей, а значений по указателю

читай внимательно: x + *a + *b + *c + *d имеет тип «целое число», а не «указатель на целое»

Это довольно странный способ узнать об этом, но, кажется, ты хочешь доказать такое высказывание: sum : {n m : ℕ} → Vec Bool n → (m ≤ n)

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

и обязательно он должен давать ошибки на варианты:

  switch( !!a + !!b + !!c + !!d ) {
    case 0: return x;
    case 1: return f1(x, a, b, c, d);
    case 2: return f2(x, a, b, c, d);
    case 4: return f3(x, a, b, c, d); 
    case 3: return x + *a + *b + *c + *d; // null pointer access
  }
  switch( !!a + !!b + !!c + !!d ) { // incomplete switch
    case 0: return x;
    case 1: return f1(x, a, b, c, d);
    case 2: return f2(x, a, b, c, d);
    case 4: return x + *a + *b + *c + *d;
  }
  switch( !!a + !!b + !!c + !!d ) {
    case 0: return x;
    case 1: return f1(x, a, b, c, d);
    case 2: return f2(x, a, b, c, d);
    case 3: return f3(x, a, b, c, d);
    case 4: return x + *a + *b + *c + *d;
    case 5: return x + 1; // unreachable
  }

> зависимости от количества экспериментальных данных, мы, с должным запасом в сторону надежности, вычисляем *a+*b+*c+*d

Если не проверишь их на NULL - сегфолт, если проверишь - твой неконвенционный switch не нужен.

каждая из функций f1, f2, f3 это такая приличная портянка с разбором случаев и комментариями

ну и что ты сэкономил своим switch?

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

1. не скатывается — квазимото известен тем, что постит простыни, когда надо задать вопрос, но это терпимо

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

2. изображать надо на чем-то; в с++ нет зависимых типов

Ну так придумай их.

опять же, надо чтобы можно было написать

int f1(int x, int* a, int* b, int* c, int* d)
{
  return x + ( !!a ? *a : !!b ? *b : !!c ? *c : *d )*3/2 ;
}

здесь, очевидно, откуда попало f1 вызывать нельзя, т.к. не проверяется, что d ненулевой (и даже если бы проверялось, не ясно, что выдавать, если он нулевой), однако если f1 сделать допустим вложенной функцией в f, или сделать модуль, который экспортирует только f, но не f1, то компилятор должен быть доволен

> Когда он делает это в темах «о языках вообще» - ладно, там люди понимающие. А здесь топик для приземленных драйверописателей.

нет уж

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

Если сказал «да, это можно» - приведи пример.

присоединяюсь к твоему пожеланию увидеть примеры на хаскеле

> присоединяюсь к твоему пожеланию увидеть примеры на хаскеле

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

> if (нашёл целые корни уравнения (x^n + y^n = z^n)) { и давай теперь требуй инструмент статического анализа, который отсечёт unreachable code

у нас же SMT-solver; варианты:

1. выдавать варнинг или ошибку, пока теорию, необходимую для этого уравнения, в SMT-solver не добавят

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

3. нашёл_целые_корни_уравнения это частичная функция?

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

3.2. если нет, то скорее всего из ее статического анализа видно, что она выдает и true и false

> Ну так придумай их.

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

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

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

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

> ну и что ты сэкономил своим switch?

щас напишу

ну и что ты сэкономил своим switch?

вот как это выглядело бы на си с паттерн-матчингом:

int h( maybe<int> a,  maybe<int> b,  maybe<int> c,  maybe<int> d)
{
  int x = g();

  switch( a ) {
    case Nothing:
      switch(b) {
        case Nothing:
          switch(c) {
            case Nothing:
              switch(d) {
                case Nothing: return x;
                case Just(dd): return h1(x, dd);
              }
            case Just(cc):
              switch(d) {
                case Nothing: return h1(x, cc);
                case Just(dd): return h2(x, cc, dd);
              }
          }
        case Just(bb):
          switch(c) {
            case Nothing:
              switch(d) {
                case Nothing: return h1(x, bb);
                case Just(dd): return h2(x, bb, dd);
              }
            case Just(cc):
              switch(d) {
                case Nothing: return h2(x, bb, cc);
                case Just(dd): return h3(x, bb, cc, dd);
              }
          }
      }
    case Just(aa):
      switch(b) {
        case Nothing:
          switch(c) {
            case Nothing:
              switch(d) {
                case Nothing: return h1(x, aa);
                case Just(dd): return h2(x, aa, dd);
              }
            case Just(cc):
              switch(d) {
                case Nothing: return h2(x, aa, cc);
                case Just(dd): return h3(x, aa, cc, dd);
              }
          }
        case Just(bb):
          switch(c) {
            case Nothing:
              switch(d) {
                case Nothing: return h2(x, aa, bb);
                case Just(dd): return h3(x, aa, bb, dd);
              }
            case Just(cc):
              switch(d) {
                case Nothing: return h3(x, aa, bb, cc);
                case Just(dd): return x + aa + bb + cc + dd;
              }
          }
      }
  }
}

отдельные функции h1,h2,h3 немного упрощаются, но это не оправдывает усложения функции h

int f1(int x, int* a, int* b, int* c, int* d)
{
  int not_null = !!a ? *a : !!b ? *b : !!c ? *c : *d;
  return x + not_null * 3 / 2 ;
}

int h1(int x, int not_null)
{
  return x + not_null * 3 / 2 ;
}

Ты реально ненавидишь паттерн-матчинг.

switch (a, b, c, d) {
case NULL, NULL, NULL, NULL:
        break;
case true, true, true, true:
        break;
case _, _, _, _:
        break;
}

Заметь, что в одной ветке используется NULL, а в другой true - значение указателя преобразуется к логическому, как и положено в Си. Если тебе не нравится идея преобразования:

switch (a != NULL, b != NULL, c != NULL, d != NULL) {
case true, true, true, true:
        break;
case false, false, false, false:
        break;
case _, _, _, _:
        break;
}

вариантов должно быть 5, и точка

я щас перепишу с твоим подходом

> вариантов должно быть 5, и точка

Ну, если нужно _всё в точности_ как у тебя, и напиши так, как сам написал, в чем проблема? То, что ты изначально написал - тоже примитивный паттерн-матчинг, кстати.

Ты реально ненавидишь паттерн-матчинг.

возможно, я не умею его готовить :-)

int h( maybe<int> a,  maybe<int> b,  maybe<int> c,  maybe<int> d)
{
  int x = g();

  switch( a; b; c; d ) {
    case Nothing; Nothing; Nothing; Nothing : return x;
    case Just(aa); Nothing; Nothing; Nothing :
    case Nothing; Just(aa); Nothing; Nothing :
    case Nothing; Nothing; Just(aa); Nothing :
    case Nothing; Nothing; Nothing; Just(aa) : return h1(x, aa);
    case Just(aa); Just(bb); Nothing; Nothing :
    case Just(aa); Nothing; Just(bb); Nothing :
    case Just(aa); Nothing; Nothing; Just(bb) :
    case Nothing; Just(aa); Just(bb); Nothing :
    case Nothing; Just(aa); Nothing; Just(bb) :
    case Nothing; Nothing; Just(aa); Just(bb) : return h2(x, aa, bb);
    /* тут мне лень было выписывать 4 варианта правильно*/
    case Just(aa); Nothing; Nothing; Nothing :
    case Nothing; Just(aa); Nothing; Nothing :
    case Nothing; Nothing; Just(aa); Nothing :
    case Nothing; Nothing; Nothing; Just(aa) : return h3(x, aa, bb, cc);
    case Just(aa); Just(bb); Just(cc); Just(dd) : return x+aa+bb+cc+dd;
}

> Ну, если нужно _всё в точности_ как у тебя, и напиши так, как сам написал, в чем проблема? То, что ты изначально написал - тоже примитивный паттерн-матчинг, кстати.

я не понял, где в твоем решении должны вызываться функции h1, h2, h3, и с какими аргументами; свой вариант с твоей идеей я чуть выше запостил

> switch (a, b, c, d)

запятая в си это еще и оператор, поэтому я использовал у себя в примере ";", хотя конечно там просится запятая

>> Ты реально ненавидишь паттерн-матчинг.

возможно, я не умею его готовить :-)

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

потом мне не нравится провал сквозь ветки, так что это можно было бы записать например так

int h( maybe<int> a,  maybe<int> b,  maybe<int> c,  maybe<int> d)
{
  int x = g(),

  switch( a, b, c, d ) {
    case (Nothing, Nothing, Nothing, Nothing) : return x;
    case (Just(aa), Nothing, Nothing, Nothing),
         (Nothing, Just(aa), Nothing, Nothing),
         (Nothing, Nothing, Just(aa), Nothing),
         (Nothing, Nothing, Nothing, Just(aa)): return h1(x, aa);
    case (Just(aa), Just(bb), Nothing, Nothing),
         (Just(aa), Nothing, Just(bb), Nothing),
         (Just(aa), Nothing, Nothing, Just(bb)),
         (Nothing, Just(aa), Just(bb), Nothing),
         (Nothing, Just(aa), Nothing, Just(bb)),
         (Nothing, Nothing, Just(aa), Just(bb)): return h2(x, aa, bb);
    case (Nothing, Just(aa), Just(bb), Just(cc)),
         (Just(aa), Nothing, Just(bb), Just(cc)),
         (Just(aa), Just(bb), Nothing, Just(cc)),
         (Just(aa), Just(bb), Just(cc), Nothing): return h3(x, aa, bb, cc);
    case (Just(aa), Just(bb), Just(cc), Just(dd)): return x+aa+bb+cc+dd;
}

есть ли вариант лучше?

> Ты его именно ненавидишь. Иначе я никак не могу объяснить, что вместо того, чтобы матчить сумму ряда признаков, ты матчишь весь ряд - при том, что для тебя имеет смысл только агрегированное значение.

непонимаю — я же с самого начала сделал свитч по сумме

напиши свой вариант в любом синтаксисе, только чтобы в нем вызывались h1, h2, h3

> я же с самого начала сделал свитч по сумме

Видимо, ты не считаешь switch паттерн-матчингом.

напиши свой вариант в любом синтаксисе, только чтобы в нем вызывались h1, h2, h3

Зачем? Пойнт в том, что если тебе нужно матчить сумму - так и делай. И получишь свой изначальный switch, но в синтаксической обертке какого-нибудь паттерн-матчинга.

> И получишь свой изначальный switch, но в синтаксической обертке какого-нибудь паттерн-матчинга.

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

>> я же с самого начала сделал свитч по сумме

Видимо, ты не считаешь switch паттерн-матчингом.

он отличается от обычного паттерн-матчинга тем, что на первый взгляд строка case 4: ... кажется разыменовывающей нулевые указатели, а после анализа — не кажется

бласт такое (ну или аналогичное) умеет, а вот то, что обычно называют паттерн-матчингом — похоже что не умеет

match one_if_notnull(a) + one_if_notnull(b) + one_if_notnull(c) + one_if_notnull(d) with
0 -> (* whatever *);
1 -> (* whatever *);
2 -> (* whatever *);
3 -> (* whatever *);
end

Функцию one_if_notnull, я надеюсь, писать не нужно? В Си ты ее использовал в виде !!.

Видимо, ты не считаешь switch паттерн-матчингом.

он отличается от обычного паттерн-матчинга

...только своей примитивностью

тем, что на первый взгляд строка case 4: ... кажется разыменовывающей нулевые указатели, а после анализа — не кажется

Паттерн матчинг здесь не причем.

>мы, как я понимаю, не можем, т.к. x +. a +. b +. c +. d будет типа MayBe Int, так?

scala> val l = Some(1) :: None :: Some(2) :: Nil;
l: List[Option[Int]] = List(Some(1), None, Some(2))

scala> l.flatMap(x=>x).foldLeft(0)(_ + _);
res1: Int = 3

подключайся

там проблема вовсе не в том, чтобы просуммировать Option-альные значения

> 3 -> (* whatever *);

end

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

> компилятор ее тебе выдаст?

Не знаю. Но я знаю, что в Си он ее не выдаст.

> Не знаю. Но я знаю, что в Си он ее не выдаст.

а бласт будет выдавать

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

собственно это я пытаюсь донести х.з. сколько времени

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

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

собственно это я пытаюсь донести х.з. сколько времени

Ты ХЗ сколько времени рисуешь чудовищные конструкции и называешь их паттерн-матчингом. А простая истина в том, что паттерн-матчинг умеет всё, что switch, и еще дофига всего.

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

«гипотетический компилятор Ocaml» проектировался в расчете на то, что кто-то будет добавлять к нему возможности проверять полноту матчинга (типа этой)?

> «гипотетический компилятор Ocaml» проектировался в расчете на то, что кто-то будет добавлять к нему возможности проверять полноту матчинга

Реальный компилятор Ocaml уже проверяет полноту матчинга. Достаточно ли он умен, чтобы понять, что значение 0..4 - хз.

> А простая истина в том, что паттерн-матчинг умеет всё, что switch, и еще дофига всего.

switch при наличии SMT-solver-а умеет все что паттерн-матчинг, и намного приятнее и надежнее, правда его требуется как-то согласовать с обычными АлгТД

> switch при наличии SMT-solver-а умеет все что паттерн-матчинг

Правда? А матчинг по чему-то более сложному, чем целые числа, он умеет?

> Ты ХЗ сколько времени рисуешь чудовищные конструкции и называешь их паттерн-матчингом.

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

после того, как экономия стала ясна, ты вернулся к моему варианту и стал именовать мой свитч частным случаем паттерн матчига

различие паттерн-матчинга от свича терминологическое, хотя есть 2 существенных детали:

1. паттерн-матчинг позволяет вводить новые переменные с областью видимости ветки *на основе выполнения гварда, защищающего ветку* — заметь, у меня в свиче они не вводятся (хотя вводятся в функциях f1,f2,f3)

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

> Правда? А матчинг по чему-то более сложному, чем целые числа, он умеет?

тут вообще-то можно было бы возразить, что множество АлгТД счетно, так что матчинг по ним это матчинг по целым числам, но есть смысл задуматься

> после того, как экономия стала ясна, ты вернулся к моему варианту

После того, как я понял твою странную задачу.

и стал именовать мой свитч частным случаем паттерн матчига

И выступил в роли КО. Кстати, ты не поверишь... любой switch, не только твой - это убогий паттерн-матчинг.

различие паттерн-матчинга от свича терминологическое, хотя есть 3 существенных детали:

0. Умеет работать со сложными структурами данных.

1. паттерн-матчинг позволяет вводить новые переменные с областью

2. паттерн-матчинг обычно проверяется компилятором

fixed

> множество АлгТД счетно, так что матчинг по ним это матчинг по целым числам

А еще есть паттерн матчинг по спискам.

в хаскеле, во всяком случае, паттерн-матчинг по спискам ничем не отличается от ПМ по АлгТД (разве что синтаксисом)

Тут у тебя «простой и ясный код» потому что f1-f3 могут применять нулевые указатели - но внутри они же должны делать выбор что у них ненулевое? Это и будут дополнительные варианты - просто матчинг разнесен в 4 функции.

Здесь

case (Just(aa), Nothing, Nothing, Nothing),
         (Nothing, Just(aa), Nothing, Nothing),
         (Nothing, Nothing, Just(aa), Nothing),
         (Nothing, Nothing, Nothing, Just(aa)): return h1(x, aa);

ты хочешь найти aa любой - но это же не так в f1..f3?

Потому что в этом случае можно описанный мной выше flat применить к списку из четырех Мейби значений и получить нормализованный список по Just a, и сделать 5 вариантов матчинга

 case a :: b :: c :: d => 
 case a :: b :: c => 
 case a :: b  => 
 case a  => 
 case Nil  => 

А если надо будет exhaustiveness check - то надо сгенерировать 22 подобных класса (это для 2х значений):

 sealed abstract class OptionTuple2[+T];

object OptionTuple2 {
	def apply[T](x:Option[T],y:Option[T]):OptionTuple2[T] = (x, y) match {
		case (Some(x), Some(y)) => OT2_2(x,y);
		case (Some(x), None) => OT2_1(x);
		case (None, Some(y)) => OT2_1(y);
		case (None, None) => OT2_Nothing;
	}
}

case object OT2_Nothing extends OptionTuple2[Nothing];
case class OT2_2[T](x:T,y:T) extends OptionTuple2[T];
case class OT2_1[T](x:T) extends OptionTuple2[T];

>А если надо будет exhaustiveness check - то надо сгенерировать 22 подобных класса (это для 2х значений):

Или Dependent Types.

у меня там было сложение не указателей, а значений по указателю

Да, не заметил.

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

В зависимых типах это будет выглядеть как раз как написание доказательств (функций) для высказываний (типов).

и обязательно он должен давать ошибки на варианты

В агде, например:

cn : Ref⁺ → Ref⁺ → Fin 3

test : Ref⁺ → Ref⁺ → _

test a b with cn a b
... | zero = _
... | suc zero = _
... | suc (suc zero) = _
... | _ = _

Ok

test a b with cn a b
... | zero = _
... | suc (suc zero) = _
... | suc (suc (suc _)) = _

Incomplete pattern matching for .M.with-19. Missing cases:
  .M.with-19 _ _ (suc {._} (zero {._}))

test a b with cn a b
... | zero = _
... | suc zero = _
... | suc (suc zero) = _
... | suc (suc (suc _)) = _
... | suc (suc (suc (suc _))) = _

ℕ.suc n != ℕ.zero of type ℕ
when checking that the pattern suc _ has type Fin ℕ.zero

test a b with cn a b
... | zero = _
... | suc zero = _
... | suc (suc _) = _
... | suc (suc (suc _)) = _

Unreachable clause

насчёт null pointer access:

Data : Set
Data = _

Address : Set
Address = _

record Null : Set where
  constructor null

record Ref : Set where
  constructor ref
  field
    address : Address
    value   : Data

Ref⁺ : Set
Ref⁺ = Null ⊎ Ref

т.е. value : Ref → Data а *не* value : Ref⁺ → Data, так что доступа к данным по null pointer-у не может быть вообще.

опять же, надо чтобы можно было написать

Ещё раз - весь код который ты тут пишешь использует только такие сишные конструкции как функции, операторы, if и switch. Те же самые конструкции есть и в хаскеле и в agde и где угодно. Почему ты думаешь, что весь этот код не может выглядеть там точно также (в хаскеле - функции/операторы = ленивые функции, if = if, switch = case)? Он так и будет выглядеть и паттерн-матчинг тут ни при чём.

Вот если бы тут были примеры с присваиванием, goto или longjump или, скажем, с тредами и IPC, это бы потребовало бOльших усилий, т.е. разработки _моделей_ выполнения с присваиванием, или goto, или longjump, или моделей многопоточных программ с расшаренной памятью. В хаскеле такие модели настраиваются с помощью монад (IO (или RWS), Cont, STM), хотя вообще могут быть определены непосредственно - заданием синтаксиса и статической семантики.

Я тут призывал к тому, чтобы точно зафиксировать типы (отделить мух от котлет) для чисел разной разрядности (причём в духе Fin (2 ^ n) из агды), для целых, натуральных и булевых чисел, для индексов, адресов, указателей, нулевых указателей и т.д. и т.п. Тогда в хорошо типизированном языке (adts + strong + static + well-typed) все упомянутые проблемы (null pointe-ов, покрытия и достижения всех clauses) отпадут сами собой.

Тогда, всё что остаётся это как раз «reasoning about programs», т.е. непосредственно верификация - доказательство определённых свойств программ. При этом любое конструктивное доказательство может быть проведено в языке с зависимыми типами, просто в силу используемой там метатеории (любое доказательство для данного языка, конечно). У Пирса недавно появилась книжка на эту тему.

тут вообще-то можно было бы возразить, что множество АлгТД счетно

Строки это АлгТД? Множество всех строк счётно?

«гипотетический компилятор Ocaml» проектировался в расчете на то, что кто-то будет добавлять к нему возможности проверять полноту матчинга (типа этой)?

Могу сказать, что любая нормальная реализация ML-я или haskell-я (например, GHC с -Wall) умеет полноту матчинга для ADT. Но они не умеют полноту матчинга для, например, чисел, т.к. числа там примитивные а не алгебраические типы.

В агде есть алгебраические числа (натуральные в виде чисел Пеано, целые со знаком) и зависимые типы для множеств с конечным числом элементов. Например, тип (Fin 3) это тип ровно из трёх элементов, поэтому, если делать по нему паттерн-матчинг, он не отстанет, пока не напишешь всех случаев - для 0, 1 и 2, причём в правильном порядке.

не умеют полноту матчинга для, например, чисел

Хотя, у GHC есть какие-то эвристики на эту тему:

t n = case n of { 1 -> 1; 2 -> 2; 3 -> 3; 5 -> 5 }

    Warning: Pattern match(es) are non-exhaustive
             In a case alternative:
                 Patterns not matched: #x with #x `notElem` [1#, 2#, 3#, 5#]

Я тут призывал к тому, чтобы точно зафиксировать типы (отделить мух от котлет) для чисел разной разрядности (причём в духе Fin (2 ^ n) из агды), для целых, натуральных и булевых чисел, для индексов, адресов, указателей, нулевых указателей и т.д. и т.п. Тогда в хорошо типизированном языке (adts + strong + static + well-typed) все упомянутые проблемы (null pointe-ов, покрытия и достижения всех clauses) отпадут сами собой.

ыыы!

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

f n = case (n*n) `mod` 4 of { 0 -> 0 ; 1 -> 1; 2 -> 99; 3 -> 99 }

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

> Я тут призывал к тому, чтобы точно зафиксировать типы (отделить мух от котлет) для чисел разной разрядности (причём в духе Fin (2 ^ n) из агды), для целых, натуральных и булевых чисел, для индексов, адресов, указателей, нулевых указателей и т.д. и т.п. Тогда в хорошо типизированном языке (adts + strong + static + well-typed) все упомянутые проблемы (null pointe-ов, покрытия и достижения всех clauses) отпадут сами собой.

этого *недостаточно*

1. пусть у нас есть корректная програма на си (корректность понимаем так, что она никогда не разыменовывает нулевые указатели)

2. пусть мы эту программу переписываем с МауВе, или вообще с АлгТД, и при этом обязательно требуется:

2А. либо тонна бойлерплейта, возможно чуток обобщенная и вынесенная с глаз долой в отдельный файл (как это предлагает r)

2В. либо отход от естественного порядка написания программы (пример: если специфика предметной области подталкивает к тому, чтобы отдельно рассматривались именно случаи 0,1,2,3,4 ненулевых указателя, а не все 16 отдельных комбинаций)

в результате: это означает фейл языка, на который мы ее переписали

тут должнен бытье еще пункт

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

я раскрою его постом ниже

(это на тему 2С, см. выше)

l.flatMap(x=>x).foldLeft(0)(_ + _);

до меня наконец дошла твоя идея

в принципе да, мы можем написать

int zero_if_nothing(maybe<int> t) { 
  switch(t){
    case Nothing: return 0;
    case Just(tt): return tt;
  }
}

int f( maybe<int> a, maybe<int> b, maybe<int> c, maybe<int> d )

  int x = g();

  switch( is_just(a) + is_just(b) + is_just(c) + is_just(d) ) {
    case 0: return x;
    case 1: return f1(x, a, b, c, d);
    case 2: return f2(x, a, b, c, d);
    case 3: return f3(x, a, b, c, d);
    case 4: return x + zero_if_nothing(a) + zero_if_nothing(b) + zero_if_nothing(c) + zero_if_nothing(d);

}

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

но тут проблемы:

* для сложения нужно zero_if_nothing, для умножения нужно one_if_nothing, для каких-то операций может вообще не быть нейтральных элементов, и тогда код становится совсем стремным (грозящим неправильным рефакторингом)

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

ну или в «си с обязательными проверками перед разыменованием» это же могло бы выглядеть так:

int f(int* a, int* b, int* c, int* d)
{
  int x = g();

  switch( !!a + !!b + !!c + !!d ) {
    case 0: return x;
    case 1: return f1(x, a, b, c, d);
    case 2: return f2(x, a, b, c, d);
    case 3: return f3(x, a, b, c, d);
    case 4: return x + (a ? *a : 0)+ (b ? *b : 0) + (c ? *c : 0) + (d ? *d : 0);
  }
}

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

>* для сложения нужно zero_if_nothing, для умножения нужно one_if_nothing,

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

т.к. выражение сделано работающим там, где оно работать не должно

Как работают f1..f3? Потому что я как-то с трудом представляю что эта программа может делать, ведь в случае (Just a, Nothing, Nothing, Nothing) и (Nothing, Just b, Nothing, Nothing) вызывается один и тот же f1, но с разными аргументами. Тут или взаимноисключающая логика подразумевается с выбором внутри f1..f3, или тогда все a..d можно обрабатывать как список значений - а тут уж списочные операции в руки.

Тут у тебя «простой и ясный код» потому что f1-f3 могут применять нулевые указатели - но внутри они же должны делать выбор что у них ненулевое? Это и будут дополнительные варианты - просто матчинг разнесен в 4 функции.

т.е. у тебя тоже сомнения, что мой свич че-то экономит?

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

вот пример, который использует расширение си — си с ограниченными локальными функциями, которые, почти что не отличаются от define

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

int f(int* a, int* b, int* c, int* d)
{
  int x = g();

  // возращают значения по первому, последнему, и среднему ненулевому указателю из указателей в последовательности a, b, c, d
  int first() { return a ? *a : b ? *b : c ? *c : *d ; }
  int last()  { return d ? *d : c ? *c : b ? *b : *a ; }
  int middle(){ return (!a || !b) ? *c : *b; }

  switch( !!a + !!b + !!c + !!d ) {
    case 0: return x;
    case 1: return h1( x, first() );
    case 2: return h2( x, first(), last() );
    case 3: return h3( x, first(), middle(), last() );
    case 4: return x + *a + *b + *c + *d;
  }
}

тут аналогия с ПМ доведена до конца в одном куске кода

тут может быть возражение, что *сразу* надо было писать h1, h2, h3, и не запутывать ситуацию с f1, f2, f3, которым могут передеваться нулевые указатели

я не согласен — на самом деле, h1, h2, h3 — это уступка сторонникам паттерн-матчинга, и одной лишь информации о ненулевых аргументах может быть мало — нам еще нужна инфа о позициях ненулевых аргументов

Тут или взаимноисключающая логика подразумевается с выбором внутри f1..f3, или тогда все a..d можно обрабатывать как список значений - а тут уж списочные операции в руки.

насчет списочных операций

пусть a..d это полученные (или неполученные) экспериментальные значения

когда их 4 штуки, мы можем по ним построить кривую методом наименьших квадратов, и обсчитать все что мы хотим с достаточной точностью

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

так что списочные операции пролетают

кстати, моя ошибка — надо было написать

case 0: return x-100;

чтобы неповадно было обращаться с ними как со списком

и case 4: return x + *a + *b + *c + *d; я тоже зря сделал таким простым

>дело в том, что когда уже известно, что у нас есть эн ненулевых указателей, то матчинг в этом случае вести проще

Но это же списочная обработка? Незачем их обрабатываьт позиционно - там сверху было как их обработать списком - тоже пять вариантов на паттерн матчинге. Ну а exhaustiveness check - dependent types.

>так что списочные операции пролетают

Независимые от длины списка. Зависимые - нет.

чтобы неповадно было обращаться с ними как со списком

«кусок кода 2» все еще валиден и паттерн матчинг на 5 значений
Архитектура системы верификации кода драйверов Linux (комментарий)

> «кусок кода 2» все еще валиден и паттерн матчинг на 5 значений Архитектура системы верификации кода драйверов Linux (комментарий)

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

кстати, я рассматривал мысль сделать аналогичный вариант на с++11, где один шаблон может вызываться с любым вариабельным количеством аргументов (а не от 0 до 22 :-)

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

> «кусок кода 2» все еще валиден и паттерн матчинг на 5 значений Архитектура системы верификации кода драйверов Linux (комментарий)

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

но оценка языка, по-моему, отсюда следует однозначная

>> так что списочные операции пролетают

Независимые от длины списка. Зависимые - нет.

от того, что ты назовешь любые 0..4 целых чисел списком, формулы для h1, h2, h3 одинаковыми («списочными») не станут — я это имел в виду

> от того, что ты назовешь любые 0..4 целых чисел списком, формулы для h1, h2, h3 одинаковыми («списочными») не станут — я это имел в виду

Зато с DT появится exhaustive PM и полиморфизм по длине.

DT = ?

> и полиморфизм по длине.

полиморфизмы по длине разные бывают

бывает полиморфизм в стиле шаблонов (для каждой длины свой код), а бывают в стиле дженериков (пофиг длина! делай вот это)

dependent types

ыыы!

Ну что смешного, поделись? :)

Ты тут путаешь (как и я в этом треде чуть раньше). unreachable code != unreachable clause. unreachable clause это нечно весьма определённое, но вместе с зависимыми типами (вроде Fin) оно может дать всё что нужно для доказательства отсутсвия unreachable code (естесвенно, _доказывать_ придётся руками).

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

Fin 2. Надо доказать, что f : ℕ → Fin 2.

кстати, интересно было бы на него взглянуть

Тут, например, можно посмотреть как подобные вещи там делают - http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/DivMod.agda

этого *недостаточно*

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

переписываем с МауВе, или вообще с АлгТД

Само произношение «АлгТД» забавное :) Но это же всё частности которыми не исчерпывается то что умеют математизированные ЯП.

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

либо отход от естественного порядка написания программы (пример: если специфика предметной области подталкивает к тому, чтобы отдельно рассматривались именно случаи 0,1,2,3,4 ненулевых указателя, а не все 16 отдельных комбинаций)

Это вообще не понятно. Весь код в твоих примерах настолько прост, что его и переписывать не нужно, проблема только в том, что это ill-typed код, прежде чем о чём-то говорить нужно хотя бы сделать код хорошо типизированным.

> Строки это АлгТД? Множество всех строк счётно?

ты спрашиваешь то, что знают все первокурсники

пусть алфавит конечен

множество строк конечной, но сколь угодно большой длины счетно

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

(вообще память у компьютера ограничена, так что множество строк конечно, но так как досчитать даже до 10^50 мы не можем, то такие числа лучше рассматривать как принадлежащие к счетному множеству)

пусть алфавит конечен

А если нет? Например, такой ADT как [ℕ] счётный?

множество строк конечной, но сколь угодно большой длины счетно

Ну хорошо,

ℕ = 0 | s ℕ
|ℕ| ≡ ℵ₀

[a] = [] | a : [a]
if |a| < ℵ₀ then |[a]| = ℵ₀
if |a| = ℵ₀ then |[a]| = 2 ^ ℵ₀ ≥ ℵ₁

> А если нет? Например, такой ADT как [ℕ] счётный?

а если подумать?

понятно, что теоремы можно и забыть, но ведь очевидно, что любой его элемент записывается в виде строки над конечным алфавитом, например 375:1900287:7:12:22

> |[a]| = 2 ^ ℵ₀

2 ^ ℵ₀ это все подмножества натурального ряда, тогда как [a] это только конечные

естественно, это все написано про не-ленивые языки

в случае лени у тебя кроме хвоста из настоящих натуральных чисел может стоять thunk, множество которых тоже счетно

> Весь код в твоих примерах настолько прост, что его и переписывать не нужно, проблема только в том, что это ill-typed код, прежде чем о чём-то говорить нужно хотя бы сделать код хорошо типизированным.

если система типов твоего языка не может доказать корректность корректного конкретного кода (это ты называешь ill-typed код?), то это проблемы твоего языка и его создателся, а не мои

по агде есть конкретный вопрос

пусть у меня есть мегабайтовый исходник с каким-то кодом, в нем есть 2 строки

f::Int->Int
f n = case (n*n) `mod` 4 of { 0 -> 0 ; 1 -> 1; 2 -> 99; 3 -> 99 }

напускаем на это допустим агду

1. выдаст ли она «варнинг: недостижимый код»?

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

или может переопределить, оператор `mod` или может быть оператор умножения  — но при этом запрещается менять саму функцию

> Тут, например, можно посмотреть как подобные вещи там делают - http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/DivMod.agda

ты сунул мне кусок стандартной библиотеки агды, и зачем?

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

> Ты тут путаешь (как и я в этом треде чуть раньше). unreachable code != unreachable clause. unreachable clause это нечно весьма определённое,

раскрой пожалуста подробнее смысл этого «нечно весьма определённого», смысл недостижимого кода и докажи, что unreachable code != unreachable clause

А если нет? Например, такой ADT как [ℕ] счётный?

а если подумать?

То что [ℕ] несчётный это то что Кантор доказывал (про действительные числа и диагональный аргумент).

2 ^ ℵ₀

Множество с такой мощностью это, как минимум, несчётное множество (вне зависимости от CH, причём).

тогда как [a] это только конечные

[a] это:

[a] ::= [] | a [a]

т.е. и бесконечные тоже.

Правда, вопрос о том сколько (ℵ₀, 2 ^ ℵ₀, ℵ₁, ... ?) неизоморфных ADT можно задать с помощью метаязыка задания ADT (т.е. типы суммы от от типов произведений) несколько сложнее. Твой изначальный посыл был, вроде, в том, что множество ветвей у switch/case счётно, что верно, т.к. часть грамматики ADT про вариантные типы такая:

type_sum ::= type_prod | type_prod type_sum

т.е. количество вариантов счётное.

корректность корректного конкретного кода

КККК? Я что-то плохо понимаю, уже поздно, наверно. Но:

если система типов твоего языка не может доказать

Какая система типов какого языка? Вообще, пусть будет хоть какая-то _система_ типов (т.е. формальная и непротиворечивая), чем её не будет вообще (как в си). Пусть будет система типов хотя бы как в Cyclone. Доказательства корректности это уже другой вопрос.

это ты называешь ill-typed код?

Это около-хаскельное понятие, ill-typed это всё что не well-typed, а well-typed язык это язык с заданной формальной и непротиворечивой статической семантикой.

ты сунул мне кусок стандартной библиотеки агды, и зачем?

Чтобы ты посмотрел тип _mod_ и то почему у неё именно такой тип.

раскрой пожалуста подробнее смысл этого «нечно весьма определённого», смысл недостижимого кода и докажи, что unreachable code != unreachable clause

Пожалуй, не буду этого делать. Ну, то есть, one всегда может заняться самообразованием :)

по агде есть конкретный вопрос

Напиши функцию squere_mod_4 : Integer -> Fin 2 и замени case (n*n) `mod` 4 of на case squere_mod_4 n of (в агде это будет не case а with), тогда скомпилируется только { 0 -> _ ; 1 -> _; } и ничего другого. При этом f останется совместимой со всем остальным кодом.

На хаскеле это будет так (чтобы пояснить идею):

{-# LANGUAGE GADTs, KindSignatures #-}

data Z
data S n

class N t
instance N Z
instance N n => N (S n)

type N0 = Z
type N1 = S N0
type N2 = S N1
-- ...

data Fin :: * -> * where
  Zf :: N n => Fin (S n)
  Sf :: N n => Fin n -> Fin (S n)

unproven :: a
unproven = error "totality is not proven."

unreachable :: a
unreachable = error "unreachable code."

square_mod_4 :: Int -> Fin N2
square_mod_4 n = case (n * n) `mod` 4 of
  0 -> Zf
  1 -> Sf Zf
  _ -> unproven

f :: Int -> Int
f n = case square_mod_4 n of
  Zf    -> 0 
  Sf Zf -> 1
  _     -> unreachable

слишком вербозно и без возможности доказать тотальность функций.

> т.е. и бесконечные тоже.

я уже сказал, что рассматриваю не-ленивые языки, и там это конечные

ленивые языки надо рассматривать отдельно — там в списке будут thunk-и, а не целые числа

в общем, если ты собрался поупорствовать на тему несчетности, я могу поспорить с тобой дальше, но на самом деле это детский сад

> То что [ℕ] несчётный это то что Кантор доказывал (про действительные числа и диагональный аргумент).

бугага

этот диагональный аргумент легко можно применить для доказательства того, что существует такое подмножество натурального ряда, что любой [ℕ], полученный в результате выполнения конечного кода (т.е. помещающегося в файл конечного размера) на хаскеле, с ней не совпадет

вообще множество конечных программ на хаскеле счетно, и множество тиков таймера тоже счетно — как ты собрался с их помощью пересчитать несчетное множество?

я уже сказал, что рассматриваю ... языки

ЯП тут вообще ни при чём, это чистая математика. В реальности вообще память ограничена.

вообще множество конечных программ на хаскеле счетно, и множество тиков таймера тоже счетно — как ты собрался с их помощью пересчитать несчетное множество?

Вот я и говорю, ADT это язык (не ЯП, а формальный математический язык) для конструктивного задания множеств и мощности задаваемых множеств нужно оценивать строго в математическом смысле. Есть другие языки (inductive families, категорное задание множеств), при этом говорить «множество всех ADT счётно» нельзя, можно сказать, что множество ветвей у данного switch/case счётно если они работают на (воображаемой) машине с бесконечной памятью, или что на машине с конечной памятью в рантайме мы можем аллоцировать только конечное количество объектов разных типов данных, ну и т.п.

этот диагональный аргумент легко можно применить для доказательства того, что существует такое подмножество натурального ряда, что любой [ℕ], полученный в результате выполнения конечного кода (т.е. помещающегося в файл конечного размера) на хаскеле, с ней не совпадет

Мой парсер, мой парсер!1 :)

> Вот я и говорю, ADT это язык (не ЯП, а формальный математический язык) для конструктивного задания множеств и мощности задаваемых множеств нужно оценивать строго в математическом смысле.

прекрасно

1. алфавит этого формального математического языка, надеюсь, конечен? (да/нет)

2. этот язык допускает слова только конечной, но сколь угодно большой длины? (да/нет)

Мы будем говорить о мощности множества термов данного ADT?

Тогда несчётны по крайней мере:

• Множества всех инфинитных строк на финитных алфавитах (n ^ ℵ₀ = 2 ^ ℵ₀ ≥ ℵ₁).
• Множества всех инфинитных строк на инфинитных алфавитах (ℵ₀ ^ ℵ₀ = 2 ^ ℵ₀ ≥ ℵ₁). Например, можно взять счётные целые числа, счётное множество простых чисел и построить несчётное множество действительных чисел как сепарабельное декартово пространство (следуя основной теореме арифметике которая тут совпадёт с теоремой об однозначности разложения вектора по ортам в декартовом пространстве).
• Всех финитных n-арных деревьев (n ^ ℵ₀ = 2 ^ ℵ₀ ≥ ℵ₁).
• Всех n-кортежей финитных строк на финитных алфавитах (n ^ ℵ₀ = 2 ^ ℵ₀ ≥ ℵ₁). ℝ в виде записи с целой и дробной частями как раз такой 2-кортеж, для которого применим диагональный аргумент.

В последних двух пунктах у нас даже обычные (финитные) структуры (деревья, строки и кортежи). Вот ещё ссылка на тему - http://okmij.org/ftp/Computation/uncountable-sets.html.

Если же говорить про то сколько неизоморфных ADT задаётся с помощью языка задания ADT, то тут paper надо писать, по крайней мере я не видел ничего на эту тему вообще.

А ∞-арные деревья и ∞-кортежи это, видимо, ℵ₀ ^ ℵ₀ = 2 ^ ℵ₀ ≥ ℵ₁

сколько неизоморфных ADT задаётся с помощью языка задания ADT

И про inductive families тогда не забыть, они интереснее.

далее слово финитный я понимаю как «имеющий конечное число элементов»

Тогда несчётны по крайней мере ... множества ... Всех n-кортежей финитных строк на финитных алфавитах

чувак, я могу понять то, что ты что-то не знал или что-то забыл

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

множество всех n-кортежей финитных строк на финитных алфавитах можно инъективно вложить во множество финитных строк над финитным алфавитом следующим образом: добавим к алфавиту новый символ "," и запишем элементы кортежа друг за другом, разделяя их запятой

заметим, что это работает, даже если n у тебя не фиксировано, и ты неявно подразумевал «объединение по всем натуральным n множеств всех n-кортежей финитных строк на финитных алфавитах»

Всех финитных n-арных деревьев

я полагаю над конечным алфавитом? ну пусть даже и над счетным, не важно

представим каждый элемент счетного алфавита в виде строки с его номером в виде десятичного числа

точно так же добавим в алфавит три символа "(" ")" "," и запишем каждое дерево в виде (вершина,ветвь,ветвь,ветвь), где каждая ветвь тоже в свою очередь дерево или элемент алфавита

в результате — опять мы представили каждый элемент Несчетного По Квазимото Множества в виде конечной строки над конечным алфавитом

какое несчастье :-(

ℝ в виде записи с целой и дробной частями как раз такой 2-кортеж

дробная часть это не финитная строка

короче, ты порешь полную чушь

Тогда несчётны по крайней мере: Множества всех инфинитных строк на финитных алфавитах

детский саааааааад

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

Про деревья - множество всех бинарных деревьев изоморфно множеству финитных и инфинитных бинарных строк, мощность которого = мощность континуума. Или так - берём бинарное дерево n-ой глубины, тогда количество его поддеревьев, т.е. бинарных деревьев глубиной до n это, с точностью до коэффициентов, 2 ^ n, тогда в пределе деревьев до счётной глубины получаем 2 ^ ℵ₀ = мощность континуума.

детский саааааааад

Ага. Вот есть множества, есть их мощности, отрицать, что тут возникают как множества счётной мощности так и множества с мощностью континуума (чисто формально) нельзя - это так.

да, несчетны, но как это связано с моей попыткой решения задачи верификации для АлгТД?

Про покрытие всех clauses мы уже решили (и сказали, что haskell/agda так умеют, а agda ещё и Fin типы умеет). А про счётность ADT - хотя это и не имеет практического значения, говорить «множество всех ADT счётно» нельзя. Можно сказать «нам нужно только счётное множество ADT», или «case осуществляет выбор по счётному количеству вариантов», хотя даже это имеет чуть более чем никакое практическое значение :)

дробная часть это не финитная строка

Точно. Про «n-кортежи финитных строк на финитных алфавитах» ступил. Но всё ещё остаются инфинитные строки и финитные (!) деревья :)