Указание инвариантов в конструкторах значений

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

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, есть ли способ обеспечить правильность конструктора значений?


constructor haskell invariants
person Nickolay Kolev    schedule 26.01.2011    source источник
comment
Не в системе типов. Вам понадобится один из (даже) более причудливых (зависимые типы? Просто догадываюсь, я не совсем лучший постер LtU).   -  person    schedule 27.01.2011
comment
Зависимые типы действительно позволяют найти решение.   -  person I GIVE CRAP ANSWERS    schedule 27.01.2011
comment
Вероятно, вы можете получить что-то с помощью хака с естественными типами уровня, но это не очень хорошее решение.   -  person Alp Mestanogullari    schedule 27.01.2011
comment
Если я не ошибаюсь, Альп Местаногуллари имеет в виду haskell.org/haskellwiki/Type_arithmetic .   -  person gspr    schedule 27.01.2011
comment
использование такой функции - это именно то, что делает большинство людей. Он называется умным конструктором: haskell.org/haskellwiki/Smart_constructors   -  person porges    schedule 27.01.2011

Ответы (2)


arrow_upward
6
arrow_downward

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

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 применять ваши инварианты с использованием расширенных функций (GADTs + фантомные типы), но после написания всего решения я понял, что на самом деле я не ответил на ваш вопрос, и что такие методы на самом деле не применимы к этой проблеме в частности. Как правило, они также доставляют больше хлопот, чем пользы. Я бы придерживался умного конструктора.

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

person luqui    schedule 27.01.2011

arrow_upward
0
arrow_downward

Мне кажется, что если вы хотите, чтобы указанные ограничения были применимы, вы должны сделать 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

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

person Dan Burton    schedule 26.01.2011
comment
Это просто кодирование по кругу. Класс Predicate можно изоморфно представить как тип данных data Predicate = Predicate String Int [Entity] Bool, то же самое, но с меньшим количеством шаблонов, что в основном уже было в OP. См. lukepalmer.wordpress.com/2010/01/24/ для получения подробной информации. - person luqui; 27.01.2011