- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
typedef struct {
UInt8 byte0;
UInt8 byte1;
UInt8 byte2;
UInt8 byte3;
UInt8 byte4;
UInt8 byte5;
UInt8 byte6;
UInt8 byte7;
UInt8 byte8;
UInt8 byte9;
UInt8 byte10;
UInt8 byte11;
UInt8 byte12;
UInt8 byte13;
UInt8 byte14;
UInt8 byte15;
} CFUUIDBytes;
signers. In principle, the necessary mechanisms (based on dependent types—see §30.5) are
well understood, but packaging them in a form that balances expressive power, predictability
and tractability of typechecking, and complexity of program annotations remains a significant
challenge. Some recent advances in the area are described by Xi and Pfenning (1998, 1999).
- Benjamin C. Pierce
* Для недоверчивых говнокодеров :)
>либо определяют тип как ValidRange[0...N]
А как еще определить массив?
Some recent advances in the area are described by Xi and Pfenning
> для связного списка чисел
Мы говорим о массивах.
Ну да. Это я понял.
Как вы собираетесь проверить выбор абсолютно произвольного элемента,
индекс которого в переменной, вводимой пользователем.
Причем проверить что введет пользователь НА ЭТАПЕ КОНПЕЛЯЦИИ.
Причем массив может быть динамическим и иметь произвольную длину.
Вы в своем уме?
все равно это будут проверки
стоило городить это всё - управляемые языки не столько уж оверхеда дают при индексном обращении - да обращение даже к кешу небось займет больше тактов, чем одно лишнее сравнение беззнаковых целых чисел
Ладно, расходимся. Это очередной вброс, дальше последуют абсурдные аргументы, ссылки на непонятных авторитетов и дискуссия сведется к превосходству лиспа над другими языками (js в частности).
Причем для x86, скорее всего, компилятор помечает переход как "маловероятный", и оверхед от криво предсказанного перехода будет только при вылете за границы массива. А в этом случае на него уже насрать.
А как в ассемблере х86-х64 отметить переход "маловероятным"?
http://bit.ly/YEdyCG
Короче, чего я рапсинаюсь. Находите доклад: Xi, Hongwei and Frank Pfenning. Eliminating array bound checking through dependent types. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada, pages 249–257, 1998.
Просвещаетесь самостоятельно.
Ответ не только автору поста выше, просто, чтобы не повторять.
Какое "говно"? У кого "но книга - говно" увидели? Слово "говно" - по треду использовали только Вы. Никто не критиковал Книгу.
Вам задали конкретные вопросы. "Как это сделать в рантайме?"
А Вы увиливаете.
Array[0][Integer], Array[1][Integer], ... Array[N][Integer];
Array[0][Float], Array[1][Float], ... Array[N][Float];
и вы в програмном коде обязаны указывать размер массива, когда описываете функцию, которая с ним работает. Конечно, у такого упрощенного варианта есть масса недостатков, т.как создание родовых функций окончится так же печально, как и попытка сравнить два числа в Скале.
Но не все так плохо, и теоретически доказано, что в принципе, возможно построить систему которая на семантическом уровне предотвратит рантайм проверки (т.е. если код скомпилировался, то значит, что он валидный, и в рантайме ничего проверять уже не нужно).
Использовать Си для примера применения такой системы - занятие очень неблагодарное, т.как в Си система типов не просто безалаберная, она небезопасная и нелогичная...
Тут вопрос возникает - сколько займет времени сборка сложного проекта?
И не дешевле ли ставить везде копеечные проверки и не париться? Если повсюду итак используют тяжеленные виртуальные машины.
А то может оказаться что на джаве проект уже давно работает, а на ASTе только скомпилился.
> И не дешевле ли ставить везде копеечные проверки и не париться?
Не в том суть. Есть задачи, в которых неправильный ответ или экцепшн в рантайме может повлечь катастрофу. А здесь все-таки гарантия, что если все тайпчекнулось, и наши предположения о системе верны, и если не распидорасит аппаратную часть, то все будет ок.
А компилируется оно скорее всего быстро. Просто скажет, что недостаточно данных для доказательства, вот и все. Я не занимался этими теориями, но насколько позволяет понять мое дилетантское чутье, большинство инвариантов придется описывать самому. И вот на это и уйдет основная часть времени.
Что было первее? Курица или Тролль?
Чуваки все еще компилят прошивку для реактора на ATS'е, а наш, с прошивкой на жабе, уже взорвался, т.к. всегда падал в рантайме если стержни вдвинуты на 25.67%.
FYI: Чернобыль, перед своим закрытием в 2000-ном приносил нищему хохлостану миллиард долларов в год.
Вот сколько стоит задержка.
А его строили, как и многое в совке, в крайней спешке и очень небрежно, но что поразительно большинство из тех заводов работает до сих пор.
Если б их коммунисты сделали за те же деньги меньше реакторов, но дорогих и с абсолютной защитой от дурака. Мы не имели столько работающих АЭС с "опасными" РБМК и производящих немыслимое количество энергии. И экономика встала бы.(ну или стали б больше больше экономить)
В нашей жизни, в нашей стране много чего делается в спешке и через жопу, но именно эти решения имеют наибольшую практичность.
Это парадоксальный, но вполне реальный факт.
человеку дышать тоже опасно - водой, например, дышать получается недолго
Тем более что дорогие ВВЭР имели защитную оболочку.
Извечная проблема короче:
дешево быстро качественно
у рбмк положительная реактивность
Можно только уменьшить вероятность фейла до разумных пределов, и надеяться на лучшее.
И большинство проблем как раз из-за ошибок операторов, а не из-за багов в прогах или железе ;(
Тут как бы делается предположение исходящее из практики Си[-подобных] языков, где тип задается вообще еще даже до появления переменной. Но вот, например, в CaML тип задается тогда, когда он становится известен. Например, если мы создали список, но еще ничего в него не положили, то тип у списка "список непонятно чего", но после того, как мы туда положили число - то это список чисел.
Похожим образом можно было бы работать и с массивами: если есть код до этого как-то определивший длину, или, по крайней мере позволивший предположить, что как минимум Х элементов там уже есть, то ошибки типов нет. Но возникают проблемы с пользовательским вводом, который не известен заранее и т.д.
Но как уже в самом верху говорилось: в то время, как теоретически доказано, что такую систему можно построить, сделать ее практичной в полном объеме представляется пока что нереальным. И вот тому, кто построит - будет бочка варенья и сколько-то там печенья.
А ведь суть всех этих зависимых типов совсем не в устранении рантайм проверок... Очень многие рантайм проверки устранить нельзя вообще, по определению, т.к. они проверяют данные из внешних источников.
Суть, имхо, в том, чтобы убедиться в необходимости и достаточности этих проверок. В первую очередь в достаточности, т.к. от этого зависит корректность кода. Во вторую очередь в необходимости, т.к. от этого зависит всего лишь эффективность.
значит компилятору нужно предусмотреть выделение ресурсов на этот элемент.
Фу, любитель скрытых ошибок.
Запомни милый бот одно:
Нет юнит-тестов - код говно.
Идеальный программист в идеальных условиях в идеальном мире... В реале же - забывают, забивают, не успевают, не замечают...
А компилятор и рантайм - они бессильны. Они не искуственный интеллект. Они ничего не понимают в задаче, они не знают, как им поступить в критической ситуации. Они в конце-концов не несут ответственности за последствия, вызванные неправильной работой программы. Поэтому они не имеют никакого права пытаться что-то исправить. Максимум что они могут - просигнализировать об ошибке. В идеале - сразу при компиляции.
Верно.
Но если программа не умирает, а втихушку продолжает творить хуйню портя данные, выдавая неправильные результаты, исполняя рандомные вещи - то лучше бы она умерла. И программист написавший ее так - еще большее говно.
Каждая программа, каждая функция должна быть написана так, чтобы продолжала выполнять своё предназначение, даже если крякнет процессор, и даже если отключится питание.
> значит компилятору нужно предусмотреть выделение ресурсов на этот элемент.
Вот это между прочим фатальная ошибка. Программист забыл проверить диапазон. Если мы сейчас выделим память, и дадим программе работать дальше - она натворит хуйни. В 99.99% подобных случаев смерть лучше чем хуйня в ответе.
Одно дело те ошибки, которые учтены программистом, и на которые он может придумать адекватную реакцию. Тут я полностью согласен - нужно продолжать работу. Ну или показать какой-то совет юзеру или записать ошибку в лог.
Другое дело - ошибки, которые программист не учел. Вот тот самый вылет за границы массива это почти всегда фейл программиста. И продолжение работы приведет только к новым проблемам. В первую очередь к тому, что программист не увидит ошибку, не узнает о ней, и она будет жить годами, пока кто-то не нарвется на серьезные последствия от нее.
Поверьте, вылет программы или дроп сессии это далеко не самое страшное, что может случиться...
P.S. Задачи, естественно, разные. Но молчаливое продолжение работы в ситуации неучтенной программистом очень редко будет адекватным поступком.
Вариант 1 - прога вылетела не дав распечатать квитанции. Позвонили программисту, тот почитал логи, нашел ошибку, пофиксил. Все довольны.
Вариант 2 - прога продолжила работу, насчитала хуйни, квитанции распечатали, разнесли по домам. Весь месяц контора выслушивала вопли от жильцов, а программист - от конторы. Куча потраченного времени и нервов.
Но ведь они в точности следуют вашим заветам "Нет элемента? Так давайте запилим!".
Какие-то типично ламерские варианты.
Очевидно же, что при возникновении исключения, прога должна попытаться исправить это исключение. Например несовпадение КБК - ищем по базе наиболее вероятное. Если проге нечего ответить - тогда отправляем уведомление текущему пользователю. Глупо продолжать выполнение явно ошибочной последовательности. Но и вылетать синей смертью, без попыток исправления, логгирования и уведомления - как минимум невежливо.
В контексте комментария, последовательность явно не ошибочная.
Для этого и придуман.
Но в целом, прав, да.
Вот скажем http://okmij.org/ftp/Haskell/types.html#branding, здесь операции над массивом заворачивают в brand, граничные индексы получаем от этого brand, можно получать следующий / предыдущий индекс / брать середину. Из чисел, разумеется, индекс не получить.
Так что уж, по крайней мере, то, что я написал выше - ну уж никак не неожиданность.
> Например, 2^32
Зачем в программе столько массивов с заранее известной длиной?
> что будет
Автора такой программы увезут к себе люди в белых халатах.
Там автор этого метода предполагает, что компилятор должен будет создать столько уникальных s, сколько разных массивов есть:
вот, тут вот. И дальше он выдвигает уникальность s, как залог работоспособности системы.
[...] The uniqueness of 's'
afforded by the explicit universal quantification prevents mixing up of
different brands.
Так что с этим проблем вроде нет.
Это уже аппелирование к конкретной реализации, bormand же бьет в основу :)
:) Никто ж не говорит "одновременно", можно и постепенно, сегодня - миллион, завтра - еще миллион.
Вот этот вот BArray и BIndex'ы можно юзать только совместно. Значения, полученные из разных вызовов brand смешать между собой не получится.
// ну все-таки вызывается первая ф-ия, а "вторая" - это значения по умолчанию, лучше бы просто вернули (Maybe w)
Вы в упор не видите разницы между тем, сколько раз вызов функции написан в коде, и сколько раз он будет произведен в рантайме?
Вот сколько раз надпись brand встречается в коде, столько временных типов сгенерит тайпчекер. На то, сколько раз потом этот brand будет вызываться в рантайме всем похер, и в первую очередь на это похер тайпчекеру.
Ага, 4 гигабайта в исходниках клипсы занимают конструкции в духе a[i]...
Санитары, срочно в палату!
P.S. Пойду я спать, уже 3 часа ночи, а разговор с интересной темы скатился в какой-то маразм про миллиард операторов.
Это к тому, что сие возражение непосредственного отношения к статье не имеет.
* - В принципе, когда мы определяем тип, то, с конструктивистксой точки зрения, его нужно наполнять, и / или это можно представить как если бы мы могли конкретизировать тип до минимальных составляющих. Так, например, во вселенной представленной в нашей программе неявно всегда существует все множество целых чисел (хотя создаем реально мы только небольшой процент от всего множества), бесконечное множество строк и т.д.
В рантайме-то их не будет.
Хороший, годный подход. Устранение проверок границ массивов путем устранения самих массивов.
Ну правильно,зачем нам проверки, они дорогие.
Давайте лучше разом повысим алгоритмическую сложность.
Почему это? Просто нужно получить каким-то образом BIndex, получили - доступ по индексу O(1). Ну можно расширить какими-нибудь методами вроде линейной комбинации двух индексов. Нужно смотреть конкретный пример, где подобный подход будет препятствием и делать вывод о его принципиальности.
Ну вот можно, конечно, добавить в trusted kernel функцию, которая по числу и массиву вернет Maybe BIndex. Но здесь ведь и будет таиться та самая проверка, от которой пытались избавиться...
Конкретный пример... да абсолютно любой алгоритм, в котором массив используют как массив, а не как список/бинарное древо.
Нужно показать принциальную необходимость получения имеенно из числа, а не из уже полученных BIndex-ов.
> как массив, а не в духе списка.
bsearch по ссылке явно не в духе списка, насколько в духе массива или дерева - не скажу
Имхо вся сила и польза массива в его эффективной операции произвольного доступа. Нет произвольного доступа - массив не нужен.
Вопрос насколько широкий класс алгоритмов отсекается, которым нужен доступ по числам, а не ранее вычисленным индексам.
Есть же, та же линейная комбинация, упомянутая выше, допустим Double -> BIndex i
Не говоря уже, что по всем полученным BIndex-ам доступ как положено, а таким (если не ошибаюсь) и zipper похвастаться не может.
Там будут проверки на попадание флоата в диапазон 0..1 ;)
О, да ты по ATS угорел. Ъ
Typestate и linear types уже изучил?
Лучшее от всех миров, т.сказать.
ЗЫ. Я даже не заметил элитизма в том, что я выше написал, но у всех свое мнение.
А заметил ли илитизм?
читать про ATS
Тут логика нужна а не ATS.
Судя по тому что я прочёл - кодоанализатор, тупо проверяющий что значение не выйдет за пределы, не станет нулём, итд.
Так это и сейчас компилеры с ide умеют - эклипс выдает ворнинги о " potential null pointer access", например.
Если поставишь выше assert (x!=null) или if (instance of ...) return ...;- то оно исчезнет.
Вот в том и прикол, что прога, в которой забыли поставить if, проверяющий выход индекса за границы "массива", или написали его неправильно, не тайпчекнется в ATS, и до рантайма дело даже не дойдет.
> Так это и сейчас компилеры с ide умеют
Они умеют только простейшие случаи, в которых неправильность очевидна. ATS же отвергает прогу, правильность которой он не может доказать.
Ну собственно так я и думал.
>ATS же отвергает прогу, правильность которой он не может доказать.
То есть большинство практичных случаев не скомпилится.
Бесполезный теоретический язык, на уровне Хацкила или даже выше.
Как любители борщеца и гумно в частности не дотянулись?
Как я понял в этом ихнем ATS можно отключить проверку сделав код "небезопасным".
Ну итог очевиден: как все бросают unchecked, так там все будут отключать проверки.
Большинство вменяемых случаев как раз таки скомпилится. Только вот неизвестно сколько уйдет времени на доказательство их корректности компилятору...
А если приводить доказательство в виде "a < 5, не могу объяснить, почему, но это так, мамой клянусь!", то никакой пользы от такой системы не будет.
У нас есть функция substring - туда приходят какие-то аргументы начала и конца строки. Мы их не знаем наверняка.
И что дальше?
Ок. Понятно.
>N = length(s)
Так а длина строки заранее неизвестна.
А. Я примерно понял как оно работает.
Ну разбор кода - крайне нетривиальная задача. Серъезные проекты будут компилится вечность.
Уж проще проверки вставлять.
Оно будет анализировать все циклы, которые используют счётчки-указатели в строке, которые в свою очередь обычно танцуют от нуля и аж до динамически определяемой длины строки.
И если каждый из этих счётчиков нигде не переполнится - то программа корректна.
В этом что-то есть.
БыдлоКод с "магическими числами" типа не соберется.
То есть указатель в строке, никак не привязанный динамически, в коде её длине - не пройдет.
Логично. Говно везде пролезет.
"Какой ужас, мы можем случайно выйти за границы массива" - не самая страшная проблема в ПО. Не припомню ни одного ArrayIndexOutOfBounds в написанном мной коде. Вот NPE прилично было.
?
> Основы Теории Чисел и Общая Топология
Просто нравится или как-то применяете на практике? Использую такие штуки для "расширения сознания и мышления". С практикой плоховато.
Согласен. Теория чисел - классная штука. Кстати говорят что Виноградов забил на первомайскую демонстрацию и в это время (пока никто не отвлекал административными делами, наверное) доказал тернарную гипотезу Гольдбаха.
>Просто нравится или как-то применяете на практике
Гумно, а ты почитай, поинтересуйся, кто знает, может докажешь проблему Римана.
Премию получишь, без хуёв, мамка борща наварит, будешь как король.
Напомнило
А ведь существовал миф о её неразрешимости.
Да, но сделал это не дилетант. Подобного рода проблемы решаются лишь бородатыми Перельманами, требуя много лет ежедневной целенаправленной работы. Даже самородки вроде Галуа врядли могут решить такие проблемы благодаря лишь благодаря своему необычному мышлению.
P.S. Можно было, конечно, обойтись хотя бы динамической проверкой, но насколько мне помнится, в стандартном векторе её нет-с. Обёртку свою писать?
От ошибок в логике и паршивой архитектуры не спасут даже самые умные компиляторы.