Парсите, а не валидируйте

Автор оригинала: Alexis King
  • Перевод

Еще в декабре мне попалась одна совершенно замечательная статья на английском, посвящённая использованию системы типов языка для более широкого класса задач, для повышения надежности приложений и простоты рефакторинга. К сожалению, в тот момент я был слишком занят написанием статей по ФП, которые крайне важно было написать, пока свежи воспоминания. Но теперь, когда с этой задачей я справился, наконец дошли руки перевести эту замечательную заметку. Оригинальный язык примеров — Хаскель, но я решил переписать их на раст, для более широкого охвата аудитории. Однако язык тут совершенно неважен, советы этой статьи я применяю в ежедневной разработке на вполне себе "приземлённых" C# и TypeScript, так что если вы просто стараетесь писать надёжный и поддерживаемый код, то, вне зависимости от языка, статья вам будет в тему.


Благодарю за вычитку и помощь в переводе Hirrolot, funkill и andreevlex



На протяжении достаточно длительного периода времени я изо всех сил старалась найти точный, простой способ объяснить, что такое "Type-Driven Design" (здесь и далее — TypeDD, прим. пер.). Довольно часто меня спрашивали "Как ты додумалась до такого решения?", но удовлетворительного ответа у меня не было. Я точно знаю, что оно не пришло ко мне как видение: у меня был итеративный процесс проектирования, не обязывающий сию минуту из ничего получить "правильную" архитектуру, но до сих пор мне не особо удавалось истолковать этот процесс другим.


Но месяц назад случился поворотный момент: я рассуждала в Твиттере о различии парсинга JSON в статически и динамически типизированных языках, и наконец я нашла то, что искала. Теперь у меня есть единственный, цепкий слоган, являющийся квинтэссенцией того, чем для меня является TypeDD, и, что ещё лучше, состоящий всего из нескольких слов:


Парсите, а не валидируйте.


Суть TypeDD


Ладно, признаю: если вы ещё не в курсе про TypeDD, мой хитроумный слоган, скорее всего, ничего вам не скажет. К счастью, именно для этого и написана вся остальная статья. Я собираюсь объяснить, что я имею в виду, во всех подробностях, но сначала давайте немного пофантазируем.


Ландшафт возможностей


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


enum Void {}

fn foo(x: i32) -> Void

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


fn head<T>(xs: Vec<T>) -> T

Эта функция возвращает первый элемент списка. Возможно ли её реализовать? Да, сперва это не выглядит чем-то сложным, но если мы попробуем её выразить, то компилятор будет недоволен:


fn head<T>(xs: Vec<T>) -> T {
    match xs.as_slice() {
        [x, ..] => *x
    }
}

error[E0004]: non-exhaustive patterns: `&[]` not covered
 --> src/lib.rs:2:11
  |
2 |     match xs.as_slice() {
  |           ^^^^^^^^^^^^^ pattern `&[]` not covered
  |

Компилятор нам заботливо сообщает, что данная функция частичная, что означает, что она не определена для всех возможных значений параметров. В частности, она не определена для случая, когда параметром является [], пустой список. И это совершенно разумно, т.к. невозможно вернуть первый элемент списка, если список пустой, ведь в нём нет ни одного элемента, чтобы его можно было вернуть! Таким образом, как ни удивительно, мы узнали, что эту функцию тоже невозможно реализовать (не прибегая к хакам вроде паник и эксепшнов, прим. пер.).


Делаем частичные функции тотальными


Для людей с опытом динамически-типизированных языков такой вывод может показаться довольно неожиданным. У нас есть список, и мы имеем полное право хотеть получить из него первый элемент. И конечно же, операция "получить первый элемент списка" не является невозможной в статически-типизированных языках, она просто требует небольшого количества церемоний. Существует два способа исправить функцию head, и мы начнём с того, который попроще.


Управление ожиданиями


Как мы уже убедились, функция head является частичной, т.к. невозможно вернуть элемент из пустого списка: мы делаем обещание, которое невозможно соблюсти. К счастью, существует простое решение этой дилеммы: ослабить наше обещание. Исходя из того, что мы не можем гарантировать, что в списке будет элемент, подлежащий возврату, нам следует немного повлиять на ожидания вызывающего кода: мы сделаем всё возможное, чтобы вернуть элемент, в то же время оставляя за собой право ничего не вернуть. В Rust мы выражаем эту возможность при помощи типа Option:


fn head<T>(xs: Vec<T>) -> Option<T>

Это даёт достаточно свободы, чтобы реализовать функцию head — позволяя вернуть None, когда мы понимаем, что не можем вернуть никакого значения типа T:


fn head<T>(xs: Vec<T>) -> Option<T> {
    match xs.as_slice() {
        [x, ..] => Some(*x),
        [] => None,
    }
}

Проблема решена, так? Ну, на текущий момент — да… Однако это решение имеет неявную цену.


Возвращение Option, несомненно, удобно, когда мы реализуем head. Однако значительно менее удобно становится её использовать. Так как head всегда может вернуть None, на весь вызывающий код накладывается бремя проверок этого варианта, и иногда такой перевод стрелок очень напрягает. Чтобы понять почему, давайте посмотрим на такой код:


fn get_configuration_directories() -> Result<Vec<String>, &'static str> {
    let config_dirs_string = std::env::var("CONFIG_DIRS").map_err(|_| "cannot read env")?;
    let list: Vec<_> = config_dirs_string.split(',').map(|x| x.to_string()).collect();
    if list.is_empty() {
        return Err("CONFIG_DIRS cannot be empty");
    }
    Ok(list)
}

fn main() -> Result<(), &'static str> {
    let config_dirs = get_configuration_directories()?;
    match head(config_dirs) {
        Some(cacheDir) => initialize_cache(cacheDir),
        None => panic!("should never happen; already checked config_dirs is non-empty")
    }
    Ok(())
}

Когда функция get_configuration_directories получает список путей из окружения, она сразу проверяет что список непустой. Однако когда мы используем head в main, чтобы получить первый элемент списка, результат типа Option<&str> требует от нас проверки случая None, который, как мы знаем, никогда не произойдёт! Это чрезвычайно плохо по многим причинам:


  1. Во-первых, это просто утомительно. Мы уже знаем, что список непустой, почему мы должны замусоривать код дополнительными ненужными проверками?


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


  3. Наконец, и что хуже всего, в этом коде затаился баг. Что, если get_configuration_directories изменят так, что она перестанет проверять список на пустоту, и не важно, случайно или специально? Программист может и не помнить, что нужно обновить main, и внезапно "невозможная" ошибка станет не просто возможной, а очень даже вероятной.



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


Платим вперёд


Понятно, что наша модифицированная версия функции head работает не совсем так, как нам хотелось бы. Мы хотели бы, чтобы она каким-то образом была умнее: если мы уже проверили, что список не пуст, head должен безусловно вернуть первый элемент, не принуждая нас обрабатывать случай, про который мы точно знаем, что он невозможен. Как бы нам это сделать?


Давайте посмотрим на изначальную (частичную) сигнатуру head ещё раз.


fn head<T>(xs: Vec<T>) -> T

В предыдущем разделе мы превратили частичную сигнатуру в тотальную, ослабив требования к возвращаемому типу. Но раз нам это не подходит, у нас остаётся лишь одна вещь, которую мы можем поменять: тип аргумента (в нашем случае — Vec<T>). Вместо ослабления возвращаемого типа мы можем усилить тип аргумента, устранив саму возможность вызова head на пустом списке.


Чтобы это сделать, нам нужен тип, представляющий непустые списки.
К счастью, такой тип NonEmptyVec несложно написать. У него будет следующее определение:


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

Заметьте, что NonEmptyVec — всего лишь пара из значения типа T и обычного (возможно, пустого) Vec<T>. Такая структура удобно моделирует непустой список путём сохранения первого элемента отдельно от хвоста, ведь даже если второй компонент Vec<T> представляет собой [], то первый компонент всегда должен присутствовать. Благодаря этому, реализация функции head становится совершенно тривиальной:


fn head<T>(xs: NonEmptyVec<T>) -> T {
    xs.0
}

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


fn get_configuration_directories() -> Result<NonEmptyVec<String>, &'static str> {
    let config_dirs_string = std::env::var("CONFIG_DIRS").map_err(|_| "cannot read env")?;
    let list: Vec<_> = config_dirs_string.split(',').map(|x| x.to_string()).collect();
    match non_empty(list) {
        Some(x) => Ok(x),
        None => Err("CONFIG_DIRS cannot be empty")
    }
}

fn main() -> Result<(), &'static str> {
    let config_dirs = get_configuration_directories()?;
    initialize_cache(head(config_dirs));
    Ok(())
}

Заметьте, что лишняя проверка в main полностью исчезла! Вместо этого мы производим проверку ровно один раз, в функции get_configuration_directories. Она конструирует NonEmptyVec из Vec с помощью функции non_empty, имеющую следующую сигнатуру:


fn non_empty<T>(list: Vec<T>) -> Option<NonEmptyVec<T>>

Обратите внимание, что Option никуда не делся, однако в этот раз мы обрабатываем случай None в самом начале программы: в том месте где мы и раньше делали валидацию. Когда проверка пройдена, мы получаем значение типа NonEmptyVec, которое сохраняет (на уровне типов!) тот факт, что список на самом деле не пуст. Другими словами, значение типа NonEmptyVec эквивалентно значению типа Vec<T> плюс доказательству, что список не пуст.


Усилив тип аргумента функции head вместо того чтобы ослабить тип результата, мы полностью избавились от всех проблем из предыдущего раздела:


  • В коде отсутствуют лишние проверки, поэтому нет и никакого оверхеда по производительности.


  • Более того, если функция get_configuration_directories перестанет проверять список на пустоту, то её результирующий тип тоже поменяется. Следовательно, функция main не сможет тайпчекнуться, сообщая о проблеме до того как мы вообще запустили программу!



Более того, мы можем тривиально восстановить старое поведение функции head с помощью новой версии, композируя её с non_empty:


fn old_head<T>(xs: Vec<T>) -> Option<T> {
    non_empty(xs).map(head)
}

Обратите внимание, что обратное неверно: не существует способа получить новую версию функции head из старой. Таким образом, второй подход превосходит первый по всем параметрам.


Сила парсинга


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


fn validate_non_empty<T>(xs: Vec<T>) -> Result<(), UserError> {
    if !xs.is_empty() {
        Ok(())
    } else {
        Err(UserError::new("list cannot be empty"))
    }
}

fn parse_non_empty<T>(mut xs: Vec<T>) -> Result<NonEmptyVec<T>, UserError> {
    if !xs.is_empty() {
        let head = xs.remove(0);
        Ok(NonEmptyVec(head, xs))
    } else {
        Err(UserError::new("list cannot be empty"))
    }
}

Эти две функции практически идентичны: они проверяют переданный список на пустоту, и если он пустой, то они возвращают сообщение об ошибке. Вся разница заключается в возвращаемом значении: validate_non_empty всегда возвращает (), тип, который не содержит никакой информации, а parse_non_empty возвращает NonEmptyVec<T>, уточнение входного типа, которое сохраняет полученное знание в системе типов. Обе функции проверяют одно и то же, но parse_non_empty даёт вызывающему коду доступ к полученной информации, а validate_non_empty просто выкидывает её.


Эти две функции элегантно иллюстрируют два различных взгляда на роль системы типов: validate_non_empty просто подчиняется тайпчекеру, но только parse_non_empty полностью использует те преимущества, которые он даёт. Если вы видите, почему функция parse_non_empty предпочтительнее, то вы должны уже понимать, что означает мантра "парсите, а не валидируйте". Однако возможно вы скептически относитесь к имени parse_non_empty. Действительно ли она что-то парсит, или она просто валидирует вход и возвращает результат? И, хотя точное определение того, что означает парсинг или валидация, является предметом для обсуждения, я считаю что parse_non_empty это полноценный парсер, пусть и очень простой.


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


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


  • Библиотека serde_json предоставляет функцию from_str которая позволяет парсить данные в формате JSON в доменные типы


  • Подобным образом clap предоставляет набор парсер-комбинаторов для разбора аргументов командной строки


  • Библиотеки вроде diesel предоставляют механизм для парсинга значений, хранящихся во внешних хранилищах.


  • Экосистема actix-web построена вокруг парсинга Rust типов из компонентов пути, строк запроса, HTTP заголовков и так далее.



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


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


Опасность валидации


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


К сожалению, всё не так просто. Ad-hoc валидация ведёт к феномену, который специалисты в области теоретико-языковой безопасности называют парсинг наугад. В статье 2016 года под названием The Seven Turrets of Babel: A Taxonomy of LangSec Errors and How to Expunge Them авторы приводят следующее определение:


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

Затем они объясняют проблемы, внутренне присущие подобной валидационной технике:


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

Другими словами, программа, которая не парсит заранее все необходимые ей данные, рискует обработать часть данных, затем обнаружить ошибку в другой части, и внезапно оказаться в ситуации, когда нужно откатить уже произведённые изменения, чтобы сохранить консистентность. Иногда — например, при работе с РСУБД, это возможно, но в общем случае — нет.


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


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


Парсим, а не валидируем, на практике


До сих пор, весь текст был больше похож на рекламный слоган. Он говорит "Ты, дорогой читатель, должен парсить!", и, если я хорошо выполняю свою работу, то по крайней мере часть читателей должна со мной согласиться. Но даже если вы понимаете "что" и "почему", вы можете быть не до конца уверены насчёт "как".


Мой совет: фокусируйтесь на типах данных.


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


fn check_no_duplicate_keys<K: Eq, V>(xs: &[(K,V)]) { ... }

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


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


fn check_no_duplicate_keys<K: Eq, V>(xs: &[(K,V)]) -> HashMap<K,V> { ... }

И теперь проверка не может быть удалена, потому что результат функции необходим для продолжения работы программы!


В этом гипотетическом сценарии видны две простые идеи:


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


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


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



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


Вот несколько дополнительных советов, расположенных в произвольном порядке:


  • Позвольте вашим типам данных информировать ваш код, не позволяйте коду контролировать типы данных. Боритесь с искушением запихнуть bool в структуру потому что он нужен в функции, которую вы пишете (На эту тему очень рекомендую к прочтению статью Булева слепота, и небольшое замечание к ней, прим. пер.). Не бойтесь рефакторить код, чтобы использовать более правильное представление данных — система типов удостоверится, что вы учли все места, которые требуют изменения, и это спасёт вас от головной боли в дальнейшем


  • Относитесь к функциям без возвращаемого результата или с типом Result<(), Error> с большим подозрением. Иногда они совершенно необходимы, потому что они могут производить императивный эффект без какого-либо разумного результата, но если единственная цель такой функции это вызвать ошибку, скорее всего есть лучший путь.


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


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


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

  • Используйте абстрактные типы данных, чтобы ваши валидаторы "выглядели как" парсеры. Иногда, сделать данные действительно непредставимыми совершенно непрактично, учитывая возможности которые даёт ваш язык программирования, например, проверка, что число попадает в некоторый диапазон. В этом случае используйте декоратор (newtype) с умным конструктором, чтобы сделать псевдо-парсер из валидатора.



Как обычно, используйте здравый смысл. Иногда просто не стоит ломать весь код и переписывать всё приложение, чтобы избежать единственного потенциального error "impossible" где-то в коде — просто не забывайте относиться к таким местам как к радиоактивной субстанции, которой они и являются, и обходитесь с ними со всей необходимой аккуратностью. В самом крайнем случае оставьте хотя бы комментарий, чтобы задокументировать инварианты для тех, кто в будущем будет модифицировать этот код.


Резюме


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


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


К сожалению, я знаю не так много ресурсов на эту тему, но я знаю одно: я никогда не стесняюсь порекомендовать классную статью Мэта Парсона Type Safety Back and Forth. Если вам нужна ещё одна доступная статью на тему этих идей, то я крайне рекомендую прочитать её. Для намного более серьёзного погружения в эти идеи я могу порекомендовать работу Мэта Нунана Ghosts of Departed Proofs, в которой изложены некоторые более продвинутые техники по выражению более сложных инвариантов, нежели чем те, что я привела в статье.


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




От переводчика


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

AdBlock похитил этот баннер, но баннеры не зубы — отрастут

Подробнее
Реклама

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

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

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


      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>;

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

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

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


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

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

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

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


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


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

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

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

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


            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) { }
              0
              В общем случае, валидация может предполагать соответствие каким-либо внешним данным, и потому принципиально не может быть выражена системой типов.

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

                0

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

                  +2

                  Тогда у вас DateTime.Now.DayOfWeek живёт в IO на самом деле, и сначала значение оттуда надо вытащить. А потом оно ничем не будет отличаться от любого другого значения.

                  0

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

                    +1

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

                  0

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

                    +1

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

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

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

                    +2

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


                    В этом плане мне нравятся языки с завтипами. Например, мы пишем функцию и хотим на этапе компиляции проверить, что мы получаем в аргументе число, но не просто число, а либо 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"

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

                      +1
                      В общем, все плюсы без особых минусов.

                      Пока вам не нужно написать функцию


                      weaken : (n : Int ** n `elem` [5, 9]) -> (n : Int ** n `elem` [5, 9, 12])
                        0

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


                        img


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

                          0

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

                        0

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


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


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

                          +3
                          Минусы такие же как и у макросов — во время компиляции начинает происходить столько магии, что теряется контроль.

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


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

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


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


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

                            0

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

                              +2

                              Ага, а потом получаем ошибки типа таких.


                              Ну и некоторые вещи в том же Coq так и работают: мол, чувак, за 5 минут доказать не смог, отменяю вычисления.

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

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

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


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

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

                                  Так это ж для всего всегда верно. Возьмите те же плюсы: лет 5 назад — «мы ещё не знаем best practices по работе с констекспрами», сейчас — «мы ещё не знаем best practices по работе с концептами».

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

                                    Мы начали с того, что «давайте запихаем побольше проверок в типы» и перешли к «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.
                                      0
                                      Я же играю в адвоката дьявола и пытаюсь показать, что на практике могут быть сложности, которые всю идею похоронят. Причем сложности эти являются оборотной стороны достоинств dependent types и от них неотделимы.
                                      То есть нельзя получить dependent types и не получить проблем с IDE и гору кода, который только автор понимает.

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


                                      Тут начинается обсуждение types vs unit tests, где я опять играю ту же роль и аргументирую, что проверки в run time проще писать и отлаживать.

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


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

                                      О практических проблемах лучше говорить всё же тогда, когда они на самом деле возникают. Лично в моём опыте основная практическая проблема — хреновое discoverability конкретно в идрисе, когда трудно по желаемой сигнатуре найти потенциальные термы. Но эта проблема решена в хаскеле (hoogle), решена в коке (там есть какой-то поиск по подключённым библиотекам), так что это вопрос конкретной реализации.

                                  0
                                  я как раз сейчас в рамках фанового проекта пилю компиляцию этих refinement types в зависимые типы

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


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

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


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

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

                                    Именно в этом и смысл. Жить в полноценном завтипизированном языке без непонятно как работающих тактик, но не доказывать руками такие нетривиальные факты, как { a b : Nat } → (a > b) → (a > 0), например.


                                    То есть, есть какое-то подмножество языка, которого достаточно для 95% прикладного ежедневного программирования, и где вам при этом вообще не нужно писать пруфтермы руками и даже думать о них — SMT-солвер за вас всё сделает, экстракция пруфа из солвера удовлетворит de Bruijn criterion (хотя пруфы там получаются ппц и, вероятно, не всегда конструктивны — ну лан, непуристам можно будет иногда и believe_me обойтись, надеясь на корректность солвера, один фиг у пруфтермов для refinement types заведомо нет вычислительного контента). При этом вы получаете все ништяки полноценного зависимо типизированного языка, всегда можете воспользоваться его мощью, и так далее.


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


                                    По-моему, это интересно.


                                    А если на самом деле допускать believe_me, то интересно ещё и метатеоретически.


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

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


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

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

                                      0
                                      Именно в этом и смысл.

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


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

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


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

                                        0
                                        Все еще не понял, в чем.

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


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

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


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

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

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

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

                                      Конечно.

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

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

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

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

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


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

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

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

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


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

                                              Но при этом на плюсах писали, пишут и будут писать (к счастью или к сожалению).

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

                                            У одних может быть квантор всеобщности, у других — нет.


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

                                            Система типов не обязана быть Тьюринг-полной.


                                            Если что, под Тьюринг-полнотой системы типов подразумевается возможность произвольных вычислений на уровне типов, а это не так: во всех интересных языках проверка типов доказуемо завершима. А term finding и полный type inference какой-нибудь и для вашего любимого языка неразрешим, но вы же как-то с этим живёте. У джавы вон вообще язык шаблонов Тьюринг-полный, в отличие от.

                                              0

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

                                                0

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


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

                                          0
                                          Чтобы можно было выразить все интересные свойства программы в виде типов, нужны те самые Тьюринг полные dependent types.

                                          Тьюринг-полные не нужны. Вся прикладная математика вообще формализуется без каких-либо dependent types.


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

                                          А как проверить, что ваши тесты правильные? Пишете ли вы тесты на тесты? Пишете ли вы тесты на тесты на тесты? Когда вы останавливаетесь?

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

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

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

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

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

                                      +4

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

                                        +3

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

                                          0

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

                                          +2

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

                                            +1

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


                                            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
                                              +1

                                              А что значит "в рамках самих типов"? Чем не угодил NonEmptyVec в статье? Если вы про выражение непустоты в сигнатуре, то в Idris это делается примерно так: Vect (S n) elem, где (S n) — как минимум единица (целые числа в Idris определены индуктивно). В F* с его типами с уточнениями длину вектора можно описать таким образом: n:nat{n>=1}.

                                                0

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

                                                  0

                                                  Ну я таким образом и в Си могу сделать:


                                                  struct NonEmptyVect {
                                                      T elem;
                                                      struct Vect rest;
                                                  };

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

                                                    0

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


                                                    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?        
                                                    } 

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

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

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

                                                      struct NonEmptyVect okay = {.elem = 1, .rest = {2}};
                                                      struct NonEmptyVect alsoOkay = {.elem = 1, .rest = {}};
                                                      struct NonEmptyVect err = ??? // error!

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

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


                                                      Есть ещё один вариант параметризации длины списка — крейт typenum в Rust, но мне его ещё не приходилось использовать.

                                                        –1

                                                        Кстати, вычитал из стандарта только что:


                                                        An array type describes a contiguously allocated nonempty set of objects with a particular member object type, called the element type.

                                                        Поэтому правильным будет хранить указатель на массив (может быть NULL), а не сам массив.

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

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

                                                        0

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


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


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

                                                          0
                                                          struct NonEmptyVect {
                                                              T elem;
                                                              T rest[];
                                                          };
                                                            0

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

                                                              0

                                                              Ну придётся хранить где-то в другом месте значит. Всё зависит от того, с чем сравниваем.

                                                                0

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


                                                                [1, 2];

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


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


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

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

                                                      +1

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


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


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

                                                        0

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

                                                          0

                                                          Ну тогда это действительно завтипы, и Vect (S n) a — самый каноничный вариант. Ещё можно (xs : List a ** null xs = False).

                                                          +1
                                                          В F* с его типами с уточнениями длину вектора можно описать таким образом: n:nat{n>=1}.

                                                          Раз тут знатоки F* есть — как именно там сочетаются refinement types и dependent types? Я быстро проглядел папир по F* и по meta-F*, и у меня сложилось впечатление, что DT там пытаются вкрутить для того, чтобы сделать язык RT более мощным, манипулируя генерируемыми verification conditions SMT-солверу, и всё.

                                                            0

                                                            Ну до знатока по F* мне ещё далеко — могу наврать по таким вещам.

                                                          0

                                                          Можно, но с костылями

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

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

                                                            +1

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


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

                                                              0

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

                                                              0

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


                                                              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-типом. Единственная проблема там с борровчекером, про которое есть замечание в конце статьи, но и её можно победить, если не пользоваться паттерн матчингом, который в текущей версии языка только для слайсов работает, а для векторов — нет.

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

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

                                                                  –2

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


                                                                  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))
                                                                      }
                                                                  }
                                                                    +1

                                                                    Ну нельзя же так делать. Когда 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)
                                                                      0

                                                                      Возможно, в глубокий ансейф я не погружался. В любом случае, это просто иллюстрация того что сделать эффективный парсинг можно, и это парсинг не обязан быть дороже валидации. В языках с ГЦ такую штуку сделать можно естественно, в расте придется обмазатся ансейфом: это к слову приём который автор смарт конструктором называет, ведь компилятор тут не помогает никак. Но сделать можно, и не очень трудно. Не нравится 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..]
                                                                          }
                                                                      }

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

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

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


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

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

                                                                          +1

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

                                                                  0

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

                                                                    +2

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




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

                                                                      0

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

                                                                  0
                                                                  fn foo(x: i32) -> Void

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

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

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


                                                                    Правда, в расте, скорее всего, можно сделать


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

                                                                    то есть, бесконечная рекурсия, и тайпчекер не пикнет, но в языках с более сложной системой типов такое написать нельзя. Для них можно формально показать, что функций -> Void не существует.

                                                                      +1
                                                                      Правда, в расте, скорее всего, можно сделать

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

                                                                        0

                                                                        Ну это легко починить:


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

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

                                                                          0

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


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

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

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

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

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

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


                                                                              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
                                                                                never и bottom это разве не одно и тоже?
                                                                                www.typescriptlang.org/docs/handbook/basic-types.html#never
                                                                                  +1

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


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

                                                                                    0
                                                                                    Спасибо за ссылку. У вас скорее 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.

                                                                                      +1
                                                                                      Вот функция a -> Void, или иными словами 0^a ни чему же не противоречит?

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


                                                                                      И это лишний повод считать, что 0^a = 0 для a ≠ 0, и 1 для a = 0 (потому что id : Void -> Void; id x = x валидно).


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

                                                                                      Void — это ноль в смысле пустого множества, ложности в логике и так далее. Bottom — это отродье, не хочу боттом в языке.

                                                                                        0

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


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

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

                                                                                          Почему?


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


                                                                                          Как контрпример возьмите System U (это где парадокс Жирара), там ⊥ вполне себе населён, но он там, собственно, есть.

                                                                                            0

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


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

                                                                                              0

                                                                                              Я что-то запутался, о чём мы спорим.

                                                                                                0

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

                                                                                        0

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

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

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

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

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


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

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


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

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

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

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

                                                                                                Почти, только мы всё еще знаем, что у неё одно яблоко. Потому что и в обратную сторону, 1+0 это 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, так?
                                                                                                    +1

                                                                                                    Просто потому что код ричабл — существует вероятность, что вернется 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 ошибку в таком использовании.

                                                                                              +1
                                                                                              Она не может претендавать на абсолютную полноту и безошибочность, по определению.

                                                                                              Поэтому отказываются от полноты (в смысле, существуют семантически корректные, но нетипизируемые термы).


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

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

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

                                                                                                0

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

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

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

                                                                                                    +1

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

                                                                                                      –1
                                                                                                      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 _ — и ничего не повиснет даже.

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

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

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

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


                                                                                                          Я вижу у тебя небольшая каша в голове, давай я по порядку все объясню. Вот у тебя есть тип 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 содержит лишнее значение (как минимум, одно).

                                                                                                            0

                                                                                                            Ну тут всё как всегда: хаскелисты прикидываются, что у них нет боттомов, и радуются жизни. Потому что иначе вообще никакая арифметика на типах не работает, потому что A + B не просто A \amalg B, а A \amalg B \amalg Bottom. Ну и (A, B) не просто A × B, а (A × B) \amalg Bottom или что-то такое, у меня голова болеть начинает, когда я о боттомах думаю.


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

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

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

                                                                                                                  0
                                                                                                                  Что вы имеете ввиду, можно пример кода?
                                                                                                          +1
                                                                                                          Это в каких? Мне ни одного не известно.

                                                                                                          Вы не знаете хаскель и идрис? Не ожидал!


                                                                                                          Тыц хаскель, тыц идрис. Что-то такое, естественно есть и в агде, и в коке, но я не помню, как оно там называется.


                                                                                                          он же undefined, он же Unit

                                                                                                          Чё. Как можно ставить знак равенства между undefined, начиная от тупо синтаксически undefined: a, Unit: *?

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

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


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

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

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


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

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

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


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

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


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

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


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

                                                                                                            +1
                                                                                                            Ну и Top, который undefined, в тс он unknown, например.

                                                                                                            Эм, почему это undefined?


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

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


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

                                                                                                              0
                                                                                                              Эм, почему это undefined?

                                                                                                              Ну а что он?


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

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


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


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

                                                                                                        –2

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

                                                                                                          +3

                                                                                                          Either T Void изоморфен T. Это буквально x+0=x.


                                                                                                          Цитата от Бартоша:


                                                                                                          image

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

                                                                                              В самом деле, статическая типизация не решает научных проблем, не страхует от всех возможных видов ошибок и не претендует на абсолютную истину. На мой взгляд, она больше про 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)
                                                                                              }
                                                                                              ...
                                                                                              


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

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


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

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

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

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

                                                                                            Она недостаточно более сложная :]

                                                                                        +2
                                                                                        В typescript для таких функций есть отдельный тип never, например
                                                                                          +1

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

                                                                                        +2

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

                                                                                        0
                                                                                        let head = xs.remove(0);

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

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

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

                                                                                              0

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

                                                                                                0

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


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

                                                                                          +1

                                                                                          Спасибо, давно пользуюсь подобными штуками в Расте. Правда 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

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


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


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

                                                                                              +1

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

                                                                                                0

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

                                                                                                +1

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

                                                                                              0

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

                                                                                                +1

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

                                                                                                  0

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

                                                                                                    +1

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


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

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

                                                                                                0

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


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

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


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

                                                                                                  +1

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

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

                                                                                                Самое читаемое