Ограничения корректности кодирования непосредственно в системе типа Haskell?

Ответ 1

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

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

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

newtype Raw a = Raw a

Затем убедитесь, что все ваши функции для ввода ввода от пользователя возвращают значения Raw вместо обычных строк. Наконец, вам нужна только санитационная функция:

sanitize :: Raw String -> String

Так как нормальные функции принимают String, а не Raw, вы не сможете случайно пройти в unsanitized строку. И поскольку мы определили Raw с помощью newtype, у него вообще нет служебных ресурсов во время выполнения.

Yesod, одна из основных веб-фреймворков Haskell, использует метод, подобный этому, для предотвращения внедрения SQL. В нем также есть несколько других интересных подходов, таких как использование системы типов для предотвращения неработающих ссылок в вашей базе данных; вы должны проверить это.

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

data Z
data S n

(Мы используем Peano Arithmetic на уровне типа здесь.) Идея проста: Z равно 0, а S - функция-преемник, поэтому S Z равно 1, S (S Z) равно 2 и т.д.

Теперь мы можем написать функцию умножения безопасной матрицы:

matMul :: Mat a b -> Mat b c -> Mat a c

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

Умножение матрицы с типом имеет более подробную информацию.

Ответ 2

Ну, на мой взгляд, одна из тех вещей, которые, как вы видели, часто не раскрываются, заключается в том, что эта информация о правильности по типу часто бывает такой, которая не происходит "естественно", а скорее происходит от использования методов для разработки ваших типов, которые не очевидны для программистов, которые приходят с других языков. Один из моих любимых примеров - страница Wiki Haskell в phantom типах; если вы посмотрите раздел 1 на этой странице, у них есть этот пример (какой IMO должен быть объявлением newtype вместо data):

data FormData a = FormData String

Что делает a? Ну, что он делает, это искусственно делает так, что FormData "foo" :: FormData Validated и FormData "foo" :: FormData Unvalidated, несмотря на то, что они "действительно" одинаковы, теперь имеют несовместимые типы, и поэтому вы можете заставить свой код не смешивать один и другой. Ну, позвольте мне не повторять то, что говорит страница, это относительно легко читать (по крайней мере, раздел 1).

Более сложный пример, который я использовал в одном из моих проектов on-off-off: OLAP гиперкубы можно увидеть как тип массива, индексированный не целыми индексами, а скорее объектами модели данных, такими как люди, дни, линейки продуктов и т.д.:

-- | The type of Hypercubes.
data Hypercube point value = ...

-- | Access a data point in a hypercube.
get :: Eq point => Hypercube point value -> point -> value

-- | This is totally pseudocode...
data Salesperson = Mary | Joe | Irma deriving Eq
data Month = January | February | ... | December deriving Eq
data ProductLine = Widget | Gagdet | Thingamabob

-- Pseudo-example: compute sales numbers grouped by Salesperson, Month and
-- ProductLine for the combinations specified as the "frame"
salesResult :: HyperCube (Salesperson, Month, ProductLine) Dollars 
salesResult = execute salesQuery frame
    where frame = [Joe, Mary] `by` [March, April] `by` [Widgets, Gadgets]
          salesQuery = ...

-- Read from salesResult how much Mary sold in Widgets on April.
example :: Dollars
example = get salesResult (Mary, April, Widgets)

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

badExample :: Dollar
badExample = get salesResult (Irma, January, Thingamabob)

Одно из возможных решений этого - сделать операцию get return Maybe value вместо просто value. Но мы можем сделать лучше; мы можем спроектировать API, где Hypercube может быть задан только вопрос о значениях, которые он содержит. Ключ похож на пример FormData, но более сложный вариант. Сначала мы вводим этот тип phantom:

data Cell tag point = Cell { getPoint :: point } deriving Eq

Теперь мы переформулируем Hypercube и get как тег-чувствительные. Я намереваюсь сделать это более конкретным в этом переформулированном примере. Начнем с этого:

{-# LANGUAGE ExistentialTypes #-}

data AuxCube tag point value = 
    AuxCube { getFrame :: [Cell tag point]
            , get :: Cell tag point -> value }

-- This is using a type system extension called ExistentialTypes:
data Hypercube point value = forall tag. Hypercube (AuxCube tag point value)

-- How to use one of these cubes.  Suppose we have:
salesResult :: Hypercube (Salesperson, Month, ProductLine) Dollars 
salesResult = execute salesQuery points
    where points = [Joe, Mary] `by` [March, April] `by` [Widgets, Gadgets]
          salesQuery = ...

-- Now to read values, we have to do something like this:
example = case salesResult of
              Hypercube (AuxCube frame getter) -> getter (head frame)

Извиняюсь, если использование ExistentialTypes смущает вас здесь, но, чтобы сделать длинную историю коротким, то, что он делает в этом примере, в основном состоит в том, что каждый Hypercube содержит AuxCube с уникальным параметром типа анонимного тега, так что теперь нет двух Hypercube может иметь Cell того же типа. По этой причине, если мы используем модульную систему для предотвращения создания вызывающих абонентов Cell s, вызывающие абоненты не могут запросить Hypercube для Cell, чтобы у него не было значения.

Кредиты: Я узнал эту технику, спросив здесь о переполнении стека.