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

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

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"]

"незаконно", потому что arity не соответствует длине списка аргументов.

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

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

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

2 7
haskell constructor invariants

2 ответа:

Ну, простой ответ состоит в том, чтобы отбросить arity от умного конструктора.

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

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

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

Есть места в середине, чтобы убедить Хаскелла применить ваши инварианты, используя расширенные функции (GADTS + phantom types), но после написания полного решения я понял, что на самом деле не обращался к вашему вопросу, и что такие методы не применимы к этой проблеме в частности. Они обычно доставляют больше хлопот, чем стоят в целом. Я бы остался с умным конструктором.

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

6

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

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

Что-то вроде этого (непроверенное) 

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

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

0