Если вы иногда задаете себе вопрос: «а всё ли хорошо мне в этот метод приходит?» и выбираете между «а вдруг пронесет» и «лучше на всякий случай проверить», то добро пожаловать под кат…

Поправка: Как заметили lorc и 0xd34df00d, то, о чем ниже идет речь, называется зависимыми типами. Почитать о них можно тут. Ну а ниже исходный текст с моими соображениями по этому поводу.

При разработке часто возникает потребность проверки валидности данных для некоторого алгоритма. Формально это можно описать следующим образом: пусть мы получаем некоторую структуру данных, проверяем ее значение на соответствие некоторой области допустимых значений (ОДЗ) и передаем ее дальше. Впоследствии эта же структура данных может быть подвергнута такой же проверке. В случае неизменяемости структуры, повторная проверка ее валидности – очевидно лишнее действие.

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

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

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

class Parent { ... }
class Child : Parent { ... }

...

void processValidObject(Parent parent) {
    if (parent is Child) {
        // process
    } else {
        // error
    }
}

Согласитесь, что теперь проблема гораздо яснее. Перед нами каноничное нарушение принципа подстановки Лисков. Почитать почему нарушать принцип подстановки плохо можно, например, тут.

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

В Swift'е, на уровне синтаксиса, решается проблема проверки на null. Идея состоит в том, чтобы разделить типы на допускающие значение null и не допускающие. При этом сделано это в виде сахара таким образом, что программисту не требуется объявлять новый тип. При объявлении типа переменной ClassName гарантируется, что в переменной ненулевое значение, а при объявлении ClassName? переменная допускает значение null. При этом между типами существует коваринтность, то есть в методы, принимающие ClassName?, можно передать и объект типа ClassName.

Эту идею можно расширить до задаваемых пользователем ОДЗ. Снабжение объектов метаданными, содержащими ОДЗ, хранящимися в типе, устранит описанные выше проблемы. Хорошо бы получить поддержку такого средства в языке, но такое поведение реализуемо и в «обычных» ОО-языках, таких как Java или C# с помощью наследования и фабрики.

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

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

Так же в статье не хватает примера. Пусть на вход к нам поступают некоторые пути файлов. Наша система в некоторых случаях работает со всеми файлами, а в некоторых случаях только с файлами, к которым мы имеем доступ. Далее мы хотим передать их в разные подсистемы, которые так же работают как с доступными, так и с недоступными файлами. Далее эти подсистемы передают файлы еще дальше, где опять не понятно файл доступен или нет. Таким образом во всяком сомнительном месте появится проверка доступа или может напротив забудется. Из-за этого система усложнится в силу повсеместной неоднозначности и проверок. А проверки эти грузят диск и вообще тяжелые. Можно эту проверку кешировать в булевом поле, но это нас не избавит от самого факта необходимости проверки. Я предлагаю ответственность проверки переложить с разработчика на компилятор.

Комментарии (46)


  1. MonkAlex
    18.11.2019 00:08

    Не знаю о каких кейсах вы, но мне непонятен кейс сущностей:
    1. сущность находится в валидном состоянии и хранится в базе
    2. выполняется действие над сущностью, сущность изменена относительно состояния в базе
    3. вызывается метод

    вы предлагаете в такой ситуации создавать из сущности явно отдельный класс, который будет заявлять о потенциальной невалидности и необходимости провалидировать входные данные? при разрастании системы такой ход потребует постоянного преобразования из одного объекта в другой, причем в обоих направлениях (сущность <-> dto).


    1. SanQri Автор
      18.11.2019 00:19

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


      1. MonkAlex
        18.11.2019 00:26

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


        1. SanQri Автор
          18.11.2019 00:43

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

          Пусть на вход к нам поступают некоторые пути файлов. Наша система в некоторых случаях работает со всеми файлами, а в некоторых случаях только с фалами, к которым мы имеем доступ. Далее мы хотим передать их в разные подсистемы, которые так же работают как с доступными, так и с недоступными файлами. Далее эти подсистемы передают файлы еще дальше, где опять не понятно файл доступен или нет. Таким образом во всяком сомнительном месте появится проверка доступа или может напротив забудется. Из-за этого система усложнится в силу повсеместной неоднозначности и проверок. А проверки эти грузят диск и вообще тяжелые. Можно эту проверку кешировать в булевом поле, но это нас не избавит от самого факта необходимости проверки. Я предлагаю ответственность проверки переложить с разработчика на компилятор.


    1. VolCh
      18.11.2019 09:22
      +1

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


      Предложение не без недостатков, но имеет право на жизнь, хотя я скорее бы создал UserData для заполнения из внешнего мира, провалидировал его и создавал бы уже User, который обеспечивает свою валидность. Другое дело, если внутри User есть какое-то свойство type на основании которого область допустимых значений меняется, например User с type admin может иметь не заполненное имя и email. Тут уже по умолчанию лучше создать подтип


      1. MonkAlex
        18.11.2019 09:37
        +1

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


        1. VolCh
          18.11.2019 10:53

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


          1. sshikov
            18.11.2019 19:26

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


  1. lair
    18.11.2019 00:40

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

    И получить взрывообразное увеличение числа типов данных.


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

    … почему же только в ООП? Вообще везде в программировании.


    1. SanQri Автор
      18.11.2019 00:46

      И получить взрывообразное увеличение числа типов данных.

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

      … почему же только в ООП? Вообще везде в программировании.

      Потому что про ООП часто говорят, что это моделирование систем на основе наблюдаемого мира. А так, согласен, применимо не только в ООП.


      1. emacsway
        18.11.2019 01:50

        Полагаю, что имелось ввиду получение проблемы «Parallel Inheritance Hierarchies».

        Если я Вас правильно понял, тогда то, что Вы предлагаете сделать, очень похоже на "Replace Type Code with Subclasses". Это, действительно, решает проблему «Switch Statements» (классифицированный Code Smell). И это, действительно, может привести к Code Smell «Parallel Inheritance Hierarchies» и взрывному комбинаторному росту типов. Чтобы этого не допустить, вместо «Replace Type Code with Subclasses» можно применить «Replace Type Code with State/Strategy».

        решается проблема проверки на null
        Обычно эта проблема решается с помощью Special Case (он же).

        можно создавать объекты через фабрику
        Действительно, в OOP желательно избегать условных операторов в исполняемом коде, поскольку вся суть ООП заключается в возможности группировать вместе данные и поведение. Чтобы обеспечить полиморфизм, условные операторы желательно переносить из исполняемого кода в конструкторы/фабрики (тут есть вариации в зависимости от возможностей конкретного языка). Здесь Вы мыслите совершенно верно. Правда, действовать нужно без фанатизма, ибо если Code Smell «Switch Statements» не угрожает перерасти в «Divergent Change» или «Shotgun Surgery», то он большой угрозы не представляет.


      1. lair
        18.11.2019 17:52

        Тип стоит заводить не всегда, а тогда, когда это поможет сократить количество валидаций и получить дополнительную надежность.

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


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


        Потому что про ООП часто говорят, что это моделирование систем на основе наблюдаемого мира.

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


        (но вообще, опять же, практически любое программирование — это моделирование на основе наблюдаемого мира)


  1. somurzakov
    18.11.2019 03:03

    насколько я понял вопрос — компилятор гарантирует нам корректность типов на уровне языка, но не корректность типов на уровне бизнес логики. Т.е. мы можем объявить объект Кошелек как int и присвоить ему отрицательное значение или объявить объект Child с внешним ключом к несуществующему в базе Parent. В этом случае возникает вопрос, что делать:

    1. засовывать проверки на бизнес логику везде и не забывать обновлять ее в тысячах мест при каждом изменении бизнес логики. Можно делать if-ами, или бодренько-креативненько с подтипами как предложил автор. Можно вообще забить болт и дать базе данных проверять целостностью внешних ключей и выбрасывать исключение при попытке сохранить невалидный объект. Т.е. программист будет изо всех сил поддерживать консистентность и целостность данных в базе и каждое изменение логики будет требовать часов разработки на изменение N мест где эта логика описана, +тесты и если повезет — то все будет хорошо, но медленно.
    2. А можно не мусорить код этими проверками на бизнес-логику и сохранять эти бессмысленные объекты на стадии data ingestion. А на стадии presentation, выводить только консистентные и правильные данные с точки зрения бизнес логики. Т.е. проверка будет только перед выводом

    я думаю каждый выбирает что ему по душе, с точки зрения — что будет лучше в данном конкретном проекте по сложности. Если много изменений в бизнес-логике — то лучше это место консолидировать в одном месте, чтобы менять оттуда и тестировать ее.
    Конечно лучше же предотвращать попадание невалидных данных в систему вообще и проверки выполнять перед изменением или сохранением объекта. Это значит, что любое действие с данными на изменение должно проверяться. Что модуль веб-формы, что контроллер rest api, и даже скрипт миграции или maintenance который написал DBA


  1. adictive_max
    18.11.2019 04:41

    Согласитесь, что теперь проблема гораздо яснее. Перед нами каноничное нарушение принципа подстановки Лисков.
    Не соглашусь. Пример целенаправленно искусственно сконструирован, чтобы нарушать именно этот принцип. Если единственное ограничение «валидности» — это соответствие заранее известному списку типов, то этот список типов должен быть прописан в сигнатуре функции. А замените
    if (parent is Child)
    на
    if (parent.someField in [5..19])
    и всё сразу становится гораздо веселей. Для каждой функции, использующей parent, понятие «валидный» будет разным, возможно ещё и зависимым от контекста и/или значения других параметров. Соответственно для каждой нужно будет городить отдельный набор подтипов, и то это применимо сильно не всегда.

    Эту идею можно расширить до задаваемых пользователем ОДЗ. Снабжение объектов метаданными, содержащими ОДЗ, хранящимися в типе, устранит описанные выше проблемы. Хорошо бы получить поддержку такого средства в языке, но такое поведение реализуемо и в «обычных» ОО-языках, таких как Java или C# с помощью наследования и фабрики.
    Вообще, такое уже есть. Называется «контрактное программирование». Из JVM-языков нативно есть в Scala, Clojure и сейчас пилят в Kotlin. И в C# есть.

    Так же в статье не хватает примера. Пусть на вход к нам поступают некоторые пути файлов… Можно эту проверку кешировать в булевом поле, но это нас не избавит от самого факта необходимости проверки. Я предлагаю ответственность проверки переложить с разработчика на компилятор.
    А компилятор как-то сможет проверить, что файл может меняться со временем независимо от кода компилируемой программы?


    1. SanQri Автор
      18.11.2019 10:37

      Для каждой функции, использующей parent, понятие «валидный» будет разным

      Именно! И для каждого надо определять подтип, если такая «валидность» встречается много раз. В этом на самом деле ничего страшного нет.

      А компилятор как-то сможет проверить, что файл может меняться со временем независимо от кода компилируемой программы?

      Не поможет, но сохранив метаданные в типе, мы не сможем передать в метод невалидные данные.


  1. Ryppka
    18.11.2019 09:06

    Если данные — «просто данные», то на уровне конкретного вызова невозможно решить, делать валидацию или нет. Обычно решают на уровне дизайна: валидацию проводят интерфейсные функции, принимающие внешние данные, а внутри — «демилитаризованная зона».
    А если мы говорим об ООП, то LSP обязано выполнятся. Или это не ООП. Контроль за соблюдением инвариантов класса (т.е. валидацию) возлагается на конструкторы/фабрики. Невалидного экземпляра в рантайме быть не может и проверять нет необходимости, это делает система типов.
    По-моему так (С) Винни-Пух


    1. MonkAlex
      18.11.2019 09:12
      +1

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


    1. VolCh
      18.11.2019 10:57
      +1

      Невалидного экземпляра в рантайме быть не может

      Экземпляр может быть валидным в одном контексте и невалидным в другом. Особенно где-то на границе слоев такое часто, где часто используется рефлексия для гидрации объектов, например при чтении из базы. Для ORM всё валидно, а вот для BL может оказаться нет. Или ситуация присвоения ID при записи сущности в базу.


  1. Ryppka
    18.11.2019 09:34

    С точки зрения пользователя объект может быть невалидным, хотя с точки зрения типов — всё норм.

    Вы считаете, что у правильно сконструированного типа может быть некое невалидное состояние и пребывание экземпляра в нем является законным в рамках жизненного цикла экземпляра? Не уверен, что это можно выразить через иерархию наследования и да, проверять придется много где: как с null, Optional, Either etc.
    Плюс, всегда есть процесс — когда объект между двумя валидными состояниями. И в бизнес-кейсах этот процесс бывает не всегда атомарен, не всегда выполняется быстро.

    Если объект может изменять свое состояние невидимым локально образом, то это проблемы конкуретности, и решать их надо с помощью синхронизации, демультиплексирования и т.д. Это не имеет отношения к типам и наследованию, другой аспект. Для всех потоков управления изменения объекта должны быть атомарны (не обязательно за счет блокировки, можно более хитрым способом, например чере CAS), либо поток должен владеть объектом эксклюзивно. Прочее — баги конкрурентности.


  1. adictive_max
    18.11.2019 12:35
    +1

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


    1. SanQri Автор
      18.11.2019 12:40

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


    1. Ryppka
      18.11.2019 14:29

      Не совсем так, комбинаторный взрыв возникает, если пытаться это сделать через наследование. Тут вообще ООП не при делах. Если «объект» может переходить из «валидного» в «невалидный» и обратно — значит он сам или его части то есть, то их нет. Выражается через option, ну или ее минималистский вариант null. Ну и так далее…


  1. 0xd34df00d
    18.11.2019 15:04
    +3

    Чего только люди не придумывают, лишь бы зависимые типы не использовать.


  1. lorc
    18.11.2019 15:10
    +2

    Кажется, вы пытаетесь построить то что называется зависимый тип.

    UPD: Я буду обновлять комментарии перед постингом.


    1. SanQri Автор
      18.11.2019 16:07
      +2

      Спасибо, что открыли для меня название этой штуки. Вообще я пришел к идее этой статьи, как к частному от идеи обобщения Optional'ов из Swift'а. У меня появилась идея того, что оказывается называется зависимыми типами и я хотел написать на эту тему свою дипломную работу. Я пару месяцев лениво поискал язык, реализующий эту идею и не нашел. Хотя я даже не знал что писать в запрос в поисковике :)

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

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

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


      1. lorc
        18.11.2019 16:13
        +1

        Самый популярный из языков, который поддерживает завтипы — это Idris, и 0xd34df00d — пророк его. А вообще, статья про завтипы на википедии содержит отсылки и к другим языкам.


        1. SanQri Автор
          18.11.2019 16:19
          +2

          Понял. Тогда подумаю что еще можно поделать в этом мире. Не зря написал этот пост. Помимо прочего нашел по этой теме статьи у 0xd34df00d. Изучу и сделаю выводы


  1. michael_vostrikov
    18.11.2019 15:34

    Связь с принципом подстановки подмечена верно. Это похоже на наследование квадрата и прямоугольника. То есть у нас есть Rectangle, но при некоторых значениях полей он также является Square. В языках программирования (императивных, известных мне) не хватает возможности преобразовать один тип в другой без создания новой структуры данных в оперативной памяти. Было бы удобнее, если данные будут одни и те же, а поведение им можно задать разное.


    Или другой пример — на входе объект типа Request, после проверок он преобразуется в ValidAPIRequest, далее в ValidCreateOrderRequest. Чем дальше вглубь бизнес-логики, тем более специфичный тип используется, что означает, что он прошел всю предварительную специфичную обработку, и внутри функций, принимающих его на вход, валидность можно не проверять. А снаружи не прошедший проверки объект нельзя передать. А сейчас надо на каждый такой тип создавать новый объект и перебрасывать данные из менее специфичного объекта.


  1. lair
    18.11.2019 17:57

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

    … и что, критерии доступности везде одинаковые?


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

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


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

    Не получится, потому что компилятор не может проверить доступность пути.


    1. SanQri Автор
      18.11.2019 18:24
      +1

      … и что, критерии доступности везде одинаковые?

      Это в сущности не имеет значения. Могут быть и разные. Выделять подтип не обязательно.

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

      Делая проверки на низком уровне мы получим n проверок в таком случае
      let variable = SomeFactory.generate();
      test1ForSpecificValue(variable);
      test2ForSpecificValue(variable);
      ...
      testnForSpecificValue(variable);

      Делая проверки на высоком уровне, мы сделаем одну проверку не потеряв в надежности. Код на свифте:
      if let variable = SomeFactory.generate() as? SpecificType {
          test1ForSpecificValue(variable);
          test2ForSpecificValue(variable);
          ...
          testnForSpecificValue(variable);
      }


      Не получится, потому что компилятор не может проверить доступность пути.

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


      1. lair
        18.11.2019 18:30

        Выделять подтип не обязательно.

        Подождите, вы же приводите это как пример того, когда выделять подтип надо?


        Делая проверки на низком уровне мы получим n проверок в таком случае

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


        Делая проверки на высоком уровне, мы сделаем одну проверку не потеряв в надежности.

        … и то, что доступность файла может поменяться, вас не волнует? А то, что файловая система все равно сделает эту проверку?


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

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


        1. 0xd34df00d
          18.11.2019 18:51

          … и то, что доступность файла может поменяться, вас не волнует? А то, что файловая система все равно сделает эту проверку?

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


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

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


          1. lair
            18.11.2019 18:55

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

            Это как раз в обратную сторону, и об этом я написал.


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

            А можно пример?


            1. 0xd34df00d
              18.11.2019 19:07

              А можно пример?

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


              Давайте я вам лучше ссылки на проверяемую компилятором сортировку дам или там, не знаю, нахождение НОД?


              1. lair
                18.11.2019 19:18

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


                1. 0xd34df00d
                  18.11.2019 19:23

                  Не обязательно (а ещё понятие чистой парадигмы бессмысленно, важен только контроль эффектов, но не будем об этом). Это значит, что ваши операции с ФС должны быть в известном смысле атомарны. Вы не можете проверить права на доступ к файлу там, а потом считать его содержимое здесь — это может быть другой файл, как вы абсолютно верно заметили! А это значит, что надо проверять и считывать одновременно (не знаю, правда, позволяют ли это ФС — может, вся затея бессмысленна и принципиально нереализуема).


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


                  1. sshikov
                    18.11.2019 19:33

                    >А это значит, что надо проверять и считывать одновременно (не знаю, правда, позволяют ли это ФС — может, вся затея бессмысленна и принципиально нереализуема).
                    Во множестве разных ФС вы обычно получите что-то типа ошибки, если попытаетесь считать файл, и у вас нет доступа. Но далеко не факт, что контекст этой ошибки позволит вам точно ответить, каких именно прав нет.

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

                    Не то чтобы бессмысленна, но боюсь что на реальных ФС — если и реализуема, то весьма и весьма нетривиально.


                    1. 0xd34df00d
                      18.11.2019 19:41

                      Во множестве разных ФС вы обычно получите что-то типа ошибки, если попытаетесь считать файл, и у вас нет доступа.

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


                  1. lair
                    18.11.2019 21:24

                    Это значит, что ваши операции с ФС должны быть в известном смысле атомарны. Вы не можете проверить права на доступ к файлу там, а потом считать его содержимое здесь

                    … и это противоречит задумке автора поста "сначала проверим, а потом будем пользоваться результатами проверки".


                    И вот смотрите, вы ещё даже не начали писать с завтипами, а у вас уже от них профит

                    Это у меня не от завтипов профит, а от привычки думать.


                    1. 0xd34df00d
                      18.11.2019 21:58

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

                      Почему же? Вы можете хоть сразу после прочтения файла проверить, хоть прямо перед вызовом функции (например, каждый раз в цикле). Можете вообще не проверять в рантайме, если пишете тест, ФС у вас моковая, и мок статически даёт соответствующее доказательство. Но доказательство проверки у вас быть обязано.


            1. 0xd34df00d
              18.11.2019 19:20

              Хотя, впрочем… Ну вот если банально и тупо делать.


              Пусть у вас результат чтения файла (или какой-то другой операции с файлом) выражается как


              record FileResult where
                construct MkFileResult
                filename : String
                contents : Whatever
                size : Nat
                owner : Nat   -- численный uid пользователя
                permissions : Perms

              Тогда тип функции, которая берёт результат операции, и которой нужна проверка, выглядит как


              doSmth : (fr : FileResult) -> (prf : owner fr = 1000) -> ...

              или даже


              record User where
                constructor MkUser
                uid : Nat
                name : String
              
              doSmthAsUser : (u : User)
                          -> (fr : FileResult)
                          -> (userMatches : uid u = owner fr)
                          -> (wannabeSshCheck : So (onlyUserCanRead (permissions fr)))
                          -> ...


              1. lair
                18.11.2019 21:23

                Ну вот видите, у вас "текущий юзер" — это параметр. Я об этом и говорил.


                1. 0xd34df00d
                  18.11.2019 21:59

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


  1. torgeek
    18.11.2019 18:48

    Историю вопроса можно описать примерно так:
    1980-е – задаваемые области допустимых значений, пример – подтипы в Аде.
    1990-е – контракты-интерфейсы-наследование, начиная с Эйфеля и до Котлина/Раста сегодня.
    2000-е – зависимые типы, которые пока только Идрисе – очень крутом и популярном в очень узком кругу языке.


    1. 0xd34df00d
      18.11.2019 18:54

      При всей моей любви к идрису, он далеко не первый. Лет за 10-15 до него была (и есть) агда, лет за 10-15 до агды — Coq, а лет за 10-20 до него всякие automath (хотя тогда с теорией завтипов было все очень плохо, но это, наверное, первые попытки реализации proofs as types/propositions as terms).


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


      А ещё теория типов идриса несовместима с HoTT, потому что axiom K с ней несовместима, но то такое.


      1. torgeek
        18.11.2019 18:57

        Этак мы в 1930-е провалимся ))

        И я не про первый, а про достаточно известный/любимый.