Comments 107
Есть какая-нибудь статистика?
То, что с помощью этого инструмента можно сделать теоретически — я и сам, примерно, представляю. Мне интересны практические результаты. В идеале — сравнение с конкурентами, использовавшими обычные типы.
К сожалению, Ticki ушел в академические исследования, так что похоже надежда только на Ральфа, Лодочника и К°. Но эта тема постоянно муссируется в сообществе, потому что есть потребность в дженериках, специализируемых значениями. Как минимум для нормальной обобщенной работы со статическими массивами.
А еще есть Formality, который позиционируется автором как язык, на котором можно одновременно и программировать и доказывать теоремы с использованием тех же типов. В перспективе автор планирует использовать его для написания надежных смарт-контрактов для эфира.
Это не говоря о других его удивительных свойствах, вроде отсутствия сборщика мусора и дикой эффективности свертки.
Такое я вам и на C++ могу сделать.
Да, на C++ завтипы тоже реализуемы. Не сказал бы что так же лаконично.
А как насчёт чего-то вроде printCol!(x? Column.INTEGER: Column.TEXT, x? 55: "hi");, где x приходит по сети в рантайме?
Компилятор заставит вас тем или иным способом проверить значение, после чего тип будет вполне конкретным. Что-то типа:
if( x == Column.INTEGER ) printCol!( Column.INTEGER , 55 )
if( x == Column.TEXT ) printCol!( Column.TEXT , "hi" )На всякий случай — зачастую проверки делаются не так топорно, а по коллекциям:
// для каждого возможного типа
static foreach( ColumnType ; Column ) {
// сверили рантайм и компайлтайм значения
if( x == ColumnType ) {
// вызвали другую функцию
// передав компайлтайм и рантайм параметры
dump!( ArrayOf!ColumnType )( y );
}
}Уж поверьте человеку, который любит обмазаться свежими темплейтами и компилировать.
Я, конечно, уже забыл c++ как страшный сон, но как-то не очень верится человеку, который не разобравшись в языковых возможностях D, спешит убедить, что зависимые типы в нём не реализуемы. Чувствуется некая предвзятость в суждениях. Хотя мне и не понятна ваша мотивация.
как реализовать считывание массива чисел заранее неизвестной длины с последующим типобезопасным доступом по индексу к нему, где компилятор бы гарантировал, что вы не выйдете за пределы массива?
Я не очень понимаю чего вы хотите. На этапе компиляции ни индекс, ни длина массива не известна. Соответственно максимум, что тут может сделать компилятор — сгенерировать код проверки выхода за границу массива ну или заставить сделать эту рантайм проверку вручную.
Не нужно заставлять делать рантайм-проверки, если не используются доступы к константным индексам (иначе да, проверка обязательна). Во всех остальных случаях язык должен предоставлять возможности доказать, что все его обращения зависят от длины массива и всегда меньше её.
Чтобы если написать что-то вроде:
for (int i = 0; i <= arrayLength; i++) sum += array[i];
Компилятор сказал: звучит неубедительно, i точно всегда будет меньше arrayLength? Докажи. Чего доказать нельзя, опечатка/баг пойман.
static if в шаблонах это интересно. Но недостаточно, нужно иметь возможность использовать типы с произвольными значениями, не обязательно известными на этапе компиляции.
Если статические вычисления могут изменять структуру шаблона/типы полей и выполняются на этапе компиляции, то язык определённо не может сделать такой тип:
int x = read();
Equal<x, x> eq = Equal.refl(x);И определять типы функций около таких:
int get(uint n, int[n] array, uint index, Less<index, n> less)Потому что понятия не имеет, какие значения приходят в шаблон и не может произвести над ними статических вычислений.
Для возможности что-либо доказывать, нужны типы, которые могут принимать аргументами любые типы/значения, включая неизвестные на этапе компиляции.
Например:
type Less<a:uint, b:uint>
zeroLessThanOne : Less<0, 1>
incrementBoth : Less<a, b> → Less<a + 1, b + 1>
incrementRight : Less<a, b> → Less<a, b + 1>У нас есть тип «число a меньше числа b». У него есть «конструктор» — «ноль меньше единицы». И две функции для получения всех остальных значений. Больше способов получить экземпляр Less нет. Очевидно, что для всех экземпляров этого типа выполняется a < b.
Для примера будем считать, что uint у нас бесконечно большой и никогда не переполняется, иначе придётся ещё передавать доказательства того, что правая сторона не равна максимальному значению uint.
Затем мы можем написать функцию:
isLesser : a:uint → b:uint → Maybe<Less<a, b>>Которая бы взяла Less<0, 1>, сделала Less<a, 1 + a>, если 1 + a меньше b — добила бы до Less<a, b>, иначе вернула nothing.
Затем мы можем где-то один раз получить значение Less<x, 5>, передавать его во все функции, куда передаём x и безопасно использовать x в качестве индекса по любым массивам длины больше либо равной пяти.
В идеале с зависимыми типами весь наш код требует доказательств корретности аргументов/результатов функций. При работе со значениями, известными на этапе компиляции, проверки не нужны, для неизвестных — нужна только одна.
Алгебраические типы-алиасы, способные помечать значения, чтобы нельзя было умножить скорость автомобиля на год его выпуска — это круто, но зависимые типы позволяют запрещать на порядок больше.
Ну вот как-то так получилось: https://run.dlang.io/is/u0P4Mr
Я не стал прям всю арифметику реализовывать. Думаю хватити умножений/делений/сложений диапазонов чисел и проверки индекса массива с учётом вырезания подмассива.
По моему впечатлению у D достоинств много, впрочем, недостатки узнаются в процессе использования, а с D мне это не доводилось — мало под него toolkit'ов всяких, хоть UI, хоть ORM, и ещё много чего. А вот если говорить о языках программирования, что я знаю с разных сторон, например, Swift, то именно чего-то подобного мне часто не хватает. Я конечно могу влепить что-то вроде
typealais Email = String
но тогда, если объявит
var email: Email;
то никто не помещает этому свойству присвоить переменную типа String, даже если это someUri.absoluteString. Наследование в этом случае не то, ибо оно, как минимум, невозможно для структур, хотя полиморфизм для этой цели вовсе не нужен.
Так вам не алиас нужен в этом случае, а отдельный тип. Например, в D достаточно создать структуру из одного поля: https://run.dlang.io/is/TOARTZ
Кстати, typealais я нередко пользуюсь, особенно для внутренних типов какого-то стороннего модуля, чтоб, если его вдруг понадобится заменить, то было проще — где он используется, остаётся прежний typealais, меняется только его обхявление.
Вам нужен аналог newtype из Haskell. Эта конструкция создаёт обёртку вокруг какого-то типа, которая гарантированно будет иметь представление в рантайме точно такое же, как и сам тип. При этом достигается типобезопасность.
λ> import Data.Text
λ> newtype Email = Email Text
λ> let f (x :: Email) = True -- определили простейшую функцию от Email
λ> :t f
f :: Email -> Bool
λ> f (Email "xyz") -- передать обёртку можно
True
λ> f "xyz" -- а передать сырой тип нельзя
<interactive>:43:3: error:
• No instance for (Data.String.IsString Email)Чтобы совсем достичь безопасности, нужно сделать так, чтобы экземпляры типа Email можно было строить только через какую-то функцию mkEmail :: Text -> Maybe Email которая вернёт Nothing, если переданная строка не является на самом деле строкой с емейлом.
Вы что-нибудь слышали о Python? Вполне себе мэйнстрим… третий язык Гугла
Автор, вы в общем то правы, и не правы) Нельзя мутить то, что вы говорите. Лютая проблема будет в оверхеде. Вы на этих ваших новых "типах" вообще далеко не уедите. И да, там где скорость не нужна — оно очень пригодится. И вот тут вы как раз таки правы. Но получается вот такая ситуация: там где надо быстро — эти ваши типы — зло. А там где надо понятно — добро, но оно будет медленное) Вывод: оставьте все как есть. Для всего свое применение. Сложить в один флакон, что бы было быстро и при этом понятно — ни у кого пока не получалось.
И да, есть вариант, когда все же это будет доступно: меняйте архитектуру процессора) Скажем так, гипотетический проц должен понимать как ооп, так и обычную функциональщину. Вот когда это будет — вот тогда в одном флаконе оно в программках будет работать без проблем.
Кое что слышал. А вы на нем много написали чего? Ну так, что бы работало и что бы продать.
Я еще раз напишу. Проще написать алгоритм на языке который за собой следит. И переписать на тот, который за собой вообще не следит, но при этом быстро работает.
И это как раз таки о том, что языков должно быть много. Маленькое но. Они должны быть похожими. Похожесть в том, что бы 95%, а по возможности чем больше, тем лучше — можно было перенести на уровне исходного кода из одного языка в другой.
Программируете на языке переполненным оверхеда и смотрите как пашет алгоритм. Затем банальной копипастой перекидываете в другой язык, который без оверхеда вообще.
Да, тут конечно же есть тонкие моменты. Например, условный язык А может использовать конструкции, такие, что их нет в условном языке Б. Используйте более-менее общие конструкции, так что бы код можно было перенести на уровне исходников.
И не надо говорить, что это не возможно) Более того, оно упрощает программирование на самом деле. Как ни странно, но упрощает)) И не надо говорить, что как бы вы не тужились, на том же шарпе или джаве — вы никогда банальный разархиватор даже не напишете, сравнимый по скорости с плюсами. Но вы почти запросто напишете разархиватор на шарпе, легко потестите, и перекините исходники в плюсы. Естественно убрав вообще даже любые намеки на оверхед полностью. Вот тут то оно и полетит. И да, такой код достаточно легко поддерживать, как ни странно, легко.
И переписать на тот, который за собой вообще не следит, но при этом быстро работает.Это не только от языка же зависит. Вам отвечают что переписывать с языка на язык — работа компилятора. Он еще и оптимизировать может, и оставляет в бинарнике ровно то что нужно (ну или почти только то в непростых случаях).
Естественно убрав вообще даже любые намеки на оверхед полностью.И это тоже забота инструментов, а не человека. Оверхед в высокоуровневом коде неважен если в машинном его нет.
И покажите мне уже высокоуровневый подход, который не имеет оверхеда) Заодно примеры приведите. Ну так что бы доказательно, а не на убеждениях.
Напишите уже на этих ваших высоких уровнях разархиватор. И как вы пишете — перепишите волшебным компилятором с языка на язык. И поглядите результаты.
Говорить можно многое, но реальность почему-то с вашими убеждениями совсем не совпадает. Никак. То что вы заявляете — вы хотя бы раз потестите.
И почему-то высоконагруженные куски вам нужные — вы реализацию этого ищете вменяемую ага? Смотрите, что бы оно было писано без оверхеда, летало и на прочие проблемы как то полное отсутствие высокоуровневости — закрываете глаза)) Ага? Да пофигу вам на это полностью, потому что надо быстро. А поделки из картона вас почему-то сразу не устраивают) Эти ваши порты, поделия на шарпе и прочий навоз. Вот почему-то сразу вас устраивать перестают. Слушайте, так это же совсем безобразие)) Вы мне впариваете какую-то тормозную фигню, но сами когда вам нужно — ею не пользуетесь) Как такое может быть вообще? Вы когда высокопроизводительную либу на плюсах писанную очередную юзать будете — всегда вспоминайте какую чушь вы тут несли) Хорошо?
Убеждение?) Я цифрами замеряю.
Ну и где в ваших комментариях хоть одна цифра?
Я цифрами замеряю.Где?
И покажите мне уже высокоуровневый подход, который не имеет оверхеда) Заодно примеры приведите. Ну так что бы доказательно, а не на убеждениях.Ну вот, не видели, не значит что этого нет. Вот вам искусственный пример Посмотрите ассемблер. У нас здесь создание структур, создание и передача замыканий, вызов нескольких методов, итераторы, а на выходе 10 команд ассемблера.
А теперь давайте свои цифры.
И как вы пишете — перепишите волшебным компилятором с языка на язык.Любой компилятор переписывает с языка на язык, это его предназначение.
Говорить можно многое, но реальность почему-то с вашими убеждениями совсем не совпадает. Никак.И вы это очень наглядно демонстрируете.
И почему-то высоконагруженные куски вам нужные — вы реализацию этого ищете вменяемую ага?Вы меня с кем-то путаете.
Вы мне впариваете какую-то тормозную фигнюЯ еще ничего вам не парил, кроме банальных, давно известных фактов. Ваша проблема в том, что вам в глаз Java и C# попали. Это плохие примеры. Мы здесь не об этом.
всегда вспоминайте какую чушь вы тут неслиЧушь здесь только вы несете. Ну у вас и картина мира. Вы видите несколько точек: C, Java и C# они лежат на прямой, чем больше уровень абстракции, тем больше оверхеда. И вы делаете вывод, что все такие точки (ЯПы) лежат на этой же прямой. Вам говорят что это не так — не хотите слышать. Ну, как хотите.
Гуглите Zero-Cost Abstractions, короче, надеюсь на лучшее. А когда разберетесь, не забудьте вернуться в этот тред и признать свои ошибочные высказывания ошибочными.
Где?Ну как это где?) Все что писано быстрого в этом мире, а не в параллельной вселенной — оно писано на плюсах) Достаточно цифр? Вы прямо щяс пользуетесь тысячей библиотек, написанных на плюсах, и ни одной на расте. Достаточно цифр? Покажите мне базовые вещи, каторые переписаны на раст, и оно вот прям поперло по всему миру, и из каждого утюга поют про то какой раст крутой, быстрый и удобный, и что на нем пишут кодеки, архиваторы, ворды, опирационки, браузеры и ваще все что вы видите вокруг. Достаточно цыфр или еще?) Я могу еще, скажите, я продолжу запросто.
Вот вам искусственный примерЭто не пример, это называется трюкачеством. Любой компилятор имеет кучи подобных трюков в рукавах. Максимальное количество таких трюков — например в фортране. Минимальное — в шарпе. Но на самом деле — это всего лишь трюки, и к компилированию они отношения не имеют. Я ж еще раз говорю. Напишите разархиватор на расте))) Уже давно пора. Что толку от ваших искусственных примеров? И вы не понимаете простой вещи. Ну подкинули вы в раст что он обштопал и обхлопал наура. Но таких вещей он может на всем вашем коде обштопать и обхлопать всего лишь процент. А 99% кода на расте как останется тормозным унылым гавном — так им и останется) Потому что на 99% этого вашего кода трюков уже нет. Извините, но… Их нет.
Ваша проблема в том, что вам в глаз Java и C# попали. Это плохие примеры. Мы здесь не об этом.Как это не об этом? И кто такие мы? Извините, я сам по себе) Статья о том, что бы поднять флаг, и с этим флагом под бой барабанов бежать по плонете и пихать очередной никому не нужный оверхед во все щщели. Или я ошибаюсь?
Чушь здесь только вы несете. Ну у вас и картина мира.Изините, что моя картина мира вменяемая))) И я пользуюсь только быстрыми языками в продакшене)
Гуглите Zero-Cost Abstractions, короче, надеюсь на лучшее.Давайте так. Проще. На реальных примерах. А не на расте, каторый у вас.
Там где-то ниже — супер-пупер что-то типа а-ля зеро-кост, когда имя проверяют на пустоту. И да, я неверно говорю)) Потому что строку проверяют на пустоту, каторая имя.
Слушайте, вы что правда не понимаете, что это сказочное идиотство?)) Вот у вас есть строка. Ага. Строка может быть пустой. А может быть и нет. Ух ты)) Ахаха! Ну ладно. Если не пустая — а давайте проверим ее на валидные символы. Нуничоссеее… Ага ага) А первый символ же должен быть заглавной буковкой, так? Ну а как? А если имя двойное — ну значит нужно это тоже проверить. И вот такое вот убогое мышление щяс поголовно у всех)
Особо одаренные нафигачат аж пятиуровневые абстракции на это все. Понакрутят еще и абстракций функциональных, как то регулярки и прочее дерьмо.
Слушайте, этот пример ниже В МОЕЙ РЕАЛЬНОСТИ вообще не встречается))) Я не знаю зачем мне строки проверять на пустоту))) Вот понимаете, я не знаю зачем мне это) Все только потому что я отбросил нафиг оверхед абстракций. Зачем он? Он не нужен. Абсолютно.
Решение: берете базу имен, запихиваете в разряженный массив и все) Причем каждый символ в имени это шесть бит))) В случае английских имен вообще пять.
У вас вмиг исчезают всякие пятиуровневые абстракции и оверхед вместе с ними, какие-то непонятные проверки на строки и прочее дерьмо. Вы по индексу массива стразу получаете валидное имя. ВСЁ!))
И сотрите уже скюель. Уже убейте эту парашу насмерть. Ваши базы не настолько крутые, что бы в обычный массив не влезли.
И НЕ НАДО ПОСТОЯННО ИЗ РАЗА В РАЗ ПОДГРУЖАТЬ ШРИФТЫ! ЧТО ЗА БРЕД ВЫ ГОРОДИТЕ??? Вы запрашиваете в форму имена вася-петя-маша-саша. ДА УЖЕ ОТРЕНДЕРЬТЕ ЭТИ ИМЕНА ОДИН РАЗ, И СЛОЖИТЕ ИХ СПРАЙТАМИ В БИТМАП НА ВИНТ! Юзера на атоме вам огромное спасибо скажут)))
Блин, да с кем я говорю вообще… Человек на расте пишет… Извините, я пожалуй с этой темки навсегда удалюсь) Смысл отсутствует напрочь…
Вы что правда не понимаете, что вы даже не в состоянии корректно и быстро форму ввода имени написать????
Там где-то ниже — супер-пупер что-то типа а-ля зеро-кост, когда имя проверяют на пустоту.
А вы значит не проверяете? Спасибо, а потом очередной Heartbleed в вашем коде находят
Объясню.
Ваши проверки проверяют строки, а не имена. Вы абстракции путаете. И это нормально. Но вам нужно же проверять имена, а не строки. Это принципиальная разница, которую не улавливают.
Отсюда следует, что я не знаю что такое пустая строка в контексте имени) Имя может быть пусто? Почему нет? Все зависит от реализации же. Где то это нужно, а где-то не нужно. Проверять строки на пустоту? А что это гарантирует валидность имени? Выясняется что нет. По этому поняв что имя это вовсе не строка [ну вот так вот оно получается, я что могу поделать], и выбран принципиально иной подход. В разряженный массив закидываете ужатые имена, сразу получается список валидных имен, с доступом по индексу массива. Вы вводите в форму символы, символы битовыми сдвигами преобразуйте в индекс массива и вы получите сразу бит валидности, и имя) Поиск О(1). Проверка валидности которая на самом деле не нужна — О(1), и т.д.
Что делать с якобы пустыми строками? А ничего не делать))) Потому что вы не знаете что это. И знать не хотите. Вам зачем это нужно? Пробел — это пустое имя? А три пробела? А пустое имя корректно? Иногда да, иногда нет. От реализации зависит. Но вам до этого дела быть не должно) Ваши имена в любом случае пустыми не будут. Потому что в разряженном массиве элемент на три пробела покажет ПУСТОЕ_ИМЯ. Вы в массиве так и напишете, сами. Вот так и запишите в массиве — ПУСТОЕ_ИМЯ) Если нужно, ну там где оно нужно — запишите НЕКОРРЕКТНОЕ_ИМЯ.
И вы сразу получаете вменяемый вид данных, который однозначно можно понять. Т.е. все эти проверки строк они вообще не нужны. Вы из массива будете получать данные типа:
САША
МАША
ПУСТОЕ_ИМЯ
НЕКОРРЕКТНОЕ_ИМЯ
И вы наконец-то от строк перейдете к именам. Именно к вменяемым абстракциям. Без оверхеда. Абсолютно. Он не нужен.
А уже логику имен как абстракций — корректные они или не корректные — проверяйте как хотите. Не в потоке формы конечно же)))
В потоке формы у вас должен быть прикручен массив, по символам вводимого в поле формы вы получите абстракцию имени. Мгновенно. А уже с этими данными, т.е. уже с абстракциями имен делайте что хотите, но в другом потоке желательно.
Это все уже 20 лет назад оттестировано и работает ну я уже не знаю в скольких проектах) Абстракций как таковых минимум, а точнее две. Оверхед напрочь отсутствует. Зачем он мне?
В зависимости от формы вы можете менять логику имен, т.е. по сути нужно сменить массив готовых данных и все.
А если у кого-то имя ПУСТОЕ_ИМЯ? :)Да оно запросто может быть) Все это слегка обговаривается в конкретной реализации с заказчиком.
Иногда заказчику вовсе и не нужно иметь весь спектр ошибок пустых полей. Выбирают себе нужные, и на основании этого пересобирается массив бд.
Более менее универсальный подход — это перед началом пользования массива бд — переписать идентификаторы ошибок под себя. Условно говоря в статическую переменную емптиНейм пихаете ПОАТИЛОРУ или что хотите, и все элементы массива с ПУСТОЕ_ИМЯ перезапишутся на новое значение.
Не придирайтесь)) Это всего лишь формальности, и они давно учтены. Только ими никто не пользуется… Нафиг оно никому не надо, такова статистика. Всех устраивает как есть.
Общее тз на эту либу аж на 15 страницах описано вообще-то) Но используется юзерами от этого всего ну максимум процентов 10% функционала.
База имен возможна. Невозможна общая база имен на всех языках, тем более с переводами. И имен не так и много. Насколько помню 15к женских и 10к мужских в русском, могу посмотреть. У нас же используется вообще где-то процентов 30% от общего корпуса. Любой корпус или почти любой все имена содержит. Даже такие о которых вы не слышали ни разу, и я тоже) Ессно все это представляет частотный словарь в разных вариациях. И конечно же редкоупотребительные имена выносятся, они ж не нужны никому. И в автозаполнении которое ну очень легко прикрутить — используется релевантность, как раз таки на частотном словаре. Цифры частот тоже вставлены в массив. Вообще, все что есть вставлено в один массив. Зачем много массивов-то?)) Это лютое зло. Дерганье готовых элементов из разных массивов всегда хуже, чем дергать сборный элемент из одного. Иногда сильно хуже по скорости. Все зависит от реализации опять же.
Для этого есть очень мелкая обычная динамическая база, все при этом ага тормозит, загружаются штатные средства, персонаж с редчайшим именем гургениус отправляется туда. При этом, за этим в общем-то следим, и если гургениусы по какой-то причине поперли — ну тогда можно пересобрать статическую базу на массиве и добавить гургениуса. Впрочем, насколько я помню, за 20 лет таких случаев не было) Обычной стандартной статической базы на 7к имен хватает всем. Что-то появляется левое периодически в базах у клиентов, но этого левого — единицы в прямом смысле этого слова, опять же насколько помню, хотя тут могу ошибаться, статистику надо уточнять. И да — эта «динамическая» база — обычный текстовый файлик) Без выкрутасов. Зачем они?
Без оверхеда
А рассчитывать его для всех имен и в памяти хранить, эти типа не оверхед. Проход по всем символам строки с битовыми преобразованиями вместо прохода со сравнением это тоже не оверхед.
А если там только в конце пробел? Его можно убрать и получится нормальное имя, которое можно сохранить, то есть убирать пробелы все равно надо. Высчитывать индекс по 3 пробелам, чтобы их потом обрезать, это видимо тоже не оверхед.
А может вы невалидным такое имя считаете? Пусть пользователь еще раз его введет, уже без пробела, и система еще раз весь запрос обработает. Это тоже не оверхед.
А отсутствие редких имен и невозможность ввести правильное имя с диакритическими знаками на других языках это наверно вменяемая абстракция.
Так что ли? Ну-ну.
P.S.: Pablo Diego José Francisco de Paula Juan Nepomuceno María de los Remedios Cipriano de la Santísima Trinidad Ruiz y Picasso
Проход по всем символам — это сборочная либа) Вы этой либой собираете готовый код, и вставляете на уровне исходников в продакшн-либу) Копипастой)) Собираете массив и втыкиваете его ручьками в плюсную либу — абсолютно ничего хитрого.
Можно автоматизировать, а зачем? Оно пересобирается раз в год.
То что пересобирается редко — можно пересобрать и ручками.
В этой либе МАША с пробелом маппится как маша.
Пробел с МАШЕЙ тоже маппится как маша.
МА пробел ША все та же маша.
Вообще без разницы на пробелы, табы и прочую непотребщину)
Вы смысла не уловили.
Вся база в виде готового массива готового к употреблению зачитывается в оперативку целиком.
Это по-сути массив не имен, это массив всех вариантов символов, которые маппятся в ужатом виде в абстракции имен. Индекс массива — это имя, битовые данные соответствующего элемента — это все атрибуты этого имени полностью.
Оверхед на массив конечно есть, но есть ли?)
Если вы запустите то же самое на скюеле убогом — вот это будет лютый оверхед.
Мой же оверхед — это совсем так себе…
Насколько я помню что-то около 7к элементов база, это ни о чем же абсолютно.
Пустая строка в моем случае — это элемент моего массива с индексом [0], смапленная автоматом заранее в например ПУСТОЕ_ИМЯ. Все зависит от реализации.
Какие такие пустые строки мне проверять тогда? Зачем?) В продакшн-решениях этого нет и не будет никогда. У меня не будет.
Проход по всем символам — это сборочная либа
Я имею в виду проход по всем символам во введенной строке, чтобы индекс вычислить.
В этой либе МАША с пробелом маппится как маша.
Судя по "битовым операциям" завязка на правило "upper case = lower case + 0x20". А если проверка прошла, то в базу оно сохраняется в нижнем регистре или в исходном виде с пробелами? Ни то ни то не тянет на вменяемую абстракцию.
смапленная автоматом заранее в например ПУСТОЕ_ИМЯ
Зачем ее мапить, если она вообще не должна участвовать в обработке? Вы эту магическую константу потом проверяете где-то, или выводите? Строковые операции на пустом месте.
В нормальном варианте, если пустая строка, то обработка прекращается и выводится сообщение об ошибке на языке пользователя.
оно писано на плюсахА где я против плюсов? Я против низкоуровневого кода, потому что там ошибки и уязвимости. А высокоуровневый код уже умеют оптимизировать очень хорошо и его можно писать на тех же плюсах, но на новых стандартах и не так как на старых плюсах. В высокоуровневом коде тоже могут быть ошибки и уязвимости, но меньше.
Тот же хром. Быстрый и современный, написанный на современных плюсах.
это называется трюкачествомВот с таких трюкачеств и состоят сейчас программы.
пихать очередной никому не нужный оверхед во все щщелиДавайте доказывайте что зависимые типы приносят оверхед, или прекращайте балаболить.
Оверхед приносит динамическая типизация и виртуальные машины. Зависимые типы, современный С++ и Раст не об этом, а о Zero-Cost Abstractions.
А вы начните подмечать уже) Да, на кор-пятом ваше поделие не тормозит, а вот на атоме тормозит безбожно. Попробуйте) И да, ваше поделие без оверхеда, т.е. без этих ваших лишних "движняков" на атоме будет работать заметно быстрее. На это же есть кучи тестов) И кто бы что не говорил — кончный оверхед всегда будет. Убирайте его, он не нужен.
А по поводу кор-пятых, ну то что они якобы есть у всех — спешу разочаровать) Они есть условно чуть ли не у единиц. Именно ваши приложения запускаются даже на кор-пятых у единиц))) У всех остальных железо на порядок хуже.
Давайте аналогию приведу. Я собираю верстку на мобилки. Казалось бы, мой тестовый лееко кул ван выдающщий в антуту 80к ничего не могущий тилипон. Ео это не так. Потому что статистика говорит о том, что аж 79% хуже по синтетической производительности, чем выдает эта леека. Вы почти 80% людей в расчет вообще брать не будете тогда?) Выходит что так… При этом, убрав лишний оверхед, всего навсего — вы сразу увеличите производительность приложения например в два раза, и оно будет запускаться без поблем на трубках с 40к в антуту, а значит аы охватите уже 65% устройств.
Уберите лишнее и не нужное, и все будет работать) Чюдес не бывает и никогда не будет.
оверхед
Я собираю верстку на мобилки.
Тогда вы должны понимать, что предпочтение сегодня отдаётся скорости разработки и надёжности, а не производительности. Никто не будет писать очередное приложение в googleplay на сях, пока производительность не оправдает вливания средств.
Что я должен понимать? Ключевое слово тут — должен) Что и кому я должен по-вашему?)) Смотрите, вы фигачите все что можно через оверхед, и предположим, вы написали клиент клеша, ну это игра такая на мобилки. На тестовой лееке оно работает при 80к впритык. При этом, эта леека по рейтингам обгоняет 79% устройств. Т.е. этот клиент по-сути и фактически сделан для 21% устройств, и все) Те что заметно ниже рейтингом, например редми 4х при 40к в антуту — будут в два раза медленней, а оно так и есть — в два раза медленней грузить клиент, и в два раза медленней рендерить уже загруженное. Об этом же говорит фпс-метр) И играть уже становится невозможно. Прямые тесты это подтверждают. Можете и сами проверить) А теперь смотрите — фокус. Вы убираете лишнее, и на редмиках оно становится играбельно. Вы повысили производительность в два раза, а охват устройств возрос в 3.5 раза) Хотя бы раз подумайте над этим. Смысл в том, что распространенность устройств вовсе не прямая зависимость от их мощности) И да, я как вменяемый программист этим пользуюсь. Т.е. я прихожу к своим маркетологам и по тестам им так и говорю. Причем есть свои тесты, есть антуту и оно все сходится) Хотите сильно увеличить охват аудитории — значит нужно допиливать вменяемо приложение. И вы не поверите, но мне в допиле никто ни разу не отказал. Люди вовсе не являются дурачьками и бизнес вовсе не является акулой) Вы хотя бы раз объяснили внято, что то что вы делаете — можно переделать, и оно полетит? Но на это нужно время. А как иначе? Так вот с этим согласны все)) Пользователи согласны, что бы у них работало быстрее, маркетологи согласны на кратный охват, я согласен это сделать и делаю. Всем все хорошо, и только вы на это не согласны))) Слушайте, дело может быть в вас?)
И да, вам вообще никто не запрещает потестить алгоритм на джаве или шарпе и переписать его на си ))) Или у вас и с этим проблема? Ну я так и делаю вообще-то, это же удобно. Или что, в джаве-шарпе-плюсах отличаются виндпрок, коллекции и выделение памяти? Алгоритмически оно все одинаково, на ваши алгоритмы оно не влияет вообще. То что у вас работает на шарпе, именно ваше написанное — будет ровно так же работать хоть где. Какая разница-то? Только шарп следит за собой, и очень удобно тестировать алгоритмы, а плюсы не следят, но зато работают быстрее. Напишите ваш словарь на шарпе, потестите, и перепишите на плюсы, и он заработает вразы быстрее при той же алгоритмической реализации. Вы просто вкрай дубовый тяжкловесный оверхед шарпа на объекты уберете и все) И у вас все полетит.
И мейнстримовые языки с точки зрения столь строгой типизации подобны reinterpret_cast: предполагается, что вы бог и знаете, что делаете совершенно нелогичные преобразования. И баги всецело оттого возникают, когда наши убкждения в собственной непогрешимости полностью ложные.
А отсюда и ответ на второй вопрос: почему данный подход не прижился в мейнстриме: нам гораздо важнее скорость разработки, а безбажность никому не нужна. Традиционные языки делают программирование сильно проще, чем оно есть на самом деле, позволяя сфокусироваться на логике, не расходуя нервы и силы на бюпократию, за счет каких удобно допущениях.
Как было бы круто, если бы у нас была функция, способная получать лишь непустой список пользователей? Либо функция, которая принимала бы адрес электронной почты, лишь если он записан в правильном формате?
Может, конечно, я не уловил суть, но в чем проблема сделать класс, который бы в конструкторе проводил указанные вами валидации, и, если валидация не проходит — бросал бы exception? А функция будет принимать в качестве аргумента объект такого класса.
Причем, все это проверяется до того, как вы запустите программу.
В мейнстримовых языках подобное невозможно.
В C++ есть static_assert, constexpr, compile-time functions, type traits. Конечно, они могут не всё, но многое.
Полно программистов, которые достаточно быстро проверяют гипотезы и достигают цели говнокодом, а за тем несколькими итерациями отладки, рефакторинга, codereview, багофиксом доводят решение до ума. (привожу в пример не небожителей, а подрастающих трудяг). Таких вырастить и использовать стоит N. Интересно, как изменится это N в реальных проектах при переходе на такой ЯП. Или как оно повлияет на процесс обучения.
функция login не будет принимать пустых строк
Я так и не понял как на уровне компиляции отловить передачу в функцию логина пустой строки от пользователя. :(
Для этого нужна функция, которая бы принимала строку логина плюс доказательство того, что эта строка не пуста. С видом около того:
fun login(name : String, nameIsNotEmpty : Less<0, length(name)>)Про то, как может выглядеть Less<a, b> выше приводил пример.
В итоге чтобы в коде вызвать функцию login, нам нужно туда второй параметр передать с экземпляром Less, который будет гарантировать, что name не пусто. Если попробовать передать что-то не то — не скомпилируется, ибо типы не совпадут.
Что будет требовать обязательной проверки данных, приходящих от пользователя (например, вызовом того же isLesser(0, length(name)) из примера комментария выше).
Но это, как бы, мелочи. Сама идея выглядит разумной, но сколько лет может уйти на практическую реализацию — непонятно. STL был рождён из похожей идеи: «давайте сделаем 100500 уровней индирекции, а компилятор научим весь этот overhead убирать».
Компилятор научили более-менее убирать «вот это вот всё» примерно через 10-15 лет (примерно, потому что разные компиляторы научились «изводить» разные конструкции в разное время).
Интересно сколько здесь потребуется…
ну так объедините два значения в пару, если очень так хотите.
Математически мы имеем тип
Name = { s : String | 0 < length s }выражаем его "логически"
Name = exist (s : String). 0 < length sпереводим в типы:
Name = (s : String, p : 0 < length s)часто это описывают так еще
isName s = 0 < length s
Name = (s : String) * isName sеще любят такой поинтфри
Sigma (A : Type) (B : A -> Type) = (x : A, B x)
Name = Sigma String isNameеще структуркой можно написать
record Name where
constructor MkName
value : String
proof : 0 < length value
f : Name -> String
f { value } = "Hello " <> value <> "!!!"
print $ f (MkName "kana" _) -- можем вывести пруф автоматически иногда, зависит от компиляторану это совсм не идрис, я намешал разных синтаксисов разных языков в одном языке, это нигде не скомпилируется в таком виде.
По моему нет, мне приходится вот так писать, но я в идрисе не шарю, тутор пролистал год назад, так что моим словам верить нельзя
record Name where
constructor MkName
value : String
p : LT 0 (length value)
mkName : (value : String) -> {auto p : LT 0 (length value)} -> Name
mkName value {p} = MkName value p
name : Name
name = mkName "kana"Эдвин Бреди написал свой Idris практически в одиночку за вполне обозримое время.Насколько я знаю — оно всё на уровне «proof-of-concept».
Обе мажорных версии Agda — по факту,курсачипроекты для защиты PhD аспирантов, ЕМНИП.
Вопрос ведь не идёт о том, чтобы «сделать, чтобы работало». Нужно, чтобы оно работало эффективно — а это уже куда сложнее.
Вы так говорите, как будто эффективная компиляция того же C++ не потребовала пары десятков лет совместной эволюции различных компиляторов и смерти 90%, если не 99% из них.Вот именно после истории с C++ — я как раз очень скептически ко всем этим новинкам отношусь.
Если реализовать эффективную компиляцию для всяких идрисов пусть даже настолько же сложно, то в чём вопрос?Вопрос, как обычно, в том можно ли этим пользоваться здесь и сейчас, как обычно.
Вы ничего не теряете, так сказать, в пределе.Ну вот когда оный «предел» настанет — можно будет и поговорить.
Это как с тем же самым C++ и STL: оно, конечно, всё хорошо и красиво, но реально метапрограммирование на C++ стало нормой не в 90е, когда оно, формально, появилось, а в последние лет 5-7 — когда им стало возможно удобно пользоваться и компиляторы стали поддерживать его все, а не только один из 10 и то если на баги не нарвёшься.
А зря, такие вопросы тоже очень интересные.Для разработчиков языков и библиотек для них — возможно. Но я ж их не разрабатываю. Я их пользую. И потому присматриваюсь скорее с практической точки зрения. Вот чего я могу получить и потерять перейдя на go или rust — я сейчас примерно понимаю. А вот в случае с языками с зависимыми типами — пока нет.
Собственно, как и во всех прочих приложениях.Собствено как и во всех прочих приложениях всё начинается с того, что ты смотришь на практические примеры (хотя обычно в туториалах они бывают упрощены) и прикидываешь — оно тебе нада или нет.
TDD with Idris не читали случаем?Нет. Как я уже сказал — я практик. Хочу сначала посмотреть на какой-нибудь практический проект на языке с зависимыми типами, сравнить его с тем же C++, увидеть в чём сходство, в чём отличие, какого оно получается размера, как много ловится багов и т.д. и т.п.
Когда-то вот так же я оценивал C# и Java и сделал для себя вывод, который, в общем, верен и сегодня: если вы хотите получить тормозного монстра, который жрёт ресурсы как не в себя, то «managed» языки с GC — это то, что доктор прописал. Правда с тех пор Electron дал способ потратить ресурсы ещё бездарнее… но то такое.
Вы не обязаны иметь возможность прочитать соответствующие папиры, но какой-то уровень соответствующей математической культуры вы должны иметь.Ну это само собой. Но для этого нужно потратить время и силы — а чтобы нужно что-нибудь типа Fearless Concurrency где можно было бы прочитать что-нибудь типа «мы заменили 160,000 строк C++ на 85,000 строк Rust'а и при этом получили такие-то и сякие-то выгоды».
Метаинформацию о предлагаемых усовершенстваниях — на практическом примере, а не на исскусственно сконструированном.
строку логина плюс доказательство того, что эта строка не пуста
Дак это должно быть записано в самом типе строки:
fun login(name : String(length > 0))И при вызове такой функции
//case 1
fun smth(name : String){
login(name) //не скомпилируется так как типы не совпадают
}
//case 2
fun smth(name : String){
if(name.length == 0) return; //далее тип name уже является String(length > 0)
login(name) //скомпилируется так как типы совпали
}Не понял, что имелось в виду под "императивных проверок"?
Вот пример из F*, чисто функционального языка, на который ссылка в конце статьи:
let canWrite (f:filename) = //определили ограничение для типа filename
match f with
| "demo/tempfile" -> true
| _ -> false
//можно передать только имя файла, в который точно можно писать (опустим случаи конкурентного доступа/изменения прав)
val write : f:filename{canWrite f} -> string -> ML unit
let write f s = //пишем в файл
//И дальше использование такое:
//тут может быть любой filename
val checkedWrite : filename -> string -> ML unit
let checkedWrite f s =
if canWrite f then
//а вот тут на filename компилятором навешалось ограничение
write f s
else
raise InvalidWriteесли String.length имеет тип integer, будет абсолютно прав
Да, в таком случае он, конечно, будет прав. Но мы тут типа идеальную типизацию рассматриваем и я счел само собой разумеющимся что длина будет unsigned integer, а не бессмысленным integer. Надо было мне сразу уточнить :(
Ну а в случае с беззнаковым int тот же F* уже сейчас может после проверки на !=0 вывести ограничение >0
Строка `if(name.length == 0) return;` Match для меня выглядит такой же императивной проверкой.
> я счел само собой разумеющимся что длина будет unsigned integer
принято
> Ну а в случае с беззнаковым int тот же F* уже сейчас может после проверки на !=0 вывести ограничение >0
То есть где-то в нём захардкожено, что это одно и то же?
Ну да, проверка. Сейчас всё равно в каком-то виде эти проверки пишутся для валидации. А в идеале на их основе компилятор уточняет область значений переменной, что позволит использовать менее ошибкоопасные типы, чем тот же integer для длины.
То есть где-то в нём захардкожено, что это одно и то же?
Тут он скорее работает с областью значений типа. Я вот поставил ограничение в x:uint32{x != 5} и после проверки переменной на >10 могу передать её функцию
Вопрос про пример с массивами: как быть если массив не статический, а динамический? Делать проверки в рантйме на всём множестве допустимых длин массивов для «приведения» типа «динамический массив» к «массив конкретной длины»?
Ну и выбор типа к валидации в моём понимании никакого отношения не имеет.
Зачем 100500 типов? В моём видении это должно быть как-то так (псевдокод):
class DTO {
field1: Array<int, N> // массив int'ов любой длины
field2: Array<int, N>(N > 10) // массив int'ов более десяти элементов
}И маппер из json в нашу DTO'шку воспользуется этой информацией чтобы, например, кинуть exception когда в field2 будет пустой массив (аналогично тому, как уже в текущих средствах он кинет ошибку если там число вместо массива). А если всё сматчилось, то и получится элемент типа Array<int, N> (N> 10) с каким-то N
Есть такой способ "сэмулировать" зависимые типы как синглтон-типы. Синглтон типы — это типы с одним значением. В данном контексте мы имеем в виду, что если у "исходного" типа будет N значений, то синглтон-типов будет тоже N на каждое значение. Это нужно для того, чтобы на типах полностью сохранить (продублировать) значение.
data Nat = Z | S Nat
-- generate also "kind" Nat (there are no kinds anymore) and two types Z : Nat, S : Nat -> Nat, using DataKinds
data SNat :: Nat -> Type where
SZ :: SNat Z
SS :: SNat n -> SNat (S n)
SS (SS (SZ)) :: SNat (S (S Z))и теперь можно делать примитивные зависимости. Подобный подход реализован у flow в js. По крайней мере так это выглядит. Можно представить систему типов flow как:
- у нас есть синглтон типы на все значения:
(true : true); (false : false); (2 : 2); ("hello" : "hello"); ([1, 2] : [1, 2]); - у нас есть юнионы типов (не суммы, а именно юнионы) и апкастинг к юниону от его элементов:
type bool = true | false; ((true : true) : bool); ((2 : 2) : 2 | 3) : number); // где number = 0.5 | 1 | 2| 3 | ... встроенный - есть and-тип, требущий выполнения обеих сингнатур:
(f : (true => string) & (false => number)); - и есть даункастинг в виде тайп рефайнмента:
declare function f(x: true): string;
declare function f(x: false): number;
function f(x: boolean): string | number {
if (x === true) {
(x: true);
return 'hello';
} else {
(x: false);
return 42;
}
}
const x: string = f(true);
const y: number = f(false);
// x: number = f(true) будет ошибка типов
Как было бы круто, если бы у нас была функция, способная получать лишь непустой список пользователей? Либо функция, которая принимала бы адрес электронной почты, лишь если он записан в правильном формате? Для этих целей вам понадобились бы типы «непустой массив» или «адрес электронной почты». (...) В мейнстримовых языках подобное невозможно.
В мейнстримовых языках никто не мешает проверять пользовательские данные и отдавать функциям/методам только прошедшие проверку.
То, чего вы хотите добиться, обычно делается при помощи class invariant. На практике это выражается в ассертах в конструкторе, которые не дают сконструировать класс в невалидном состоянии. Также этот класс должен быть неизменяемым(immutable). И всё – вы можете засовывать туда любые проверки, какие считаете нужным для данного типа данных.
И если хранимое таким образом значение не является сущностью(не имеет id), то этот класс называется value object(объект-значение – объект, являющийся значением). Затем из таких инвариантов можно собрать целую сущность и ей тоже можно добавить инвариантов, если нужно.
Если заинтересовал такой подход, почитайте и другие тактические паттерны DDD (Domain Driven Design)
assert в конструкторе — это замечательно, но это проверки во время исполнения. Главная проблема такого подхода — даже если вы можете гарантировать что инвариант соблюдается, вы всё равно должны его лишний раз проверить. Завтипы как раз позволяют избежать этой самой лишней проверки.
Альтернативный способ избавления от лишних проверок — внутренние "небезопасные" конструкторы, которые способны сконструировать value object в обход лишних проверок. Но тут уже возникает проблема как проверить что эти методы используются правильно. И завтипы как раз позволяют это проверить.
Так что DDD никоим образом не замена завтипам, напротив — завтипы способны значительно сократить накладные расходы в DDD.
Зависимые типы — будущее языков программирования