Задание инвариантов для конструкторов значений

Question

Рассмотрим следующее

data Predicate = Pred Name Arity Arguments

type Name      = String
type Arity     = Int
type Arguments = [Entity]
type Entity    = String

Это позволит создать

Pred "divides" 2 ["1", "2"]
Pred "between" 3 ["2", "1", "3"]

но и "нелегал"

Pred "divides" 2 ["1"]
Pred "between" 3 ["2", "3"]

"Недопустимо", поскольку арность не соответствует длине списка аргументов.

Если не использовать такую ​​функцию

makePred :: Name -> Arity -> Arguments -> Maybe Predicate
makePred n a args | a == length args = Just (Pred n a args)
                  | otherwise = Nothing

и только экспортируя makePred из модуля Predicate, есть ли способ обеспечить правильность конструктора значений?

Answer 1

Что ж, простой ответ - отбросить арность из умного конструктора.

makePred :: Name -> Arguments -> Predicate
makePred name args = Pred name (length args) args

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

Не существует прямого способа применения этого инварианта.То есть вы не сможете получить makePred 2 ["a","b"] для проверки типов, но makePred 2 ["a","b","c"] - нет.Для этого вам нужны реальные зависимые типы.

В середине есть места, чтобы убедить haskell в принудительном применении ваших инвариантов с использованием расширенных возможностей (GADT s + фантомных типов), но после написания целого решения я понялЯ на самом деле не отвечал на ваш вопрос, и что такие методы не совсем применимы к этой проблеме, в частности.Как правило, они доставляют больше хлопот, чем стоят вообще.Я бы придерживался умного конструктора.

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

Answer 2

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

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

Примерно так (НЕПРОВЕРЕНО)

data Entity = Str String | Numeric Int

class Predicate a where
    name :: a -> String
    arity :: a -> Int
    args :: a -> [Entity]
    satisfied :: a -> Bool

data Divides = Divides Int Int
instance Predicate Divides where
    name p = "divides"
    arity p = 2
    args (Divides n x) = [(Numeric n), (Numeric x)]
    satisfied (Divides n x) = x `mod` n == 0

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