Я работаю в критически важной для безопасности отрасли, и наши проекты программного обеспечения обычно предъявляют требования безопасности; вещи, которые мы должны продемонстрировать, что программное обеспечение делает с высокой степенью уверенности. Часто это негативы, такие как "не коррумпировать чаще, чем 1 в". (Я должен добавить, что эти требования вытекают из требований безопасности статистической системы).
Одним из источников коррупции явно являются ошибки кодирования, и я хотел бы использовать систему типов Haskell для исключения хотя бы некоторых классов этих ошибок. Что-то вроде этого:
Во-первых, вот наш критический элемент данных, который не должен быть поврежден.
newtype Critical = Critical String
Теперь я хочу сохранить этот элемент в некоторых других структурах.
data Foo = Foo Integer Critical
data Bar = Bar String Critical
Теперь я хочу написать функцию преобразования из Foo в Bar, которая гарантированно не будет конфликтовать с данными Critical.
goodConvert, badConvert :: Foo -> Bar
goodConvert (Foo n c) = Bar (show n) c
badConvert (Foo n (Critical s)) = Bar (show n) (Critical $ "Bzzt - " ++ s)
Я хочу, чтобы "goodConvert" напечатал проверку, но "badConvert" проверяет тип проверки.
Очевидно, что я могу не импортировать конструктор Critical в модуль, который выполняет преобразование. Но было бы намного лучше, если бы я мог выразить это свойство в типе, потому что тогда я могу составить функции, гарантирующие сохранение этого свойства.
Я попытался добавить типы phantom и "forall" в разных местах, но это не помогает.
Одна вещь, которая могла бы работать, заключалась бы в том, чтобы не экспортировать конструктор Critical, а затем
mkCritical :: String -> IO Critical
Поскольку единственное место, где создаются эти критические элементы данных, находится во входных функциях, это имеет смысл. Но я бы предпочел более элегантное и общее решение.
Edit
В комментариях FUZxxl предложил посмотреть Safe Haskell. Это похоже на лучшее решение. Вместо добавления модификатора "без коррупции" на уровне типа, который я изначально хотел, похоже, что вы можете сделать это на уровне модуля, например:
1: Создайте модуль "Критический", который экспортирует все функции типа Critical, включая его конструктор. Отметьте этот модуль как "небезопасный", поставив "{- # LANGUAGE Unsafe # -}" в заголовок.
2: Создайте модуль "SafeCritical", который повторно экспортирует все, кроме конструктора, и любые другие функции, которые могут быть использованы для повреждения критического значения. Отметьте этот модуль как "заслуживающий доверия".
3: Отметьте все модули, которые необходимы для обработки критических значений без коррупции как "безопасные". Затем используйте это, чтобы продемонстрировать, что любая функция, импортированная как "безопасная", не может вызвать повреждение Критического значения.
Это оставит меньшую часть кода, например код ввода, который анализирует критические значения, требующие дополнительной проверки. Мы не можем устранить этот код, но сокращение суммы, требующей детальной проверки, по-прежнему является значительной победой.
Метод основан на том, что функция не может придумать новое значение, если функция не возвращает его. Если функция получает только одно критическое значение (как в функции "преобразовать" выше), то это единственное, на что он может вернуться.
Более сложная вариация проблемы возникает, когда функция имеет два или более критических значения одного и того же типа; он должен гарантировать, чтобы не смешивать их. Например,
swapFooBar :: (Foo, Bar) -> (Bar, Foo)
swapFooBar (Foo n c1, Bar s c2) = (Bar s c1, Foo n c2)
Однако это может быть выполнено путем предоставления той же обработки содержащим структурам данных.
