Несмотря на диковинность и некоторую отвлеченность рассматриваемой сегодня темы — надеемся, что она сможет разнообразить вам выходные. В конце поста помещаем три ссылки от автора, позволяющие познакомиться с зависимой типизацией в Idris, F# и JavaScript
Иногда создается впечатление, словно языки программирования почти не изменились с 60-х годов. Когда мне об этом говорят, я часто вспоминаю, сколько крутых инструментов и возможностей теперь есть в нашем распоряжении, и как они упрощают жизнь. Навскидку: это и интегрированные отладчики, и модульные тесты, и статические анализаторы, и крутые IDE, а также типизированные массивы и многое другое. Развитие языков – процесс долгий и поступательный, и здесь нет таких «серебряных пуль», с появлением которых развитие языков бы изменилось раз и навсегда.
Сегодня я хочу рассказать вам об одном из последних этапов в этом поступательном процессе. Технология, о которой пойдет речь, пока активно исследуется, но все указывает на то, что вскоре она укоренится в мейнстримовых языках. А начинается наша история с одной из самых фундаментальных концепций в информатике: с типов.
Мир типов
Типизация – одна из тех вещей, которые настолько неотделимы от нашего мышления, что мы едва ли даже задумываемся о концепции типов как таковой? Почему 1 – это
int, но, стоит только поместить это значение в кавычки – и оно превращается в string? Что же такое «тип», в сущности? Как это часто бывает в программировании, ответ зависит от формулировки вопроса.Типы многообразны. В некоторых системах типов существуют очень четкие границы между типами и значениями. Так, 3, 2 и 1 – это значения типа
integer, но integer – это не значение. Этот конструкт «вмурован» в язык и принципиально отличается от значения. Но, на самом деле, такое различие необязательно и может лишь ограничивать нас.Если освободить типы и превратить их в еще одну категорий значений, то открывается ряд потрясающих возможностей. Значения можно хранить, преобразовывать и передавать функциям. Таким образом, можно было бы сделать функцию, принимающую тип в качестве параметра, создавая обобщенные функции: такие, которые могут работать со множеством типов без перегрузок. Можно иметь массив значений заданного типа, а не заниматься странной арифметикой указателей и приведением типов, как приходится делать в C. Также можно собирать новые типы по ходу выполнения программы и обеспечивать такие возможности, как, например, автоматическая десериализация JSON. Но, даже если трактовать типы как значения, все равно с типами не сделаешь всего того, что можно делать со значениями. Так, оперируя экземплярами user, можно, например, сравнивать их имена, проверять их возраст или идентификатор и т.д.
if user.name == "Marin" && user.age < 65 {
print("You can't retire yet!")
}Однако, при попытке сделать то же самое с типом
User, вы могли бы сравнить только имена типов и, возможно, имена свойств. Поскольку это тип, а не экземпляр, нельзя проверить значения его свойств.if typeof(user) == User {
print("Well, it's a user. That's all I know")
}Как было бы круто, если бы у нас была функция, способная получать лишь непустой список пользователей? Либо функция, которая принимала бы адрес электронной почты, лишь если он записан в правильном формате? Для этих целей вам понадобились бы типы «непустой массив» или «адрес электронной почты». В данном случае речь идет о типе, зависящем от значения, т.е. о зависимом типе. В мейнстримовых языках подобное невозможно.
Чтобы типами можно было пользоваться, компилятор должен проверять их. Если вы утверждаете, что переменная содержит integer, то лучше бы в ней не было
string, а то компилятор станет ругаться. В принципе, это хорошо, поскольку не дает нам набажить. Проверять типы совсем просто: если функция возвращает integer, а мы пытаемся вернуть в ней "Marin", то это ошибка. Однако, с зависимыми типами все сложнее. Проблема заключается в том, когда именно компилятор проверяет типы. Как ему убедиться, что в массиве именно три значения, если программа еще даже не выполняется? Как убедиться, что целое число больше 3, если оно еще даже не присвоено? Для этого есть магия… или, иными словами, математика. Если можно математически доказать, что множество чисел всегда больше 3, то компилятор может это проверить.
Математику в студию!
Математическая индукция применяется для формулирования доказательств. Индукция позволяет безусловно подтвердить истинность некоторого утверждения. Например, мы хотим доказать, что следующая математическая формула выполняется для любого положительного числа:
1 + 2 + 3 + ... + x = x * (x + 1) / 2Существует бесконечное множество возможных x, поэтому нам потребовалось бы очень длительное время, чтобы проверить все числа вручную. К счастью, это не обязательно. Нам всего лишь нужно доказать две вещи:
- Данное утверждение соблюдается для первого числа. (Обычно это 0 или 1)
- Если данное утверждение соблюдается для числа
n, то оно будет соблюдаться и для следующего числаn + 1
Поскольку утверждение соблюдается как для первого числа, так и для всех следующих чисел, мы знаем, что оно является верным для всех возможных чисел.
Доказать это не составляет труда:
1 = 1 * (1 + 1) / 2
1 = 1Теперь мы также должны доказать, что утверждение соблюдается и для всех других чисел. Для этого предположим, что оно работает для некоторого числа n, а далее убедимся, что оно работает и для n + 1.
Предположив, что следующее выражение верно:
1 + 2 + 3 + ... + n = n * (n + 1) / 2Проверим его для
n + 1:(1 + 2 + 3 + ... + n) + (n + 1) = (n + 1) * ((n + 1) + 1) / 2Таким образом, можно заменить
"(1 + 2 + 3 + ... + n)" вышеприведенным равенством:(n * (n + 1) / 2) + (n + 1) = (n + 1) * ((n + 2) / 2)и упростить до
(n + 1) * (n/2 + 1) = (n + 1) * (n/2 + 1)Поскольку обе части выражения равны, мы убедились, что данное утверждение истинно. Это один из способов, которым можно проверять истинность утверждений, не вычисляя вручную каждый случай, и именно на базе этого принципа работают зависимые типы. Вы пишете математическое утверждение, чтобы убедиться, что тезис о типе является верным.
Красота данного подхода заключается в том, что любое математическое доказательство можно оформить в виде компьютерной программы – а именно это нам и нужно!
Вернемся к программированию
Итак, мы установили, что некоторые вещи вполне можно сначала доказать, а потом переходить к конкретным значениям. Чтобы сделать это на языке программирования, нужен способ выразить эти утверждения в коде, который будет записан в саму систему типов, то есть, систему типов требуется усовершенствовать.
Рассмотрим пример. Здесь у нас есть функция append, принимающая два массива и комбинирующая их. Как правило, сигнатура такой функции будет выглядеть примерно так:
append: (arr1: Array, arr2: Array) -> ArrayОднако, просто взглянув на сигнатуру, мы не можем быть уверены в правильности реализации. Сам тот факт, что функция возвращает массив, еще не означает, что она что-то сделала. Один из способов проверить результат – убедиться, что длина результирующего массива равна сумме длин массивов параметров.
newArray = append([1], [2, 3])
assert(length(newArray) == 3)Но зачем же проверять это во время выполнения, если можно создать ограничение, которое будет проверяться во время компиляции программы:
append: (arr1: Array, arr2: Array) -> newArray: Array
where length(newArray) == length(arr1) + length(arr2)Мы объявляем, что
append – это функция, принимающая два аргумента Array и возвращающая новый аргумент Array, который мы назвали newArray. Лишь на сей раз мы добавляем оговорку о том, что длина нового массива должна равняться сумме длин всех аргументов функции. Утверждение, имевшееся у нас выше во время выполнения, во время компиляции преобразуется в тип.Вышеприведенный код относится к миру типов, а не значений, то есть, знак
== свидетельствует о сравнении возвращаемого типа length, а не его значения. Чтобы такой механизм работал, возвращаемый тип length должен давать нам какую-либо информацию о фактическом числе.Чтобы обеспечить работу такого механизма, нужно убедиться, что каждое число относится к отдельному типу. Тип One может содержать всего одно значение: 1. То же самое касается Two, Three и всех других чисел. Естественно, такая работа очень утомительна, но именно для такой работы у нас есть программирование. Можно написать компилятор, который будет делать это за нас.
Сделав это, можно создать отдельные типы для массивов, содержащих 1, 2, 3 и другое количество элементов.
ArrayOfOne, ArrayOfTwo, т.д.Таким образом, можно определить функцию length, которая станет принимать один из вышеприведенных типов массивов и иметь зависимый возвращаемый тип
One для ArrayOfOne, Two для ArrayOfTwo и т.д. для каждого числа.Теперь, когда у нас есть отдельный тип на любую конкретную длину массива, можно убедиться (во время компиляции), что оба массива имеют равную длину. Для этого сравним их типы. А поскольку типы – это такие же значения, как и любые другие, можно назначать операции над ними. Можно определить сложение двух конкретных типов, задав, что сумма
ArrayOfOne и ArrayOfTwo равна ArrayOfThree.Вот и вся информация, требующаяся компилятору, чтобы убедиться, что написанный вами код правилен.
Допустим, мы хотим создать переменную типа
ArrayOfThree:result: ArrayOfThree = append([1], [2, 3])Компилятор может определить, что у [1] есть всего одно значение, поэтому можно присвоить тип
ArrayOfOne. Он также может присвоить ArrayOfTwo для [2, 3].Компилятор знает, что тип result должен быть равен сумме типов первого и второго аргумента. Он также знает, что ArrayOfOne+ ArrayOfTwo равно ArrayOfThree, то есть, знает, что все выражение в правой части тождества относится к типу ArrayOfThree. Оно совпадает с выражением в левой части, и компилятор доволен.
Если бы мы написали следующее:
result: ArrayOfTwo = append([1], [2, 3])то компилятор был бы совершенно недоволен, поскольку ему было бы известно, что тип неверен.
Зависимая типизация – это очень круто
В таком случае огромное количество багов допустить попросту невозможно. При зависимой типизации можно избежать ошибок на единицу, обращений к несуществующим индексам массивов, исключений нулевого указателя, бесконечных циклов и неработоспособного кода.
При помощи зависимых типов можно выразить практически что угодно. Функция факториала будет принимать только натуральные числа, функция
login не будет принимать пустых строк, функция removeLast будет принимать только непустые массивы. Причем, все это проверяется до того, как вы запустите программу.Проблема с проверками во время выполнения заключается в том, что они не удаются, если программа уже работает. Это нормально, если программа запущена только у вас, но не у пользователя. Зависимые типы позволяют вынести такие проверки на уровень типов, поэтому отказ такого рода в ходе выполнения программы становится невозможен.
Думаю, зависимая типизация – будущее мейнстримовых языков программирования, и мне уже не терпится его дождаться!
> Idris
> F*
> Добавление зависимых типов в JavaScript
Комментарии (97)
vintage
07.12.2018 17:45+1Ну, добавьте ещё ссылку на D: www.infognition.com/blog/2015/dependent_types_in_d.html
0xd34df00d
07.12.2018 18:38Я очень быстро просмотрел ту статью, но, похоже, это не совсем то: это просто вычисления на этапе компиляции. Чего для завтипов недостаточно совсем.
vintage
07.12.2018 18:55Там вычисление типов на этапе компиляции :-) Вот более наглядный пример с библиотекой единиц измерений: biozic.github.io/quantities/quantities/compiletime.html
0xd34df00d
07.12.2018 18:58Ну, это все ещё не завтипы. В зависимых типах у вас в рантайме у переменной может быть тип «если x равно 1, то Int, иначе String».
vintage
07.12.2018 19:02В статье есть пример же: «For example, we can call printCol!(Column.INTEGER, 55) and printCol!(Column.TEXT, „hi“) just fine but we cannot call printCol!(Column.TEXT, 55), this does not compile.»
0xd34df00d
07.12.2018 19:47+3Такое я вам и на C++ могу сделать.
А как насчёт чего-то вроде
printCol!(x ? Column.INTEGER : Column.TEXT, x ? 55 : "hi");, гдеxприходит по сети в рантайме?vintage
07.12.2018 20:56Такое я вам и на 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" )vintage
07.12.2018 21:08На всякий случай — зачастую проверки делаются не так топорно, а по коллекциям:
// для каждого возможного типа static foreach( ColumnType ; Column ) { // сверили рантайм и компайлтайм значения if( x == ColumnType ) { // вызвали другую функцию // передав компайлтайм и рантайм параметры dump!( ArrayOf!ColumnType )( y ); } }
0xd34df00d
08.12.2018 01:00+2Да, на C++ завтипы тоже реализуемы. Не сказал бы что так же лаконично.
Нет, нереализуемы. Уж поверьте человеку, который любит обмазаться свежими темплейтами и компилировать.
Компилятор заставит вас тем или иным способом проверить значение, после чего тип будет вполне конкретным.
Это может быть реализованным частным случаем.
Вы не так давно были в соседнем треде, и там тоже возникал этот критерий, а он хороший, на мой взгляд: как реализовать считывание массива чисел заранее неизвестной длины с последующим типобезопасным доступом по индексу к нему, где компилятор бы гарантировал, что вы не выйдете за пределы массива?
vintage
08.12.2018 12:09Уж поверьте человеку, который любит обмазаться свежими темплейтами и компилировать.
Я, конечно, уже забыл c++ как страшный сон, но как-то не очень верится человеку, который не разобравшись в языковых возможностях D, спешит убедить, что зависимые типы в нём не реализуемы. Чувствуется некая предвзятость в суждениях. Хотя мне и не понятна ваша мотивация.
как реализовать считывание массива чисел заранее неизвестной длины с последующим типобезопасным доступом по индексу к нему, где компилятор бы гарантировал, что вы не выйдете за пределы массива?
Я не очень понимаю чего вы хотите. На этапе компиляции ни индекс, ни длина массива не известна. Соответственно максимум, что тут может сделать компилятор — сгенерировать код проверки выхода за границу массива ну или заставить сделать эту рантайм проверку вручную.
Rulexec
08.12.2018 14:48+2Не нужно заставлять делать рантайм-проверки, если не используются доступы к константным индексам (иначе да, проверка обязательна). Во всех остальных случаях язык должен предоставлять возможности доказать, что все его обращения зависят от длины массива и всегда меньше её.
Чтобы если написать что-то вроде:
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 у нас бесконечно большой и никогда не переполняется, иначе придётся ещё передавать доказательства того, что правая сторона не равна максимальному значению uint.
vintage
08.12.2018 21:24Ну вот как-то так получилось: https://run.dlang.io/is/u0P4Mr
Я не стал прям всю арифметику реализовывать. Думаю хватити умножений/делений/сложений диапазонов чисел и проверки индекса массива с учётом вырезания подмассива.0xd34df00d
08.12.2018 22:23+2А какие у этого ограничения? Можно, опять же, индекс вместе с массивом из сети или из файла прочитать, скажем, и чтобы компилятор от меня потребовал проверку в рантайме? И чтобы, например, если бы я индексировался в обратном порядке от этого индекса до нуля, то проверка была ровно одна (ибо если максимальный индекс подходит, то и остальные подходят, и это можно доказать как теорему)?
Sirikid
09.12.2018 13:58Я, конечно, уже забыл c++ как страшный сон, но как-то не очень верится человеку, который не разобравшись в языковых возможностях D, спешит убедить, что зависимые типы в нём не реализуемы.
При всем уважении, маловероятно чтобы энтузиасты зависимых типов проглядели их в таком широкораспространенном языке как D.
Ilya81
08.12.2018 12:50По моему впечатлению у D достоинств много, впрочем, недостатки узнаются в процессе использования, а с D мне это не доводилось — мало под него toolkit'ов всяких, хоть UI, хоть ORM, и ещё много чего. А вот если говорить о языках программирования, что я знаю с разных сторон, например, Swift, то именно чего-то подобного мне часто не хватает. Я конечно могу влепить что-то вроде
typealais Email = String
но тогда, если объявит
var email: Email;
то никто не помещает этому свойству присвоить переменную типаString, даже если этоsomeUri.absoluteString. Наследование в этом случае не то, ибо оно, как минимум, невозможно для структур, хотя полиморфизм для этой цели вовсе не нужен.vintage
08.12.2018 13:45Так вам не алиас нужен в этом случае, а отдельный тип. Например, в D достаточно создать структуру из одного поля: https://run.dlang.io/is/TOARTZ
Ilya81
09.12.2018 10:53Структуру можно создать и в Swift, но по каждому поводу — это будет слишком громоздко. Тем более на практике обычно дело до валидации не доходит. Но для меня смысл не в валидации, а в том, чтоб, например, не спутать местами два параметра, если они оба строковые. К тому ж с отдельной структурой неудобство в том, что параметр скорее всего далее будет в составе другой структуры, а вложенные структуры тоже будут всё запутывать.
Кстати, typealais я нередко пользуюсь, особенно для внутренних типов какого-то стороннего модуля, чтоб, если его вдруг понадобится заменить, то было проще — где он используется, остаётся прежний typealais, меняется только его обхявление.
nlinker
09.12.2018 20:10+1Вам нужен аналог
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, если переданная строка не является на самом деле строкой с емейлом.
Palich239
07.12.2018 20:29В данном случае речь идет о типе, зависящем от значения, т.е. о зависимом типе. В мейнстримовых языках подобное невозможно.
Вы что-нибудь слышали о Python? Вполне себе мэйнстрим… третий язык Гугла0xd34df00d
08.12.2018 01:01+2В Python вы, вероятно, говорите о динамических типах, что немного не то.
InterceptorTSK
08.12.2018 00:48-5Автор, вы в общем то правы, и не правы) Нельзя мутить то, что вы говорите. Лютая проблема будет в оверхеде. Вы на этих ваших новых "типах" вообще далеко не уедите. И да, там где скорость не нужна — оно очень пригодится. И вот тут вы как раз таки правы. Но получается вот такая ситуация: там где надо быстро — эти ваши типы — зло. А там где надо понятно — добро, но оно будет медленное) Вывод: оставьте все как есть. Для всего свое применение. Сложить в один флакон, что бы было быстро и при этом понятно — ни у кого пока не получалось.
И да, есть вариант, когда все же это будет доступно: меняйте архитектуру процессора) Скажем так, гипотетический проц должен понимать как ооп, так и обычную функциональщину. Вот когда это будет — вот тогда в одном флаконе оно в программках будет работать без проблем.0xd34df00d
08.12.2018 01:02+2Но получается вот такая ситуация: там где надо быстро — эти ваши типы — зло.
Почему?
Про ATS вы, судя по всему, не слышали?
InterceptorTSK
09.12.2018 00:24-3Кое что слышал. А вы на нем много написали чего? Ну так, что бы работало и что бы продать.
Я еще раз напишу. Проще написать алгоритм на языке который за собой следит. И переписать на тот, который за собой вообще не следит, но при этом быстро работает.
И это как раз таки о том, что языков должно быть много. Маленькое но. Они должны быть похожими. Похожесть в том, что бы 95%, а по возможности чем больше, тем лучше — можно было перенести на уровне исходного кода из одного языка в другой.
Программируете на языке переполненным оверхеда и смотрите как пашет алгоритм. Затем банальной копипастой перекидываете в другой язык, который без оверхеда вообще.
Да, тут конечно же есть тонкие моменты. Например, условный язык А может использовать конструкции, такие, что их нет в условном языке Б. Используйте более-менее общие конструкции, так что бы код можно было перенести на уровне исходников.
И не надо говорить, что это не возможно) Более того, оно упрощает программирование на самом деле. Как ни странно, но упрощает)) И не надо говорить, что как бы вы не тужились, на том же шарпе или джаве — вы никогда банальный разархиватор даже не напишете, сравнимый по скорости с плюсами. Но вы почти запросто напишете разархиватор на шарпе, легко потестите, и перекините исходники в плюсы. Естественно убрав вообще даже любые намеки на оверхед полностью. Вот тут то оно и полетит. И да, такой код достаточно легко поддерживать, как ни странно, легко.0xd34df00d
09.12.2018 01:48+3Кое что слышал. А вы на нем много написали чего? Ну так, что бы работало и что бы продать.
Увы, конкретно на нём пока не писал, я больше по всяким упомянутым в статье идрисам. Но мой жизненный путь вообще, увы, тернист и извилист :(
И переписать на тот, который за собой вообще не следит, но при этом быстро работает.
А вы после переписывания больше к коду не возвращаетесь никогда? А то естественным образом ведь возникает вопрос поддержки того, что вы там переписали.
А если позадавать подобные вопросы дальше, получится, что лучше всего поручить преобразование из следящего языка в неследящий какой-нибудь программе. Выбрать в роли неследящего, например, С (или прям сразу язык ассемблера, или LLVM IR) и назвать эту программу компилятором.
Похожесть в том, что бы 95%, а по возможности чем больше, тем лучше — можно было перенести на уровне исходного кода из одного языка в другой.
Успехов с вещами, описанными в статье. Потому что, в частности...
И не надо говорить, что как бы вы не тужились, на том же шарпе или джаве — вы никогда банальный разархиватор даже не напишете, сравнимый по скорости с плюсами.
… не надо сравнивать с шарпом или джавой, речь не о них совсем.
vlad9486
09.12.2018 02:02+2У вас странное (неверное) убеждение что высокоуровневый подход это оверхед, а низкоуровневый — нет. Сейчас вполне себе можно писать высокоуровневый код имея производительность почти ассемблера.
И переписать на тот, который за собой вообще не следит, но при этом быстро работает.
Это не только от языка же зависит. Вам отвечают что переписывать с языка на язык — работа компилятора. Он еще и оптимизировать может, и оставляет в бинарнике ровно то что нужно (ну или почти только то в непростых случаях).
Естественно убрав вообще даже любые намеки на оверхед полностью.
И это тоже забота инструментов, а не человека. Оверхед в высокоуровневом коде неважен если в машинном его нет.InterceptorTSK
09.12.2018 05:10-5Убеждение?) Я цифрами замеряю. Чем вы замеряете — я понятия не имею. Наверное, убеждением.
И покажите мне уже высокоуровневый подход, который не имеет оверхеда) Заодно примеры приведите. Ну так что бы доказательно, а не на убеждениях.
Напишите уже на этих ваших высоких уровнях разархиватор. И как вы пишете — перепишите волшебным компилятором с языка на язык. И поглядите результаты.
Говорить можно многое, но реальность почему-то с вашими убеждениями совсем не совпадает. Никак. То что вы заявляете — вы хотя бы раз потестите.
И почему-то высоконагруженные куски вам нужные — вы реализацию этого ищете вменяемую ага? Смотрите, что бы оно было писано без оверхеда, летало и на прочие проблемы как то полное отсутствие высокоуровневости — закрываете глаза)) Ага? Да пофигу вам на это полностью, потому что надо быстро. А поделки из картона вас почему-то сразу не устраивают) Эти ваши порты, поделия на шарпе и прочий навоз. Вот почему-то сразу вас устраивать перестают. Слушайте, так это же совсем безобразие)) Вы мне впариваете какую-то тормозную фигню, но сами когда вам нужно — ею не пользуетесь) Как такое может быть вообще? Вы когда высокопроизводительную либу на плюсах писанную очередную юзать будете — всегда вспоминайте какую чушь вы тут несли) Хорошо?mayorovp
09.12.2018 11:01Убеждение?) Я цифрами замеряю.
Ну и где в ваших комментариях хоть одна цифра?
vlad9486
09.12.2018 11:51+1Я цифрами замеряю.
Где?
И покажите мне уже высокоуровневый подход, который не имеет оверхеда) Заодно примеры приведите. Ну так что бы доказательно, а не на убеждениях.
Ну вот, не видели, не значит что этого нет. Вот вам искусственный пример Посмотрите ассемблер. У нас здесь создание структур, создание и передача замыканий, вызов нескольких методов, итераторы, а на выходе 10 команд ассемблера.
А теперь давайте свои цифры.
И как вы пишете — перепишите волшебным компилятором с языка на язык.
Любой компилятор переписывает с языка на язык, это его предназначение.
Говорить можно многое, но реальность почему-то с вашими убеждениями совсем не совпадает. Никак.
И вы это очень наглядно демонстрируете.
И почему-то высоконагруженные куски вам нужные — вы реализацию этого ищете вменяемую ага?
Вы меня с кем-то путаете.
Вы мне впариваете какую-то тормозную фигню
Я еще ничего вам не парил, кроме банальных, давно известных фактов. Ваша проблема в том, что вам в глаз Java и C# попали. Это плохие примеры. Мы здесь не об этом.
всегда вспоминайте какую чушь вы тут несли
Чушь здесь только вы несете. Ну у вас и картина мира. Вы видите несколько точек: C, Java и C# они лежат на прямой, чем больше уровень абстракции, тем больше оверхеда. И вы делаете вывод, что все такие точки (ЯПы) лежат на этой же прямой. Вам говорят что это не так — не хотите слышать. Ну, как хотите.
Гуглите Zero-Cost Abstractions, короче, надеюсь на лучшее. А когда разберетесь, не забудьте вернуться в этот тред и признать свои ошибочные высказывания ошибочными.InterceptorTSK
09.12.2018 15:33-3Где?
Ну как это где?) Все что писано быстрого в этом мире, а не в параллельной вселенной — оно писано на плюсах) Достаточно цифр? Вы прямо щяс пользуетесь тысячей библиотек, написанных на плюсах, и ни одной на расте. Достаточно цифр? Покажите мне базовые вещи, каторые переписаны на раст, и оно вот прям поперло по всему миру, и из каждого утюга поют про то какой раст крутой, быстрый и удобный, и что на нем пишут кодеки, архиваторы, ворды, опирационки, браузеры и ваще все что вы видите вокруг. Достаточно цыфр или еще?) Я могу еще, скажите, я продолжу запросто.Вот вам искусственный пример
Это не пример, это называется трюкачеством. Любой компилятор имеет кучи подобных трюков в рукавах. Максимальное количество таких трюков — например в фортране. Минимальное — в шарпе. Но на самом деле — это всего лишь трюки, и к компилированию они отношения не имеют. Я ж еще раз говорю. Напишите разархиватор на расте))) Уже давно пора. Что толку от ваших искусственных примеров? И вы не понимаете простой вещи. Ну подкинули вы в раст что он обштопал и обхлопал наура. Но таких вещей он может на всем вашем коде обштопать и обхлопать всего лишь процент. А 99% кода на расте как останется тормозным унылым гавном — так им и останется) Потому что на 99% этого вашего кода трюков уже нет. Извините, но… Их нет.Ваша проблема в том, что вам в глаз Java и C# попали. Это плохие примеры. Мы здесь не об этом.
Как это не об этом? И кто такие мы? Извините, я сам по себе) Статья о том, что бы поднять флаг, и с этим флагом под бой барабанов бежать по плонете и пихать очередной никому не нужный оверхед во все щщели. Или я ошибаюсь?Чушь здесь только вы несете. Ну у вас и картина мира.
Изините, что моя картина мира вменяемая))) И я пользуюсь только быстрыми языками в продакшене)Гуглите Zero-Cost Abstractions, короче, надеюсь на лучшее.
Давайте так. Проще. На реальных примерах. А не на расте, каторый у вас.
Там где-то ниже — супер-пупер что-то типа а-ля зеро-кост, когда имя проверяют на пустоту. И да, я неверно говорю)) Потому что строку проверяют на пустоту, каторая имя.
Слушайте, вы что правда не понимаете, что это сказочное идиотство?)) Вот у вас есть строка. Ага. Строка может быть пустой. А может быть и нет. Ух ты)) Ахаха! Ну ладно. Если не пустая — а давайте проверим ее на валидные символы. Нуничоссеее… Ага ага) А первый символ же должен быть заглавной буковкой, так? Ну а как? А если имя двойное — ну значит нужно это тоже проверить. И вот такое вот убогое мышление щяс поголовно у всех)
Особо одаренные нафигачат аж пятиуровневые абстракции на это все. Понакрутят еще и абстракций функциональных, как то регулярки и прочее дерьмо.
Слушайте, этот пример ниже В МОЕЙ РЕАЛЬНОСТИ вообще не встречается))) Я не знаю зачем мне строки проверять на пустоту))) Вот понимаете, я не знаю зачем мне это) Все только потому что я отбросил нафиг оверхед абстракций. Зачем он? Он не нужен. Абсолютно.
Решение: берете базу имен, запихиваете в разряженный массив и все) Причем каждый символ в имени это шесть бит))) В случае английских имен вообще пять.
У вас вмиг исчезают всякие пятиуровневые абстракции и оверхед вместе с ними, какие-то непонятные проверки на строки и прочее дерьмо. Вы по индексу массива стразу получаете валидное имя. ВСЁ!))
И сотрите уже скюель. Уже убейте эту парашу насмерть. Ваши базы не настолько крутые, что бы в обычный массив не влезли.
И НЕ НАДО ПОСТОЯННО ИЗ РАЗА В РАЗ ПОДГРУЖАТЬ ШРИФТЫ! ЧТО ЗА БРЕД ВЫ ГОРОДИТЕ??? Вы запрашиваете в форму имена вася-петя-маша-саша. ДА УЖЕ ОТРЕНДЕРЬТЕ ЭТИ ИМЕНА ОДИН РАЗ, И СЛОЖИТЕ ИХ СПРАЙТАМИ В БИТМАП НА ВИНТ! Юзера на атоме вам огромное спасибо скажут)))
Блин, да с кем я говорю вообще… Человек на расте пишет… Извините, я пожалуй с этой темки навсегда удалюсь) Смысл отсутствует напрочь…
Вы что правда не понимаете, что вы даже не в состоянии корректно и быстро форму ввода имени написать????alhimik45
09.12.2018 16:25Там где-то ниже — супер-пупер что-то типа а-ля зеро-кост, когда имя проверяют на пустоту.
А вы значит не проверяете? Спасибо, а потом очередной Heartbleed в вашем коде находят
InterceptorTSK
09.12.2018 18:17Нет, не проверяю. Потому что я не знаю как проверить) Вы знаете? Нет.
Объясню.
Ваши проверки проверяют строки, а не имена. Вы абстракции путаете. И это нормально. Но вам нужно же проверять имена, а не строки. Это принципиальная разница, которую не улавливают.
Отсюда следует, что я не знаю что такое пустая строка в контексте имени) Имя может быть пусто? Почему нет? Все зависит от реализации же. Где то это нужно, а где-то не нужно. Проверять строки на пустоту? А что это гарантирует валидность имени? Выясняется что нет. По этому поняв что имя это вовсе не строка [ну вот так вот оно получается, я что могу поделать], и выбран принципиально иной подход. В разряженный массив закидываете ужатые имена, сразу получается список валидных имен, с доступом по индексу массива. Вы вводите в форму символы, символы битовыми сдвигами преобразуйте в индекс массива и вы получите сразу бит валидности, и имя) Поиск О(1). Проверка валидности которая на самом деле не нужна — О(1), и т.д.
Что делать с якобы пустыми строками? А ничего не делать))) Потому что вы не знаете что это. И знать не хотите. Вам зачем это нужно? Пробел — это пустое имя? А три пробела? А пустое имя корректно? Иногда да, иногда нет. От реализации зависит. Но вам до этого дела быть не должно) Ваши имена в любом случае пустыми не будут. Потому что в разряженном массиве элемент на три пробела покажет ПУСТОЕ_ИМЯ. Вы в массиве так и напишете, сами. Вот так и запишите в массиве — ПУСТОЕ_ИМЯ) Если нужно, ну там где оно нужно — запишите НЕКОРРЕКТНОЕ_ИМЯ.
И вы сразу получаете вменяемый вид данных, который однозначно можно понять. Т.е. все эти проверки строк они вообще не нужны. Вы из массива будете получать данные типа:
САША
МАША
ПУСТОЕ_ИМЯ
НЕКОРРЕКТНОЕ_ИМЯ
И вы наконец-то от строк перейдете к именам. Именно к вменяемым абстракциям. Без оверхеда. Абсолютно. Он не нужен.
А уже логику имен как абстракций — корректные они или не корректные — проверяйте как хотите. Не в потоке формы конечно же)))
В потоке формы у вас должен быть прикручен массив, по символам вводимого в поле формы вы получите абстракцию имени. Мгновенно. А уже с этими данными, т.е. уже с абстракциями имен делайте что хотите, но в другом потоке желательно.
Это все уже 20 лет назад оттестировано и работает ну я уже не знаю в скольких проектах) Абстракций как таковых минимум, а точнее две. Оверхед напрочь отсутствует. Зачем он мне?
В зависимости от формы вы можете менять логику имен, т.е. по сути нужно сменить массив готовых данных и все.VolCh
09.12.2018 18:35А если у кого-то имя ПУСТОЕ_ИМЯ? :) И вообще, база имён невозможна, по-моему, родители обычно имею право назвать ребёнка как угодно в общем случае и не везде и не всегда записи из свидетельств о рождении, паспартов, метрик или их аналогов существую в электронном виде.
InterceptorTSK
09.12.2018 19:24-1А если у кого-то имя ПУСТОЕ_ИМЯ? :)
Да оно запросто может быть) Все это слегка обговаривается в конкретной реализации с заказчиком.
Иногда заказчику вовсе и не нужно иметь весь спектр ошибок пустых полей. Выбирают себе нужные, и на основании этого пересобирается массив бд.
Более менее универсальный подход — это перед началом пользования массива бд — переписать идентификаторы ошибок под себя. Условно говоря в статическую переменную емптиНейм пихаете ПОАТИЛОРУ или что хотите, и все элементы массива с ПУСТОЕ_ИМЯ перезапишутся на новое значение.
Не придирайтесь)) Это всего лишь формальности, и они давно учтены. Только ими никто не пользуется… Нафиг оно никому не надо, такова статистика. Всех устраивает как есть.
Общее тз на эту либу аж на 15 страницах описано вообще-то) Но используется юзерами от этого всего ну максимум процентов 10% функционала.
База имен возможна. Невозможна общая база имен на всех языках, тем более с переводами. И имен не так и много. Насколько помню 15к женских и 10к мужских в русском, могу посмотреть. У нас же используется вообще где-то процентов 30% от общего корпуса. Любой корпус или почти любой все имена содержит. Даже такие о которых вы не слышали ни разу, и я тоже) Ессно все это представляет частотный словарь в разных вариациях. И конечно же редкоупотребительные имена выносятся, они ж не нужны никому. И в автозаполнении которое ну очень легко прикрутить — используется релевантность, как раз таки на частотном словаре. Цифры частот тоже вставлены в массив. Вообще, все что есть вставлено в один массив. Зачем много массивов-то?)) Это лютое зло. Дерганье готовых элементов из разных массивов всегда хуже, чем дергать сборный элемент из одного. Иногда сильно хуже по скорости. Все зависит от реализации опять же.VolCh
09.12.2018 19:34+1Что значит «не нужны никому»? Вот у человека имя в паспорте и надо его ввести. И не то, что редкоупотребимое, а уникальное.
InterceptorTSK
09.12.2018 21:59-1Ну вот так. Не нужны никому. У меня все всегда упирается в производительность и только. Если вы на семи тыщах запросов получаете готовые валидные имена из готового массива запросов имен — семьтыщпервый которого нет — роли не играет совсем.
Для этого есть очень мелкая обычная динамическая база, все при этом ага тормозит, загружаются штатные средства, персонаж с редчайшим именем гургениус отправляется туда. При этом, за этим в общем-то следим, и если гургениусы по какой-то причине поперли — ну тогда можно пересобрать статическую базу на массиве и добавить гургениуса. Впрочем, насколько я помню, за 20 лет таких случаев не было) Обычной стандартной статической базы на 7к имен хватает всем. Что-то появляется левое периодически в базах у клиентов, но этого левого — единицы в прямом смысле этого слова, опять же насколько помню, хотя тут могу ошибаться, статистику надо уточнять. И да — эта «динамическая» база — обычный текстовый файлик) Без выкрутасов. Зачем они?0xd34df00d
09.12.2018 22:25Два комментария вверх я надеялся, что вам никогда не придётся разочароваться во мне после нашей с вами совместной работы. Теперь я просто надеюсь, что мне не придётся пользоваться такими базами.
michael_vostrikov
09.12.2018 20:25+1Без оверхеда
А рассчитывать его для всех имен и в памяти хранить, эти типа не оверхед. Проход по всем символам строки с битовыми преобразованиями вместо прохода со сравнением это тоже не оверхед.
А если там только в конце пробел? Его можно убрать и получится нормальное имя, которое можно сохранить, то есть убирать пробелы все равно надо. Высчитывать индекс по 3 пробелам, чтобы их потом обрезать, это видимо тоже не оверхед.
А может вы невалидным такое имя считаете? Пусть пользователь еще раз его введет, уже без пробела, и система еще раз весь запрос обработает. Это тоже не оверхед.
А отсутствие редких имен и невозможность ввести правильное имя с диакритическими знаками на других языках это наверно вменяемая абстракция.
Так что ли? Ну-ну.
P.S.: Pablo Diego Jose Francisco de Paula Juan Nepomuceno Maria de los Remedios Cipriano de la Santisima Trinidad Ruiz y Picasso
InterceptorTSK
09.12.2018 20:55-1))))
Проход по всем символам — это сборочная либа) Вы этой либой собираете готовый код, и вставляете на уровне исходников в продакшн-либу) Копипастой)) Собираете массив и втыкиваете его ручьками в плюсную либу — абсолютно ничего хитрого.
Можно автоматизировать, а зачем? Оно пересобирается раз в год.
То что пересобирается редко — можно пересобрать и ручками.
В этой либе МАША с пробелом маппится как маша.
Пробел с МАШЕЙ тоже маппится как маша.
МА пробел ША все та же маша.
Вообще без разницы на пробелы, табы и прочую непотребщину)
Вы смысла не уловили.
Вся база в виде готового массива готового к употреблению зачитывается в оперативку целиком.
Это по-сути массив не имен, это массив всех вариантов символов, которые маппятся в ужатом виде в абстракции имен. Индекс массива — это имя, битовые данные соответствующего элемента — это все атрибуты этого имени полностью.
Оверхед на массив конечно есть, но есть ли?)
Если вы запустите то же самое на скюеле убогом — вот это будет лютый оверхед.
Мой же оверхед — это совсем так себе…
Насколько я помню что-то около 7к элементов база, это ни о чем же абсолютно.
Пустая строка в моем случае — это элемент моего массива с индексом [0], смапленная автоматом заранее в например ПУСТОЕ_ИМЯ. Все зависит от реализации.
Какие такие пустые строки мне проверять тогда? Зачем?) В продакшн-решениях этого нет и не будет никогда. У меня не будет.michael_vostrikov
09.12.2018 23:01+1Проход по всем символам — это сборочная либа
Я имею в виду проход по всем символам во введенной строке, чтобы индекс вычислить.
В этой либе МАША с пробелом маппится как маша.
Судя по "битовым операциям" завязка на правило "upper case = lower case + 0x20". А если проверка прошла, то в базу оно сохраняется в нижнем регистре или в исходном виде с пробелами? Ни то ни то не тянет на вменяемую абстракцию.
смапленная автоматом заранее в например ПУСТОЕ_ИМЯ
Зачем ее мапить, если она вообще не должна участвовать в обработке? Вы эту магическую константу потом проверяете где-то, или выводите? Строковые операции на пустом месте.
В нормальном варианте, если пустая строка, то обработка прекращается и выводится сообщение об ошибке на языке пользователя.
vlad9486
09.12.2018 21:53+2оно писано на плюсах
А где я против плюсов? Я против низкоуровневого кода, потому что там ошибки и уязвимости. А высокоуровневый код уже умеют оптимизировать очень хорошо и его можно писать на тех же плюсах, но на новых стандартах и не так как на старых плюсах. В высокоуровневом коде тоже могут быть ошибки и уязвимости, но меньше.
Тот же хром. Быстрый и современный, написанный на современных плюсах.
это называется трюкачеством
Вот с таких трюкачеств и состоят сейчас программы.
пихать очередной никому не нужный оверхед во все щщели
Давайте доказывайте что зависимые типы приносят оверхед, или прекращайте балаболить.
Оверхед приносит динамическая типизация и виртуальные машины. Зависимые типы, современный С++ и Раст не об этом, а о Zero-Cost Abstractions.
Ilya81
08.12.2018 11:18Если говорить о влиянии на производительность конечного приложения, то я не подмечал, чтоб подобные решения сильно влияли, особенно если учесть т. с. типичный уровень оптимизированности массово создаваемых приложений. На скорость компиляции влиять, конечно, может, но уж лучше пусть долго компилируется, чем искать те ж ошибки в runtime.
InterceptorTSK
08.12.2018 14:14-6А вы начните подмечать уже) Да, на кор-пятом ваше поделие не тормозит, а вот на атоме тормозит безбожно. Попробуйте) И да, ваше поделие без оверхеда, т.е. без этих ваших лишних "движняков" на атоме будет работать заметно быстрее. На это же есть кучи тестов) И кто бы что не говорил — кончный оверхед всегда будет. Убирайте его, он не нужен.
А по поводу кор-пятых, ну то что они якобы есть у всех — спешу разочаровать) Они есть условно чуть ли не у единиц. Именно ваши приложения запускаются даже на кор-пятых у единиц))) У всех остальных железо на порядок хуже.
Давайте аналогию приведу. Я собираю верстку на мобилки. Казалось бы, мой тестовый лееко кул ван выдающщий в антуту 80к ничего не могущий тилипон. Ео это не так. Потому что статистика говорит о том, что аж 79% хуже по синтетической производительности, чем выдает эта леека. Вы почти 80% людей в расчет вообще брать не будете тогда?) Выходит что так… При этом, убрав лишний оверхед, всего навсего — вы сразу увеличите производительность приложения например в два раза, и оно будет запускаться без поблем на трубках с 40к в антуту, а значит аы охватите уже 65% устройств.
Уберите лишнее и не нужное, и все будет работать) Чюдес не бывает и никогда не будет.Akon32
08.12.2018 16:18-2оверхед
Я собираю верстку на мобилки.Тогда вы должны понимать, что предпочтение сегодня отдаётся скорости разработки и надёжности, а не производительности. Никто не будет писать очередное приложение в googleplay на сях, пока производительность не оправдает вливания средств.
InterceptorTSK
08.12.2018 20:11-4Что я должен понимать? Ключевое слово тут — должен) Что и кому я должен по-вашему?)) Смотрите, вы фигачите все что можно через оверхед, и предположим, вы написали клиент клеша, ну это игра такая на мобилки. На тестовой лееке оно работает при 80к впритык. При этом, эта леека по рейтингам обгоняет 79% устройств. Т.е. этот клиент по-сути и фактически сделан для 21% устройств, и все) Те что заметно ниже рейтингом, например редми 4х при 40к в антуту — будут в два раза медленней, а оно так и есть — в два раза медленней грузить клиент, и в два раза медленней рендерить уже загруженное. Об этом же говорит фпс-метр) И играть уже становится невозможно. Прямые тесты это подтверждают. Можете и сами проверить) А теперь смотрите — фокус. Вы убираете лишнее, и на редмиках оно становится играбельно. Вы повысили производительность в два раза, а охват устройств возрос в 3.5 раза) Хотя бы раз подумайте над этим. Смысл в том, что распространенность устройств вовсе не прямая зависимость от их мощности) И да, я как вменяемый программист этим пользуюсь. Т.е. я прихожу к своим маркетологам и по тестам им так и говорю. Причем есть свои тесты, есть антуту и оно все сходится) Хотите сильно увеличить охват аудитории — значит нужно допиливать вменяемо приложение. И вы не поверите, но мне в допиле никто ни разу не отказал. Люди вовсе не являются дурачьками и бизнес вовсе не является акулой) Вы хотя бы раз объяснили внято, что то что вы делаете — можно переделать, и оно полетит? Но на это нужно время. А как иначе? Так вот с этим согласны все)) Пользователи согласны, что бы у них работало быстрее, маркетологи согласны на кратный охват, я согласен это сделать и делаю. Всем все хорошо, и только вы на это не согласны))) Слушайте, дело может быть в вас?)
И да, вам вообще никто не запрещает потестить алгоритм на джаве или шарпе и переписать его на си ))) Или у вас и с этим проблема? Ну я так и делаю вообще-то, это же удобно. Или что, в джаве-шарпе-плюсах отличаются виндпрок, коллекции и выделение памяти? Алгоритмически оно все одинаково, на ваши алгоритмы оно не влияет вообще. То что у вас работает на шарпе, именно ваше написанное — будет ровно так же работать хоть где. Какая разница-то? Только шарп следит за собой, и очень удобно тестировать алгоритмы, а плюсы не следят, но зато работают быстрее. Напишите ваш словарь на шарпе, потестите, и перепишите на плюсы, и он заработает вразы быстрее при той же алгоритмической реализации. Вы просто вкрай дубовый тяжкловесный оверхед шарпа на объекты уберете и все) И у вас все полетит.
0xd34df00d
08.12.2018 16:46+8И да, ваше поделие без оверхеда, т.е. без этих ваших лишних "движняков" на атоме будет работать заметно быстрее. На это же есть кучи тестов) И кто бы что не говорил — кончный оверхед всегда будет. Убирайте его, он не нужен.
Почему, по-вашему, статические типы приводят к рантайм-оверхеду?
Скорее, как раз наоборот: чем больше вещей вы можете доказать статически, тем меньше проверок (и вообще телодвижений в общем случае, например, по выделению памяти) вам нужно делать динамически.
А компиляторы очень сильно стараются всю неиспользуемую информацию (включая термы, используемые только в доказательствах) вырезать.
Ilya81
09.12.2018 11:05В качестве физических устройств кораздо чаще используются iPhone 6 или iPhone SE, чем iPhone X, к примеру. Так что заметно было б. Скажем, длинные действия в UI-потоке становятся заметными сразу, даже parsing, к примеру. А вот использование enum с параметром, к примеру, заметным в плане производительности не становится. Догадываюсь, что оптимизатор в компиляторе прекрасно справляется с тем, чтоб конечные инструкции процессора не влияли сильно на производительность. Скорость компиляции, как я уже говорил, при этом, конечно, не радует, причём на том самом iCore 5 в три с лишним гигагерца, но если альтернативы — ошибки в runtime — мой выбор однозначен.
vlad9486
08.12.2018 13:48Если что-то записано в исходном коде, не факт что это попадет в машинный код. Исходный код должен содержать как можно больше информации, что не мешает машинному коду содержать только то что нужно. На самом деле небольшой оверхед всегда есть, но это проблема инструментов, а не языка или подхода.
Lure_of_Chaos
08.12.2018 01:03Цена вопроса в том, что очень сложно написать реальную программу, которая работает аналогично, и при этом содержит полную информацию обо всех возможных ситуациях, не говоря об экспоненциальном росте трудоемкости поддержки и рефакторинга, учитывая то, насколько (на самом деле) стали сложны программы. Т.е. вам нужно написать всю логику с теми же тестами и 100%тпокрытием [?без возможности даже скомпилировать и запустить программу.
И мейнстримовые языки с точки зрения столь строгой типизации подобны reinterpret_cast: предполагается, что вы бог и знаете, что делаете совершенно нелогичные преобразования. И баги всецело оттого возникают, когда наши убкждения в собственной непогрешимости полностью ложные.
А отсюда и ответ на второй вопрос: почему данный подход не прижился в мейнстриме: нам гораздо важнее скорость разработки, а безбажность никому не нужна. Традиционные языки делают программирование сильно проще, чем оно есть на самом деле, позволяя сфокусироваться на логике, не расходуя нервы и силы на бюпократию, за счет каких удобно допущениях.
gitKroz
08.12.2018 04:26-2Как было бы круто, если бы у нас была функция, способная получать лишь непустой список пользователей? Либо функция, которая принимала бы адрес электронной почты, лишь если он записан в правильном формате?
Может, конечно, я не уловил суть, но в чем проблема сделать класс, который бы в конструкторе проводил указанные вами валидации, и, если валидация не проходит — бросал бы exception? А функция будет принимать в качестве аргумента объект такого класса.
Причем, все это проверяется до того, как вы запустите программу.
В мейнстримовых языках подобное невозможно.
В C++ есть static_assert, constexpr, compile-time functions, type traits. Конечно, они могут не всё, но многое.
ankh1989
08.12.2018 06:49+1А можно пример с emailом? Все эти ArrayOfThree выглядят совсем неубедительно.
ahanoff
08.12.2018 22:44+1Я думаю вам сюда: DDD в F# https://fsharpforfunandprofit.com/posts/designing-with-types-intro/
Roumed1
08.12.2018 14:38+1Мне нравится идея написания кода, который во время компиляции позволит детерминировать кучу типозовисимых событий. Но особенно интересно, на сколько вырастет\сократиться время написания такого кода?
Полно программистов, которые достаточно быстро проверяют гипотезы и достигают цели говнокодом, а за тем несколькими итерациями отладки, рефакторинга, codereview, багофиксом доводят решение до ума. (привожу в пример не небожителей, а подрастающих трудяг). Таких вырастить и использовать стоит N. Интересно, как изменится это N в реальных проектах при переходе на такой ЯП. Или как оно повлияет на процесс обучения.
s_suhanov
09.12.2018 12:02функция login не будет принимать пустых строк
Я так и не понял как на уровне компиляции отловить передачу в функцию логина пустой строки от пользователя. :(
Rulexec
09.12.2018 13:43Для этого нужна функция, которая бы принимала строку логина плюс доказательство того, что эта строка не пуста. С видом около того:
fun login(name : String, nameIsNotEmpty : Less<0, length(name)>)
Про то, как может выглядеть Less<a, b> выше приводил пример.
В итоге чтобы в коде вызвать функцию login, нам нужно туда второй параметр передать с экземпляром Less, который будет гарантировать, что name не пусто. Если попробовать передать что-то не то — не скомпилируется, ибо типы не совпадут.
Что будет требовать обязательной проверки данных, приходящих от пользователя (например, вызовом того же
isLesser(0, length(name))из примера комментария выше).khim
09.12.2018 15:23+2Передавать два параметра — это бред. Сам тип должен содержать и строки и требование непустоты.
Но это, как бы, мелочи. Сама идея выглядит разумной, но сколько лет может уйти на практическую реализацию — непонятно. STL был рождён из похожей идеи: «давайте сделаем 100500 уровней индирекции, а компилятор научим весь этот overhead убирать».
Компилятор научили более-менее убирать «вот это вот всё» примерно через 10-15 лет (примерно, потому что разные компиляторы научились «изводить» разные конструкции в разное время).
Интересно сколько здесь потребуется…kana-desu
09.12.2018 16:40ну так объедините два значения в пару, если очень так хотите.
Математически мы имеем тип
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" _) -- можем вывести пруф автоматически иногда, зависит от компилятора0xd34df00d
09.12.2018 16:42Ух ты, ещё идрис :)
А у record syntax есть возможность impliict auto поля задавать?
kana-desu
09.12.2018 17:25ну это совсм не идрис, я намешал разных синтаксисов разных языков в одном языке, это нигде не скомпилируется в таком виде.
По моему нет, мне приходится вот так писать, но я в идрисе не шарю, тутор пролистал год назад, так что моим словам верить нельзя
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"
0xd34df00d
09.12.2018 16:41Передавать два параметра — это бред. Сам тип должен содержать и строки и требование непустоты.
Ну так объедините их:
data ValidLoginName : Type where MkValidLoginName : (name : String) -> {auto prf : So (length name /= 0)} -> ValidLoginName
У типов есть всякие там принципы единственной ответственности и прочее подобное, прям как в ООП. Ну и когда вы разделяете типы, то вырезать доказательства компилятору проще.
Сама идея выглядит разумной, но сколько лет может уйти на практическую реализацию — непонятно.
Эдвин Бреди написал свой Idris практически в одиночку за вполне обозримое время.
Обе мажорных версии Agda — по факту,курсачипроекты для защиты PhD аспирантов, ЕМНИП.khim
09.12.2018 21:02Эдвин Бреди написал свой Idris практически в одиночку за вполне обозримое время.
Насколько я знаю — оно всё на уровне «proof-of-concept».
Обе мажорных версии Agda — по факту,курсачипроекты для защиты PhD аспирантов, ЕМНИП.
Вопрос ведь не идёт о том, чтобы «сделать, чтобы работало». Нужно, чтобы оно работало эффективно — а это уже куда сложнее.0xd34df00d
09.12.2018 22:31+1Насколько я знаю — оно всё на уровне «proof-of-concept».
Ну, Agda уже вполне себе используется в продакшене (там, где на такие вещи вообще смотрят и подумывают об их использовании).
Idris, гм, хрен знает. Я с ним ничего не делал, что требовало бы производительности (да и что бы требовало запускать получающийся код, в конце концов, но это так, шутеечка для самоиронии). А вот на баги там я натыкался, кстати, некоторые из которых печалят.
Хаскелевский ghc, в который уже почти завезли зависимые типы, вообще давно де-факто образец чудес, которые продвинутый компилятор может творить с ФП-кодом. Правда, собирается оно всё адски долго, стоит начать дёргать всякие там семейства типов и прочее такое. Правда, я тут на днях на C++ кое-что отрефакторил, так что теперь мой самодельный недоORM-фреймворк за меня генерирует запросы, так тот файл тоже собирается секунд 30.
Вопрос ведь не идёт о том, чтобы «сделать, чтобы работало».
А зря, такие вопросы тоже очень интересные. Потому что помимо эффективности компиляции ещё возникает вопрос эффективности процесса доказывания теорем. А там опа, оказывается, есть разные теории зависимых типов, которые имеют разные трейдоффы (потому что в наиболее общем случае тайпчекинг завтипов, очевидно, неразрешим), и по этому поводу проводится ресёрч, пишутся статьи, вот это вот всё.
Нужно, чтобы оно работало эффективно — а это уже куда сложнее.
Вы так говорите, как будто эффективная компиляция того же C++ не потребовала пары десятков лет совместной эволюции различных компиляторов и смерти 90%, если не 99% из них. Если реализовать эффективную компиляцию для всяких идрисов пусть даже настолько же сложно, то в чём вопрос? Вы ничего не теряете, так сказать, в пределе.
khim
10.12.2018 02:02Вы так говорите, как будто эффективная компиляция того же C++ не потребовала пары десятков лет совместной эволюции различных компиляторов и смерти 90%, если не 99% из них.
Вот именно после истории с C++ — я как раз очень скептически ко всем этим новинкам отношусь.
Если реализовать эффективную компиляцию для всяких идрисов пусть даже настолько же сложно, то в чём вопрос?
Вопрос, как обычно, в том можно ли этим пользоваться здесь и сейчас, как обычно.
Вы ничего не теряете, так сказать, в пределе.
Ну вот когда оный «предел» настанет — можно будет и поговорить.
Это как с тем же самым C++ и STL: оно, конечно, всё хорошо и красиво, но реально метапрограммирование на C++ стало нормой не в 90е, когда оно, формально, появилось, а в последние лет 5-7 — когда им стало возможно удобно пользоваться и компиляторы стали поддерживать его все, а не только один из 10 и то если на баги не нарвёшься.
А зря, такие вопросы тоже очень интересные.
Для разработчиков языков и библиотек для них — возможно. Но я ж их не разрабатываю. Я их пользую. И потому присматриваюсь скорее с практической точки зрения. Вот чего я могу получить и потерять перейдя на go или rust — я сейчас примерно понимаю. А вот в случае с языками с зависимыми типами — пока нет.
alhimik45
09.12.2018 15:30строку логина плюс доказательство того, что эта строка не пуста
Дак это должно быть записано в самом типе строки:
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) //скомпилируется так как типы совпали }VolCh
09.12.2018 16:01-1То есть мы получаем ограничение в виде использования императивных проверок, только понятных компилятору? Вот в даже вашем примере условие в описании типа и условие в исполняемом коде разные. Если компилятор не будет знать, что для выполнения length > 0 необходимо и достаточно, чтобы name.length != 0, то вашу конструкцию он не скомпилирует. Причём в общем случае, если String.length имеет тип integer, будет абсолютно прав.
0xd34df00d
09.12.2018 16:45Если компилятор не будет знать, что для выполнения length > 0 необходимо и достаточно, чтобы name.length != 0, то вашу конструкцию он не скомпилирует.
Так компилятору это знать не надо, если вы можете написать функцию с нужным типом и доказать это как теорему (Карри-Говард там где-то рядом).
А если
lengthимеет типInteger, а неNat, то да, он будет прав, а вы, написавшие такую функцию — нет.VolCh
09.12.2018 18:38Я-то может доказать могу, но как компилятор узнает, что я доказал, например, что int & -1 === 0 тождественно равно int === 0?
0xd34df00d
09.12.2018 22:36Зависит от того, как именно вы строите представление
intв виде битиков.
Как это делают Ъ посоны, и как и что они потом доказывают, можно посмотреть здесь, например. Из коробки тайпчекер ни про эту библиотеку, ни про эти представления ничего не знает, конечно.
alhimik45
09.12.2018 16:58Не понял, что имелось в виду под "императивных проверок"?
Вот пример из 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вывести ограничение>0VolCh
09.12.2018 18:45> Не понял, что имелось в виду под «императивных проверок»?
Строка `if(name.length == 0) return;` Match для меня выглядит такой же императивной проверкой.
> я счел само собой разумеющимся что длина будет unsigned integer
принято
> Ну а в случае с беззнаковым int тот же F* уже сейчас может после проверки на !=0 вывести ограничение >0
То есть где-то в нём захардкожено, что это одно и то же?alhimik45
09.12.2018 19:02Ну да, проверка. Сейчас всё равно в каком-то виде эти проверки пишутся для валидации. А в идеале на их основе компилятор уточняет область значений переменной, что позволит использовать менее ошибкоопасные типы, чем тот же integer для длины.
То есть где-то в нём захардкожено, что это одно и то же?
Тут он скорее работает с областью значений типа. Я вот поставил ограничение в
x:uint32{x != 5}и после проверки переменной на>10могу передать её функцию
VolCh
09.12.2018 16:06По-моему, гораздо быстрее эти типы появятся как синтаксический сахар в динамически типизированных языках.
Вопрос про пример с массивами: как быть если массив не статический, а динамический? Делать проверки в рантйме на всём множестве допустимых длин массивов для «приведения» типа «динамический массив» к «массив конкретной длины»?0xd34df00d
09.12.2018 16:46Не обязательно делать на всём множестве проверки, достаточно проверку будет сделать ровно один раз, чтобы валидировать длину массива (ну или индекс).
Почитайте при случае Type-driven development in Idris, ну или Software Foundations, но там Coq.
VolCh
09.12.2018 19:32В смысле валидировать? Вот приходит какой-то json, где может быть по какому-то пути ни одного элемента в массиве, а может быть 100500. Нам не валидировать надо а определить к какому из Array его привести.
unC0Rr
09.12.2018 21:23Это не отличается от json, в котором поле то ли строка, то ли число, и тип надо определить.
VolCh
09.12.2018 21:39Всё же есть разница в выборе между двумя типами и 100500 — два легко захардкодить, а вот писать 100500 типов ArrayZero, ArrayOne,… ArrayOneHandredThouthandsFiveHundreds несколько странновато, даже если не ручками писать а кодогенератором.
Ну и выбор типа к валидации в моём понимании никакого отношения не имеет.alhimik45
09.12.2018 22:02Зачем 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
0xd34df00d
09.12.2018 22:39Например, вы можете проверить наличие длиннейшего пути один раз, а наличие префиксов этого пути при наличии самого пути доказать статически как теорему. Тогда код, который требует более короткие пути, дополнительных проверок требовать не будет.
А, не так прочитал ваш пост сначала.
Не надо его приводить ни к какому конкретному ArrayOfN. У вас есть полноценный тип —
(n ** Array n), что можно рассматривать как логическое утверждение «существует такая пара, что её первый элемент — n, что второй элемент — массив этой длины». Зависимой парой (ну или сигма-типом) называется. И стопицот или 2^32 проверок хардкодить тоже не надо.
Похоже, распространённая ошибка людей, не имеющих большого опыта с теорией зависимых типов — рассматривать её не как математический формализм, а как какой-то, не знаю, паттерн проектирования, который без проблем влезает в темплейты C++, или в метапрограммирование на D, или что-то такое. А это не так. Вы же не пытаетесь рассматривать исчисление предикатов как паттерн внутри исчисления высказываний, хотя некоторые частные случаи работают и там, и там?
kana-desu
09.12.2018 17:12Есть такой способ "сэмулировать" зависимые типы как синглтон-типы. Синглтон типы — это типы с одним значением. В данном контексте мы имеем в виду, что если у "исходного" типа будет 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) будет ошибка типов0xd34df00d
09.12.2018 18:06Синглтоны очень быстро разваливаются, например, как только вам нужно поднять функцию на термах (хаскелевские singletons тупо темплейтхаскелем генерят соответствующую type family), или когда вам сигма-тип поднять нужно. Последнее у меня не получилось совсем.
- у нас есть синглтон типы на все значения:
DoctorMoriarty
09.12.2018 17:46Как было бы круто, если бы у нас была функция, способная получать лишь непустой список пользователей? Либо функция, которая принимала бы адрес электронной почты, лишь если он записан в правильном формате? Для этих целей вам понадобились бы типы «непустой массив» или «адрес электронной почты». (...) В мейнстримовых языках подобное невозможно.
В мейнстримовых языках никто не мешает проверять пользовательские данные и отдавать функциям/методам только прошедшие проверку.0xd34df00d
09.12.2018 18:04+2Но никто не мешает и не проверять, что и является проблемой.
DoctorMoriarty
09.12.2018 18:20Так на то и существуют best practices, которые как бы следует прививать начинающим.
alhimik45
09.12.2018 18:30+1Но когда выполнение хотя бы части этих practices гарантирует компилятор, оно как-то спокойнее.
ozkriff
09.12.2018 18:36Так разница ж принципиальная, аналогично как между написанием кода на ЯП со статической типизацией и на языке с динамической типизацией, но где мы при вызове функций в рантайме спрашиваем тип аргументов, возвращая ошибку, если нам вместо строки число передали.
VolCh
09.12.2018 19:53-1Разница принципиальная только для языков со статической типизацией. В случае языков с динамической типизации подобная система типов выглядит лишь как синтаксический сахар.
khim
Вопрос, как и везде и всегда — «сколько стоит» и «какой процент ошибки ловит»… А про это в статье — ни звука…
Есть какая-нибудь статистика?
0xd34df00d
Ошибок ловит сколько угодно — это по факту (интуиционистская) логика, поэтому все, что вы можете записать как теорему, вы можете поймать.
Стоит дорого, потому что нужно, блин, садиться и доказывать теоремы.
evocatus
Возможно, в любой программе, предназначенной для реального мира (т.е. работающей с человеческими именами, человеческим временем, человеческой бизнес-логикой) большинство типов будут сводиться к Maybe T.
0xd34df00d
Из-за человеческой лени — да, возможно. Но сами такие языки не запрещают выразить в типах практически любую спеку.
kana-desu
Или скорее всего нет, опять же, из-за человеческой лени. Работать с вездесущим Maybe неудобно, работать вообще с неправильно спроектированной моделью неудобно.
aeeneas
Интересно, что дороже: покрывать юнит-тестами или доказывать теоремы?
К тому же есть автоматизаторы типа такого http://www.esterel-technologies.com/products/scade-suite/verification-validation/scade-suite-design-verifier/.
0xd34df00d
Юнит-тесты не заменяют доказательство теорем, особенно когда теоремы про квантор всеобщности.
khim
Я, извините, спрашивал не про теоретические выкладки, а про практический опыт использования.
То, что с помощью этого инструмента можно сделать теоретически — я и сам, примерно, представляю. Мне интересны практические результаты. В идеале — сравнение с конкурентами, использовавшими обычные типы.
Halt
Есть трилогия про пи типы в Rust. Внутри RFC есть и занятные примеры практического использования.
К сожалению, Ticki ушел в академические исследования, так что похоже надежда только на Ральфа, Лодочника и К°. Но эта тема постоянно муссируется в сообществе, потому что есть потребность в дженериках, специализируемых значениями. Как минимум для нормальной обобщенной работы со статическими массивами.
А еще есть Formality, который позиционируется автором как язык, на котором можно одновременно и программировать и доказывать теоремы с использованием тех же типов. В перспективе автор планирует использовать его для написания надежных смарт-контрактов для эфира.
Это не говоря о других его удивительных свойствах, вроде отсутствия сборщика мусора и дикой эффективности свертки.