Как стать автором
Обновить

Комментарии 155

Толково.
Вопрос возникает часто в такой ситуации — должен ли код считать потенциально невалидными данные, которые он же сам сохраняет например в БД?
С одной стороны, я хочу условные Save(...) и Load(...) типизированные, и не думать о валидации-парсинге.
С другой, если я поменял схему БД, кто-то поправил данные в БД руками — могут полезть неожиданные баги, которых можно бы было избежать.

А можно пример? Самое близкое, что я могу придумать — это когда у нас на создание записи айди всегда не должно быть, а на апдейт всегда должен быть. К сожалению, сишарп достаточно слабоват, чтобы это выразить в одном типе, поэтому я делаю по модели на возможный сценарий. В более продвинутом языке вроде раста можно было бы обойтись перечислением:


enum Model {
    Get { id: u32, name: String },
    Create { name: String, password: String }
}

В еще более продвинутой системе можно было бы попросить компилятор такие вещи выводить:


struct Model<MId, MPassword> {
    id: MId<u32>,
    name: String,
    password: MPassword<String> 
}

...

type GetModel = Model<Id, Option>;
type CreateModel = Model<Option, Id>;

Если речь шла о чем-то другом, то просьба уточнить что имелось в виду.

В «общем» вопрос в другом — стоит ли считать БД недостоверным источником данных и парсить их так же, как описано в статье.

Ну так ORM этим и занимается в любом случае, поэтому да — стоит. В статье же был пример про Diesel. Если ORM не сможет распарсить данные в типизированную модель она выдаст ошибку.


Какой-нибудь EF даже может сказать, на сколько версий БД отличается от схемы кода, и даже автоматически её обновить. Ну или обнаружить, что кто-то руками что-то наменял, и написать в лог "тут какой-то нехороший человек в базу криво лазил".

Если вы можете получить метаданные о типах из БД, и написать конверсию в типы языка — то можно считать сами данные достоверными (т.к. у вас код начнёт ругаться на этапе конверсии метаданных, даже не дойдя до приема данных, если что-то не так).

Суть в том, что если есть возможность проверять типы — проверяйте именно их. Если нет (тот же JSON) — то увы, придётся проверять уже сами данные.

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


Хотя в контексте базы данных есть одно "но". База данных — shared-ресурс, и данные могла поменять другая программа (другая версия) с другими представлениями о жизни.


Так что IO с базой данных — это всего лишь IO со всеми втекающе-вытекающими. На самом деле споткнуться там можно и на более нетривиальных вещах. Например, кто-то поменял локаль базы данных (и не смотря на unicode) у нас I и ı — теперь одна буква. А были — разные.
(https://en.wikipedia.org/wiki/Dotted_and_dotless_I)

Ну, схему мог поменять и я сам в ходе разработки и выпуска новых версий.
И забыть написать конвертер. В идеале, я бы хотел защиту от таких проблем =)

Но да, в такой ситуации БД стоит считать недоверенным источником и работать с режиме паранойи =_=
Можно пойти дальше и валидировать данные между модулями :) Вдруг кто-то сигнатуры методов, поля объектов поменял, например?

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


abstract class Validated<T> {
    public T Value;
    public Validated(T value) {
      if (!IsValid(value)) throw new Exception("Not valid");
      Value = value;
    }
    public abstract bool IsValid(T value);
  }

  class Int42Validated : Validated<int> {
    public Int42Validated(int value) : base(value) { }
    public override bool IsValid(int value) {
      return value==42;
    }
  }

  void Foo(Int42Validated arg) { }
НЛО прилетело и опубликовало эту надпись здесь

А если так:
bool IsValid(int value) {
return value==(int)DateTime.Now.DayOfWeek;
}

НЛО прилетело и опубликовало эту надпись здесь

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

НЛО прилетело и опубликовало эту надпись здесь

Это то, что автор в статье называет "псевдо-парсер". "Псевдо" потому что вы никто не помешает написать value==547, и связь между value==42 и именем Int42Validated только у вас в голове. Это уже куда лучше чем разбросанные по коду проверки, но всё ещё можно ошибиться. И самое главное: на каждое условие не напасёшься писать такой Validated. Если у вас сотня таких Validated то писать сотню типов может быть накладно. Хотя кто-то так делает.

А кто-то помешает в head положить последний элемент, вместо первого? Как по мне, что "псевдо-парсер", что "парсер" — в сущности работают одинаково и без зав. типов дают одинаковые гарантии.

Отдельный вопрос на эту тему.
Бизнес-сущности любят менять своё состояние в зависимости от их жизненного цикла. Черновик может быть не очень валидным, сущность в работе должна быть максимально валидна, а сущность, чей жизненный цикл завершен может быть в отдельном особом состоянии. И промежуточных стадий может быть много.
Стоит ли в такой ситуации упарываться и создавать по отдельному типу на каждое состояние жизненного цикла, чтобы от проблем нас спасал компилятор и парсер, или можно таки уйти в валидации, ибо дешевле (но страдает стабильность, видимо)?

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

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


В этом плане мне нравятся языки с завтипами. Например, мы пишем функцию и хотим на этапе компиляции проверить, что мы получаем в аргументе число, но не просто число, а либо 5, либо 7, либо 12. И другая функция, которая возвращает либо 5, либо 7, и мы хотим передать её вызов в первую функцию (пример на питоне). В слабых языках нужно писать все эти IntegerFiveOrSevernOrTwelve, писать конвертер в него из IntegerFiveOrSeven и так далее. Короче — морока. А теперь приходят завтипы и говорят, что вы можете просто написать:


f : (Int n ** n `elem` [5, 9])
f = 5

g : (Int n ** n `elem` [5, 9, 12]) -> String
g _ = "123"

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

НЛО прилетело и опубликовало эту надпись здесь

Ну такая функция вроде легко пишется. А вот в общем случае сегодня в идрис чатике обсуждали — не придумали как сделать. Лучшее что вышло:


img


Нужно уже нормально взяться за учебник и нормально начать работать.

НЛО прилетело и опубликовало эту надпись здесь

Минусы такие же как и у макросов — во время компиляции начинает происходить столько магии, что теряется контроль. В теории, если все программисты пишут понятный код, dependent types как и макросы дают очень многое. Но пока программисты регулярно пишут лапшу, боюсь нам не светит повсеместное внедрение.


Подобные размышления приводят меня к тому, что текущие «простые» системы типов Java/C# уже близки к оптимуму. Нужно просто забить на идею контролировать все с помощью типов и контролировать только то, что легко.


Другое дело, если компилятор научится выводить dependent types и использовать эту информацию для оптимизации. То есть программист расставляет, по сути, подсказки в виде всех этих int, string, MyObject. А компилятор уже разбирается в том, какие реальные диапазоны значений можно в функцию передать. Тогда мы могли бы ожидать ошибки вида «эта функция принимает int, но сломается при значениях меньше 5», было бы волшебно такое иметь. Правда, что-то мне подсказывает, что такой компилятор невозможно сделать в принципе из-за проблемы останова.

НЛО прилетело и опубликовало эту надпись здесь

а что значит не разрешима из-за проблемы останова. Почему это проблема? Если компилятор не может что то разрешить он всегда может сказать программисту: прости бро но я ушёл в рекурсию на пять минут — так что иди переписывай. Или это не то?

НЛО прилетело и опубликовало эту надпись здесь
Если компилятор не может что то разрешить он всегда может сказать программисту: прости бро но я ушёл в рекурсию на пять минут — так что иди переписывай.

А как вы отличите процесс вывода типов, который ушёл в бесконечную рекурсию, от процесс вывода типов, который просто очень долго идёт? Если, скажем, давать пять минут — значит ли это, что разрешимость вывода типов должна зависеть от мощности процессора, на которой идёт вывод типов? Что делать, если вывод типов занимает 5 минут 1 секунду?

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


С тулами все сильно хуже, насколько мне известно, непонятно как это дебажить. Еще такая проблема — программисты не знают, что является хорошими практиками, а что делать не стоит. Мы еще не прошли этап «goto considered harmful» с dependent types и прочими продвинутыми штуками. Это не проблема для одного программиста, но меня как тим лида пугает перспектива делать проект на языке, настолько мощном.

Наверное, еще лет 10 и dependent types появятся в каком-то популярном языке. Как только это случится я буду первым, кто возьмет его на вооружение, а пока оставляю энтузиастам набивать шишки и находить удачные решения.
НЛО прилетело и опубликовало эту надпись здесь
Для всего нового и неизведанного, да :) и нужно допустить, что это новое не полезно. И кажется мы зацикливаемся в аргументации, я попробую резюмировать.

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

То есть нельзя получить dependent types и не получить проблем с IDE и гору кода, который только автор понимает. И все эти сложности должны меркнуть в свете получаемых преимуществ и альтернативных способов получить похожие эффекты. Тут начинается обсуждение types vs unit tests, где я опять играю ту же роль и аргументирую, что проверки в run time проще писать и отлаживать.

Только практика покажет чья точка зрения ближе к истине. Я надеюсь, что моя критика поможет энтузиастам найти решения для обозначенных, вполне практических, проблем. Проблемы — tools, debug and unit tests give me same benefits and I know how to write them.
НЛО прилетело и опубликовало эту надпись здесь
я как раз сейчас в рамках фанового проекта пилю компиляцию этих refinement types в зависимые типы

А в чем смысл? С refinement типами же удобнее работать.


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

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


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

НЛО прилетело и опубликовало эту надпись здесь
Именно в этом и смысл.

Все еще не понял, в чем. Язык refinement типов — это по сути высокоуровневая надстройка поверх языка зав. типов. Ну т.е. зав. типы вместо рефайнемент — это как руками менеджить стек и делать джампы, вместо того чтобы использовать функции.
Или писать доказательство в рамках строгого zfc-формализма, занимаясь какой-нибудь общей топологией, хз. Ну, типа, можно — но зачем?


Но зато у тех, кто способен, хотя бы будет выбор.

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


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

НЛО прилетело и опубликовало эту надпись здесь
Подобные размышления приводят меня к тому, что текущие «простые» системы типов Java/C# уже близки к оптимуму.

Пока существуют вещи типа property based testing, которые в чистом виде являются брутфорс-костылем под неполноценностью системы типов — никаким оптимумом тут и не пахнет.
Чтобы можно было выразить все интересные свойства программы в виде типов, нужны те самые Тьюринг полные dependent types. Забудем на секунду, что это сильно усложняет тулинг, типа auto complete и рефакторингов. Есть проблема с тем, как проверить что наши типы правильные? Кажется нужно будет писать что-то вроде unit тестов для самих определений типов. А тогда возникает вопрос — а есть ли профит, не напишем ли мы больше тестов на типы, чем на интересующие нас свойства программы?
Чтобы можно было выразить все интересные свойства программы в виде типов, нужны те самые Тьюринг полные dependent types.

Конечно.

Есть проблема с тем, как проверить что наши типы правильные?

Это ровно такая же проблема, как «проверить, что наши тесты правильные». Вы пишете тесты на тесты? А почему нет?

Между двумя TDD (test-driven development и type-driven development) практический выхлоп в общих чертах точно такой же, и все те аргументы, которые можно высказать за и против типов — их точно так же можно высказать за и против юнит-тестов.

Вот прям по вашему тексту: тесты усложняют тулинг, утяжеляют рефакторинг (зато делают его проведение возможным без самоубийств, ага), и неясно, как проверить, правильные ли они ¯\_(ツ)_/¯
Понятно что и типы и тесты делают проверки. Одни в compile time, другие в run time.

тесты усложняют тулинг, утяжеляют рефакторинг


Тьюринг полная система типов делает невозможным auto complete в IDE в общем случае. Также тяжело дебажить типы, юнит тесты дебажить проще. Я об этом.
Тьюринг полная система типов делает невозможным auto complete в IDE в общем случае.

К счастью, абсолютные решения на практике не нужны, если хватает и неабсолютных. Собственно, вся концепция автотестов тому подтверждение — тесты тоже «в общем случае» могут и не сработать. Ничего, все живут с этим.

Понятно что и типы и тесты делают проверки. Одни в compile time, другие в run time.

Разницы нет, процессорные циклы не деляется на compile time и run time. Проблемы в практической плоскости начинаются только тогда, когда циклов настолько мало, что рантайм выползает за нужные для задачи рамки. Но ничего, я вот например уверен, что нынешние процессоры с десятками ядер уж как-нибудь смогут обсчитывать типы для автокомплита IDE, не вешая всю систему, и убивая совсем уж выпадающие за рамки разумного (т.е. зациклившиеся) обсчеты.
Но ничего, я вот например уверен, что нынешние процессоры с десятками ядер уж как-нибудь смогут обсчитывать типы для автокомплита IDE, не вешая всю систему, и убивая совсем уж выпадающие за рамки разумного (т.е. зациклившиеся) обсчеты.


Думаю вы недооцениваете размер проблемы. Мне вспоминается C++ и бесконечные попытки сделать для него нормальную IDE. Кажется, так никто до сих пор не сделал ничего, что по удобству было бы близко к IntelliJ IDEA. Даже CLion того же производителя. Хотя могу ошибаться, CLion я уже пару лет как не трогал.
НЛО прилетело и опубликовало эту надпись здесь
НЛО прилетело и опубликовало эту надпись здесь

А почему не может быть квантора всеобщности?

НЛО прилетело и опубликовало эту надпись здесь
НЛО прилетело и опубликовало эту надпись здесь
Минусы такие же как и у макросов — во время компиляции начинает происходить столько магии, что теряется контроль. В теории, если все программисты пишут понятный код, dependent types как и макросы дают очень многое. Но пока программисты регулярно пишут лапшу, боюсь нам не светит повсеместное внедрение.

А можно уточнить, какая конкретно магия происходит во время выполнения? Когда вы строки в инты или там uuid парсите из жсона вы тоже конроль теряете? Потому что разница такая же, как в микросервисе десериализовать входные данные в структуру и просто прокидывать везде JObject, делая по-месту foo["MyBar"].ToObject<Bar>() ?? throw new Exception("Bar not found")

Если этим все ограничится, то прекрасно. Но ведь будут делать более сложные вещи, типа «а давайте ставку налога в compile time считать, ведь круто же!» или «а давайте статически доказывать, что сложность реализации этого метода не превышает log(n)», «в статус New может перевести только Админ или Support, но только если пользователя в роли Support имперсонирует пользователь в роли Admin».

Все это можно выразить в dependent types. Что-то из этого может быть имеет смысл сделать в типах, но никто не знает хорошая ли это идея. Поэтому у первых внедренцев будут проблемы.

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

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

НЛО прилетело и опубликовало эту надпись здесь

Я думаю что стоит, и обычно так и делаю. Благо в Rust это можно сделать бесплатно.

Мне немного грустно, что современная система типов не позволяет определить "непустой список" в рамках самих типов. (Интуитивно я подозреваю, что зависимые типы это позволят, но мои мозги не позволяют зависимые типы).

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


infix  4 :+:

data Vect : Nat -> Type -> Type where
   Nil  : Vect Z a
   (:+:) : a -> Vect k a -> Vect (S k) a

testFunc : (Vect n a) -> (Vect m a) -> (n = m) -> Integer
testFunc _ _ _ = 50

foo : Integer
foo = let arr = (1 :+: (2 :+: (3 :+: Nil)))
          arrWithFour = 4 :+: arr
      in testFunc arr arrWithFour Refl
НЛО прилетело и опубликовало эту надпись здесь

В тайпскрипт, оказывается, тоже можно

НЛО прилетело и опубликовало эту надпись здесь

Создайте, только, чтобы вот это так же работало:


type NonEmptyArray<T> = [T, ...T[]];

const okay: NonEmptyArray<number> = [1, 2];
const alsoOkay: NonEmptyArray<number> = [1];
const err: NonEmptyArray<number> = []; // error!

if (isNonEmptyArray(bar)) {
    needNonEmpty(bar); // okay
} else {
    needEmpty(bar); // error!! urgh, do you care?        
} 

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

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

НЛО прилетело и опубликовало эту надпись здесь
НЛО прилетело и опубликовало эту надпись здесь
Cоздайте, только, чтобы вот это так же работало:

Ой, это не также. [] — это стандартный литерал для массива в typescript а вам приходится делать что-то специальное. Часть с тайпгардом не реализована.

Нет. В Си вы сделали структуру данных со своим представлением в памяти, отличным от представления Vect.


Вы не можете, проверив что в Vect есть хотя бы один элемент, скастовать Vect в ваш NonEmptyVect так, чтобы всё заработало.


А на Typescript — можете.

НЛО прилетело и опубликовало эту надпись здесь

А тут уже потерялась информация о длине массива...

НЛО прилетело и опубликовало эту надпись здесь

Подсказка: вот это — стандартный литерал для массива.


[1, 2];

В TS вы можете стандартный массив попробовать привести этому типу.


И вот тут идет речь про стандартный массив:


if (isNonEmptyArray(bar)) {
    needNonEmpty(bar); // okay
} else {
    needEmpty(bar); // error!! urgh, do you care?        
}

Внутри If у переменной bar уточняется тип до NonEmpty а внутри else — стандартный массив

Чтобы у меня был тип "список", который не может быть пустым. NonEmptyVec — это такой костыль, слепленный из двух типов.


Условно, на воображаемом мунспике:fn foo () ->Vec<i32> where Vec<i32>.next() -> i32.


И чтобы компилятор докапывался до всех по call-стеку, требуя соответствующих гарантий.

НЛО прилетело и опубликовало эту надпись здесь
НЛО прилетело и опубликовало эту надпись здесь
НЛО прилетело и опубликовало эту надпись здесь
НЛО прилетело и опубликовало эту надпись здесь
нулевой оверхед
создавать объект NonEmptyVec и копировать в него содержимое вектора при каждой проверке на пустоту.

Потерялась логика.

Ну, вовсе не при каждой, а при первой. Зачем второй-то раз проверять на пустоту, когда уже известно, что вектор не пустой?


Но вот с тем, что про нулевой оверхед автор погорячился — соглашусь.

Ну если это делается один раз, то ладно. А если оно как-нибудь хитро в цикле должно проходиться массиву массивов? Получаем сложность N*M. Вот такой вот нулевой оверхед.

Я специально сделал некоторые упрощения для того, чтобы показать принцип. Вот вам более корректный пример:


pub struct NonEmptySlice<'a, T>(pub &'a T, pub &'a [T]);

pub fn parse_non_empty_slice<T>(slice: &[T]) -> Option<NonEmptySlice<'_, T>> {
    match slice {
        [x, ys @ ..] => Some(NonEmptySlice(x, ys)),
        [] => None
    }
}

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


Во-вторых никаких копирований там и нет, там вектор передаётся по-значению, и он не является Copy-типом. Единственная проблема там с борровчекером, про которое есть замечание в конце статьи, но и её можно победить, если не пользоваться паттерн матчингом, который в текущей версии языка только для слайсов работает, а для векторов — нет.

Во-вторых никаких копирований там и нет, там вектор передаётся по-значению, и он не является Copy-типом.

Там куча перемещений (которые для железа — те же копирования) при выполнении операции .remove(0).

Ну всегда же можно сделать по-честному, оптимизированно:


pub struct NonEmptyVec<T>(pub T, pub Vec<T>);

pub fn parse_non_empty<T>(x: Vec<T>) -> Option<NonEmptyVec<T>> {
    if x.is_empty() {
        return None;
    }
    unsafe {
        let (ptr, len, cap) = x.into_raw_parts();
        let vec = Vec::from_raw_parts(ptr.offset(1), len - 1, cap - 1);
        let first = std::ptr::read(ptr);
        Some(NonEmptyVec(first, vec))
    }
}

Ну нельзя же так делать. Когда vec попытается ваш ptr.offset(1) деаллоцировать — получится повреждение кучи...


ptr needs to have been previously allocated via String/Vec (at least, it's highly likely to be incorrect if it wasn't)

Возможно, в глубокий ансейф я не погружался. В любом случае, это просто иллюстрация того что сделать эффективный парсинг можно, и это парсинг не обязан быть дороже валидации. В языках с ГЦ такую штуку сделать можно естественно, в расте придется обмазатся ансейфом: это к слову приём который автор смарт конструктором называет, ведь компилятор тут не помогает никак. Но сделать можно, и не очень трудно. Не нравится Vec? Окей, можно сделать into_boxed_slice, у него я таких ограничений не помню.


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




Удалять из начала вектора действительно дорого, но это не должна быть частая операция, а только операция на этапе парсинга. То есть раз на запрос или типа того. Плюс есть другие способы моделировать такую вещь — например, просто хранить приватный вектор и давать на него слайсы. Типа такого:


pub struct NonEmptyVec<T>(Vec<T>);

impl<T> NonEmptyVec<T> {
    fn parse_non_empty(x: Vec<T>) -> Option<Self> {
        if x.is_empty() {
            return None;
        }
        Some(NonEmptyVec(x))
    }

    fn head(&mut self) -> &mut T {
        unsafe {
            self.0.get_unchecked_mut(0)
        }
    }

    fn tail(&mut self) -> &mut [T] {
        &mut self.0[1..]
    }
}

Не так удобно, но что ещё от низкоуровневого языка хотеть.

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

Это противоречит идее "можно парсить в несколько этапов".


Плюс есть другие способы моделировать такую вещь — например, просто хранить приватный вектор и давать на него слайсы.

Вот этот вариант мне больше нравится: он универсален и может тривиально выразить любой инвариант. Главное — не увлечься и не перемешать unsafe с бизнес-логикой.

да unsafe не особо нужен, одно лишнее сравнение можно потерпеть.

Это, конечно, здорово, но не все языки — Раст. В тех же плюсах или джаве такого нет. Мне придется либо копировать массив, чтобы быть уверенным, что он не станет пустым, либо в голове держать, что я завернул массив в NotEmptyVec, и теперь его нельзя менять. Многопоточка может превратиться в тот еще ад.

Как у вас массив станет пустым если у вас в отдельном поле лежит значение? Ну вон как выше показали. Если только вам элемент не перезатрут мусором, но тут уж никто гарантий никаких не даст. В джаве же трейдофы другие, там копировать не так дорого. Во-вторых есть персистентные структуры данных, которые не копируют. Третий вариант — моделировать иначе, как я выше показал. Четвёртый вариант — ничего не делать, а отрефакторить другой кусок, где импакт на перфоманс будет нулевым или положительным.




Статья предполагалась как рассказ о том, как систему типов можно использовать для получения гарантий корректности. Перфоманс это плюс который зачастую (но не всегда!) идет вкупе с таким подходом. Я просто смотрю на стандартную библиотеку сишарпа, тот же LINQ, там один и тот же аргумент может 20 раз на нулл провериться пока реально начнется выполнение какой-то логики. И это нифига не круто. Удаление первого элемента из непрерывной области памяти — да, дорогостоящая операция, это ситуация которую я никак не могу рассматривать как "частый кейс". Просто автор реализовал самым наивным способом, причем в хаскелле, где как раз персистентность и удалить голову ничего не стоит. Я мог бы написать эффективную реализацию, обмазавшись ансейфом, на расте, плюсах, сишарпе, джаве и десятке других языков. Вопрос, дало бы ли это что-то статье? Потому что мне кажется, что ответ отрицательный.

Как раз в плюсах и не такое есть.

fn foo(x: i32) -> Void

Возможно ли реализовать данную функцию? Очевидно, ответ на этот вопрос — нет, т.к. Void — это тип с нулём возможных значений, поэтому невозможно написать ни одной функции, возвращающей значение типа Void.

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

можно и проще:


fn foo(x: i32) -> Void {
    unimplemented!()
}

но в языках с более сложной системой типов такое написать нельзя.

Я так понимаю хаскель "языком с более сложной системой типов" не считается?

Функция может кидать исключение, оставаться в бесконечном цикле, завершать программу exit(0):
function error(message: string): never {
    throw new Error(message);
}

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

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


function error(message: string): never | bottom {
    throw new Error(message);
}

function runMe(callback: (err: Error, data: string) => never | bottom): never | bottom {
    callback(null, "Hey there!");
}

Причём в каком-нибудь ленивом хаскелле сами значения тоже функции, потому там вообще будет что-то вроде:


function runMe(callback: (err: Error | bottom, data: string | bottom) => never | bottom): never | bottom {
    callback(null, "Hey there!");
}

Не делают так, потому что оно даёт 0 выразительной мощи, а бойлерплейта куча. Всем и так понятно, что функция может никогда не завершиться, потому что это проблема останова, что любая функция может вернуть боттом.

Нет, не одно и то же. Просто боттом всегда опускается, а по законам математики 0+1=1. Поэтому never | bottom = bottom. Так что всё последовательно.


Вот небольшая занимательная арифметика на типах.

Спасибо за ссылку. У вас скорее 0 + 0 = 0 :). Вот функция a -> Void, или иными словами 0^a ни чему же не противоречит?

Мне почему-то кажется, что Void, bottom и never это и есть 0, только разными словами (плюс-минус особенности языка, которые тут нас ни к чему не обязывают).

В тайпскрипте основные свойства можно даже показать:
type T32<T> = never extends T ? true : false;  // true
type T33<T> = T extends never ? true : false;  // Deferred

В хаскеле он выражается с помощью кастылей. Но это скорее следствие тех самых особенностей, чем теоретическая необходимость. Я бы не стал возводить в абсолют.

Вот кратко в вики en.wikipedia.org/wiki/Bottom_type или популярно у Милевски в блоге bartoszmilewski.com/2015/03/13/function-types.

НЛО прилетело и опубликовало эту надпись здесь

Вообще-то, bottom как тип — это такой тип, что любой другой тип является его субтипом.


Если ⊥-тип в языке в принципе существует — он обязан быть ненаселённым типом, и с тотальностью это никак не связано.

НЛО прилетело и опубликовало эту надпись здесь

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


Так-то понятно, что если язык не тотален, то в любом типе будет ⊥-значение, и в ⊥-типе тоже.

НЛО прилетело и опубликовало эту надпись здесь

О том, входит ли ⊥-значение в тип never

Нет, это как раз 0 + 1, потому что везде в программе где написано foo :: a на самом деле написано foo :: Either a Bottom. Просто договорились не писать Either _ Bottom везде, потому что это утомительно. Боттом вполне себе значение, вы же его сами конструируете с помощью throw new Exception(), значит он населён.

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

never, в системе типов typescript, является подтипом все других типов, т.е. наименьшим элементом, т.е. это bottom по всем формальным признакам. Вы же не с этим утверждением спорите?

Насколько я понял ваши аргументы, есть проблема останова и она не решается. Теоретически это можно выразить в системе типов, введя дополнительный тип, который может быть еще «меньше». Но так ни кто не делает. В самом деле, зачем в систему типов вводить дополнительные свойства, ради задач, которые она все равно не может решить, какова польза?
Любая формальная система либо неполна, либо противоречива. Система типов это модель, которая нужна чтобы помочь программисту делать меньше ошибок (определенного класса). Она не может претендавать на абсолютную полноту и безошибочность, по определению.

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


never, в системе типов typescript, является подтипом все других типов, т.е. наименьшим элементом, т.е. это bottom по всем формальным признакам. Вы же не с этим утверждением спорите?

Я не буду спорить, потому что это ненаблюдаемая разница. Когда вы возвращаете боттом вместо числоа можно сказать, что вы вернули подтип, а можно сказат, что там было написано number | bottom, и был возвращён правый вариант. Содержательно это эквивалентные вещи.


Насколько я понял ваши аргументы, есть проблема останова и она не решается.

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

Когда вы возвращаете боттом вместо числоа можно сказать, что вы вернули подтип, а можно сказат, что там было написано number | bottom, и был возвращён правый вариант.

У Пети нет яблок, их 0. А у Маши есть одно яблоко. Можно сказать, что у Маши их 1. Но 1 = 1 + 0. Поэтому можно сказать, что Машино яблоко находится в суперпозиции существующего и отсутствующего яблока. А значит сказать однозначно сколько у Маши яблок становится проблемой. Так что-ли?

Почти, только мы всё еще знаем, что у неё одно яблоко. Потому что и в обратную сторону, 1+0 это 0. А так да, у маши столько же яблок, сколько у маши и пети. Никаких противоречий.

Спасибо, вроде сейчас стало понятно. Фича кажется полезной в частном случае:
function error(message: string) : never {
    throw new Error(message)
}

error("foo")
console.log('bar') // Unreachable code detected.

Но вот здесь тайп чекер уже не может найти ошибку:
function error(message: string) : never {
    throw new Error(message)
}

function run(test: Boolean) : number {
    if (test) {
        return error("foo")
    } else {
        return 1;
    }
}

const res: number = run(true)
console.log('bar')

Видимо потому, что сумма number|never ни чем не отличается от number, так?

Просто потому что код ричабл — существует вероятность, что вернется number, а значит следующая строчка может быть исполнена. Раз так, что подчеркивать код как unreachable компилятор не имеет права.


Видимо потому, что сумма number|never ни чем не отличается от number, так?

Так.


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


interface Foo<TErr> {
    foo(): Either<Terr, number>;
}

class ConstFoo implements Foo<never> {
 constructor (value: number,) {
  this.value = value;
 }

 foo(): Either<never, number> {
   return Ok(this.value)
 }
}

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

НЛО прилетело и опубликовало эту надпись здесь
Нет, это как раз 0 + 1, потому что везде в программе где написано foo :: a на самом деле написано foo :: Either a Bottom.

Нет, потому что a + 0 != a (для АТД не может существовать нейтрального элемента по сложению — достаточно очевидный факт), но a | 0 = a.

Плюс на уровне типов это Either, нейтральный элемент — Void, всё правильно.

Плюс на уровне типов это Either, нейтральный элемент — Void, всё правильно.

Void — это единица, т.е. тип-синглтон. А нуля (нейтрального элемента по сложению) там нет, т.к. должно быть 0 = a*0 = (a, 0). Это для ленивых пар недостижимо. Bottom — не 0.

Void в приличных языках это необитаемый тип

Это в каких? Мне ни одного не известно. Если ф-я возвращает ненаселенный тип, то эта ф-я либо виснет, либо бросает эксцепшен. Но не завершается нормально. С другой стороны — если ф-я возвращает bottom, то она обязана либо повиснуть либо бросить эксцепшен. А ф-я, которая нормально отработала, но "ничего не вернула" — это и есть ф-я, которая возвращает void, он же undefined, он же Unit, он же любой выделенный тип-синглтон в рамках конкретного соглашения.
Это на самом деле элементарно проверяется — если ф-я возвращает bottom, то тогда к результату такой ф-и можно применить любую другую ф-ю и это не будет ошибкой. НО:


function f() {
  throw new Error();
}

function g(x: number) {

}

g(f());

ошибка, т.к. f возвращает void, это тип-синглтон и он не подтип number. Нету языка в котором бы такой код тайпчекнулся, т.е. в котором результат возвращающей void ф-и можно подставить вместо аргумента любой другой.


а вот так:


function f(): never {
  throw new Error();
}

function g(x: number) {

}

g(f());

нет ошибки, т.к. never = bottom < number.
При этом:


function f(): never {

}

ожидаемо не чекается, т.к. void > never.
Вот так себя ведут ф-ю, которые возвращают чистый bottom. Совсем не так как ф-и, возвращающие void.


Either T Void изоморфен T.

Ноуп.


Цитата от Бартоша:
Это буквально x+0=x.

В Set — да, а в Hask — нет.
В Hask не существует типа 0, который бы удовлетворял x + 0 = x для любого х. Не может такой тип существовать. Потому что в категории множеств x*0 = 0, а в категории типов — нет. По-этому не существует типа, для которого Either x 0 = x при любом х. Это очевидно, на самом деле, не знаю, чего ты тупишь. Either A Bottom в Hask был бы ("бы", потому что жопо-типа в хаскеле нет, только жопо-значения) населен не только значениями Left a, но там есть еще одно значение Right bottom. Это значение в хаскеле вполне конструируется, просто делаешь f x = f x, right = Right $ f x. А потмо можно его деконструировать как Right _ — и ничего не повиснет даже.

В Set — да, а в Hask — нет.

Вся разница между сетами и хасками по большому счету — боттомы. Мне кажется, это не настолько большая разница чтобы моё утверждение стало кардинально неверным.

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

В данном случае как раз достаточно.


Я вижу у тебя небольшая каша в голове, давай я по порядку все объясню. Вот у тебя есть тип Bottom (или не есть, но допустим ты можешь его в свою систему ввести) он определяется так, чтобы соответствующий домен как множество являлся подмножеством доменов всех остальных типов.
В том случае, если у тебя например какая-то система лямбда-куба, то она не тьюринг-полна и в ней этот тип не населен. Т.е. ему в домене можно сопоставить пустое множество, т.к. множество соответствующих термов — пусто.
Если ты введешь в эти системы Bottom то все остальные типы будут включать Bottom как свое подмножество — просто потому, что любое множество содержит как подмножество пустое множество. И если ты добавишь подтипирование — Bottom будет подтипом любого типа и этот факт будет даже явно выражен в твоей системе. При этом из-за того что тип не населен ты не сможешь написать терм этого типа. Но сможешь написать терм типа, в котором Bottom сидит. Например можно будет написать терм Bottom -> Number.
Т.к. Bottom соответствует пусто множество, то Either А Bottom = А. Потому что у тебя нет в языке терма с типом Bottom и Right yoba ты написать не в состоянии. Either A Bottom состоит только из значений А (обернутых в Left).


Другое дело хаскель — в хаскеле ты можешь написать виснущий терм. Ты можешь написать терм с типом Bottom, этот Bottom населен, т.е. соответствующий данному типу домен — непуст. И мы говорим "ну раз он не пуст, то пусть он содержит некоторое значение bottom (с маленькой буквы)". Любой домен другого типа содержит Bottom и, значит, ему принадлежит bottom как значение — и Bottom подтип любого типа, если в твоей системе есть подтипирование (как в тс, например).
Но, из-за того что Bottom теперь населен, то твой a + 0 = a ломается, т.к. 0 — непустое множество, он содержит bottom как минимум. У тебя теперь есть корректный типизируемый терм bottom и терм Right bottom, который типизируется в Either A Bottom. Either A Bottom содержит лишнее значение (как минимум, одно).

НЛО прилетело и опубликовало эту надпись здесь
В хаскеле есть product и sum, но между типами нет ни какого порядка. Bottom это наименьшее значение в poset. Иными словами, для существования Bottom между типами необходимо (но не достаточно) хотя бы номинально определить отношение «меньше или равно».
Иными словами, для существования Bottom между типами необходимо (но не достаточно) хотя бы номинально определить отношение «меньше или равно».

Не между типами, а между их доменами. А между доменами оно есть.

Что вы имеете ввиду, можно пример кода?
НЛО прилетело и опубликовало эту надпись здесь
НЛО прилетело и опубликовало эту надпись здесь
Вы не знаете хаскель и идрис? Не ожидал!
Чё. Как можно ставить знак равенства между undefined, начиная от тупо синтаксически undefined: a, Unit: *?

Ну тут в общем надо уточнять, что имеется в виду, т.к. у нас есть ситуация когда ф-я корректно отработала но вроде как "ничего не вернула", есть ситуация с жопой (повисла или эксцепшон) и есть ситуация когда тип "не известен" ака "любой", т.е. это тогда не Bottom а наоборот Top. В разных языках эти штуки по-разному обозначаются и возникает путаница. Void из идриса это Bottom он же never из ts. Классический жопотип. void из тс он же void из сишки ну и вообще void из мейнстримных языков — это Unit. Ну и Top, который undefined, в тс он unknown, например.


Это если у вас арифметика на типах обязана формировать кольцо. А она обязана?

И, кстати, да, это таки выполняется: (Void, a) ≅ Void, очевидно.

Ну да, в идрисе выполняется. А в хаскеле — нет.


Это если у вас арифметика на типах обязана формировать кольцо. А она обязана?

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


В общем, если хотите быть последовательным, идите до конца: утверждайте, что в хаскеле нет типов-сумм и типов-произведений.

Хаскель с seq вообще не категория. кек. Что до произведений и сумм — там вроде фиксится определение, ничего не лмоая.


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

НЛО прилетело и опубликовало эту надпись здесь
Эм, почему это undefined?

Ну а что он?


Поэтому можно обсуждать первые боттомы модуло вторые

Конечно же, нельзя. Это вопрос корректности модели. Мы можем обсуждать хаскель модуло боттомы до тех пор, пока наши рассуждения верны — т.е. ровно до тех пор, пока они боттомов не касаются. Но как только они конкретно боттомов (или ситуаций, на которые влияют боттомы) начинают касаться — мы так поступать не имеем права.


Ну это как — пока вы рассуждаете о скорости движения своего автомобиля относительно мимо идущего пешехода, то можете игнорировать поправки СТО. И будете получать хорошие, годные результаты. Но если у вас скорости, сравнимые с световыми — уже не можете. Т.к. в этом случае вы получите чепуху.


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

Either T Void != T, это два разных типа.

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

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

Довольно типичная проблема при рефакторингах.
Было:
function error(message: string) : void {
   console.log(message)
}

runMe((err: string, data: string) => { 
  err ? error(err) : console.log(data)
  console.log("complete");
})

Стало:
function error(message: string) : never {
   console.log(message)
   process.exit(1)
}
...


Ведь здорово, когда за такое можно получить по шапке не в рантайме, а еще на этапе кодинга?

Здорово, но эта проблема останова, и она в принципе не решается. Есть языки типа идриса, которые пытаются её решить. но за это вы платите тем, что вам приходится переписывать валидный код так, чтобы компилятор смог удостовериться что всё в порядке. Можете зайти в чат растовиков, послушать как они "удовлетваоряют" борровчекер, ведь код правильный, а борровчекер не пускает. То же самое — есть некоторые гарантии, которые компилятор проверяет, за это расплачиваешься тем, что нужно подстраивать код под его правила, даже если ничего плохого этот код не делает. До банального: поменял две независимые строчки местами — код начал работать.


Такова жизнь.

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

В том, что программист может ошибаться. Понятное дело, что в любом системе типов есть форточка: без аксиом трудно жить. Это ансейфы всевозможных видом, trustme и прочее. Попытка выйти в такую форточку может закончиться плачевно. Поэтому обычно люди переписывают так, чтобы укладываться в систему типов, а не курочат всё в угоду своим представлениям. Что получается, когда они делают по второму сценарию можно посмотреть на примере драмы с актиксом.

НЛО прилетело и опубликовало эту надпись здесь
В typescript для таких функций есть отдельный тип never, например

Ну это и есть Never, просто его можно руками объявить.

Там ниже есть замечание про "хаки" в виде эксепшнов, и вообще речь про тотальную реализацию. Если вы пишете int Foo() { throw new Exception() } то эксепшн не является валидным значением типа int и программа не может продолжать свою обычную работу. Функция эффективно не вычислилась, потому что мы не получили результат, Или, говоря формально, функция вернула боттом. Но боттом может вернуть любая функция любой сигнатуры (кроме специальных языков, которые не тьюринг-полные), поэтому говорить о них немного неинтересно. Неплохая статья на тему.

let head = xs.remove(0);

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

  1. пример переписан с хаскелля где список — это скорее итератор. Удаление первого элемента итератора, как нетрудно догадаться, не проблема.
  2. я мог бы переделать всё на итераторы, но обмазываться тучей impl Iterator<Item=T> и генериков ради этого счёл нецелесообразным.

В качестве примера годится, спасибо. Я больше думал что оставить под капотом Vec просто сделать к нему api который будет гарантировать что вектор не пустой.

Это подход который автор называет "псевдовалидатором". Он даёт больше гарантий, чем разбросанные по коду проверки, но всё еще не валидируется компилятор. а полагается на ваш "здравый смысл" при реализации такой обёртки.

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


Upd: да уже обсудили это в комментах выше, я не внимательно их прочитал https://habr.com/ru/post/498042/#comment_21519322

Спасибо, давно пользуюсь подобными штуками в Расте. Правда NonEmptyVec можно реализовать и проще, скажем так:


pub struct NonEmptyVec<T>(Vec<T>);

impl<T> NonEmptyVec<T> {
    pub fn head(&self) -> &T {
        unsafe { self.0.get_unchecked(0) }
    }
}

impl<T> TryFrom<Vec<T>> for NonEmptyVec<T> {
    type Error = &'static str;

    fn try_from(vec: Vec<T>) -> Result<Self, Self::Error> {
        if vec.is_empty() {
            Err("NonEmptyVec only accepts non empty vec!")
        } else {
            Ok(NonEmptyVec(vec))
        }
    }
}

Запустить


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

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


А добавить функций, а потом ещё функций, а потом ещё функций, чтобы где-то случайно пролезла любая мутабельная история — можно очень просто. В данном случае тут 0 помощи от системы типов, и недаром пришлось писать unsafe — потому что это информация в голове программиста, про которую компилятор не знает ничего.


Но это лучше, чем ничего, с этим никто не спорит.

как я же уже говорил unsafe не обязателен, пусть будет паника.
Зато можно прокинуть все не мутабельные методы через Deref и будут сразу и итераторы и слайсы и всё остальное, а если голова лежит отдельно то iter() надо отдельно писать, а слайс вообще не сделаешь наверное.

Ну, тут зависит от задачи. Я вот предпочту тип HashSet<T> чем struct NoDuplicates(Vec<T>). Кмк, с ним и работать удобнее, и ошибиться сложнее.

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

Все это очень хорошо в теории. Я так попытался писать на плюсах в реальном проекте, только настоящая проблема этого подхода не в том что система типов слаба (а она на самом деле слаба) а в коллегах, которые с полным недоумением спрашивают, а нахрена это все? И у них есть непрошибаемый козырь писать так объективно сложнее, а читать неподготовленному мозгу такое вообще противопоказанно. С легаси несовместимо категорически, т.к. требует неимоверных усилий по рефакторингу и как обычно в условиях отсутствия тестов и времени под давлением типа давай результат вчера и погуще. Так что в реальном мире мне пришлось согласиться с мертворожденностью этого подхода. Пока мне приходится героически преодолевать ограничения системы типов и костность мозгов это никогда не выйдет дальше вот таких статей. Мозги нужно учить лучшему в вузе, а этого там не рассказывают. Человек валидировал десятки лет и по его словам успешно ( с точки зрения формальных критериев: закрытые таски, вовремя сделанные релизы), это значит вы никогда не сможете убедить его работать больше чем прежде для достижения того же результата. Обещанию меньшего количества багов НИКТО не верит, а увидеть логику почему это так не может в силу скудоумия/костности. Пробовать отказываются не понимая зачем им это надо. Компилятор тоже вам вставит палки в колеса везде где только возможно, т.к. уже давно в тренде требовать от программиста выражать свои намерения максимально явно, а это в свою очередь вызывает необходимость писать много бойлерплэйт кода в парадигме парсинга. Так что я вам категорически не советую даже пробовать такое в реальных проектах на плюсах, идею не оценят, и сделают все от них возможное чтобы вы отказались от этой идеи и по скорее.

А что мешает это использовать в новых проектах, без косных коллег?

Да вобщем то ничего не мешает. Только без колег значит в одиночку значит какой-то мало кому нужный опен соурс в ваше свободное время. На работах за последние 10 лет не было ни разу случая что нужно что то писать с нуля. Это всегда уже существующий и как то работающий код который нужно расширить/пофиксить. Мест работ и стран и профилей компаний много разных но это ни на что не влияет. Ситуация где у вас на работе нет/мало колег и нужно писать новый код == вы в самом начале стартапа или совершенно новый проект, по какой то неведомой мне причине это значит что вы и 1,5 других колег джуниоры и вам все это ещё неизвестно или нет времени на эксперименты. Может быть потому что стартапы не могут предложить денег/интерес для более опытных девелоперов, а свой стартап опытные девелоперы почему то не спешат начинать. Вобщем такое возможно, но мне не довелось поучаствовать.

Вы не так прочитали. Не без коллег вообще, а без костных коллег. Последние 2 рабочие места (получается, больше трёх лет) меня окружают люди, разделяющее моё стремление писать более надежный и производительный код, и которые хоть немного стараются развиваться и совершенствоваться. И это не потому, что мне везёт — в какой-то момент у меня бывало по 5 собеседований в день, когда я выходил в 8 часов из дома на первое собеседование и возвращался в 22.00 с последнего. Ну и, оглядывясь назад, в общем-то не зря я это делал. Чего и вам желаю.


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

Как раз-таки в стартапах мне обычно предлагают больше всего, не считая банков, где меня хотят купить в рабство, чтобы я страдал, и доплачивают исключительно за это. И задачи в стартапах тоже интересные бывают — у меня вон коллега например с vtune ползал просто на корточках по миллиметру по кодовой базе, вылизывая каждый угол, чтобы нагрузить архитектуру на 100%. И судя по отчёту интеловского тулинга, это получилось. Опыт написания такого софта — очень полезный, и главное, интересный.

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


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

Прочитал, сделал шажок, но ничего полезного не получил ((


Может я не Rust программист??

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

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

Нет, тут идея в другом.

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

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

Нет, тут идея та же самая.

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

Просто синтаксический сахар.

Иными словами, вы прочитали всю статью, но так и не поняли её.

Зарегистрируйтесь на Хабре , чтобы оставить комментарий

Публикации

Истории