Какова наилучшая практика для создания данных, которые удовлетворяют определенному свойству в QuickCheck?

Question

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

например

data Expr
    = LitI Int
    | LitB Bool
    | Add Expr Expr
    | And Expr Expr

data TyRep = Number | Boolean

typeInfer :: Expr -> Maybe TyRep
typeInfer e = case e of
    LitI _ -> Number
    LitB _ -> Boolean
    Add e1 e2 -> case (typeInfer e1, typeInfer e2) of
        (Just Number, Just Number) -> Just Number
        _ -> Nothing
    And e1 e2 -> case (typeInfer e1, typeInfer e2) of
        (Just Boolean, Just Boolean) -> Just Boolean
        _ -> Nothing

Теперь мне нужно определить генератор Expr (т.е. Gen Expr или же instance Arbitrary Expr), но также хотят, чтобы он генерировал правильные типы (т.е. isJust (typeInfer generatedExpr))

наивный способ сделать это - использовать suchThat отфильтровать недействительные, но это явно неэффективно, когда Expr а также TyRep усложняется с большим количеством случаев.

Другая похожая ситуация касается ссылочной целостности, например

data Expr
    = LitI Int
    | LitB Bool
    | Add Expr Expr
    | And Expr Expr
    | Ref String -- ^ reference another Expr via it's name

type Context = Map String Expr

В этом случае мы хотим, чтобы все ссылочные имена в сгенерированном Expr содержатся в некоторых конкретных Contextтеперь я должен генерировать Expr для конкретного Context:

arbExpr :: Context -> Gen Expr

но теперь проблема с сжатием будет проблемой, и чтобы решить эту проблему, я должен определить конкретную версию сжатия и использовать forAllShrink каждый раз, когда я использую arbExprэто значит, много работы.

Итак, я хочу знать, есть ли лучшая практика, чтобы делать такие вещи?

Answer 1

Для хорошо типизированных терминов во многих случаях простой подход состоит в том, чтобы иметь один генератор для каждого типа или, что эквивалентно, функцию TyRep -> Gen Expr, Добавляя переменные поверх этого, это обычно превращается в функцию Context -> TyRep -> Gen Expr,

В случае генерации терминов с переменными (и без или с очень простыми типами), индексирование типа терминов по контексту (например, как вы бы сделали, используя bound библиотека) должно сделать довольно просто получить генератор в общем.

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

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

---

Для более продвинутой техники / связанной литературы, с моими собственными комментариями о возможном использовании ее в Haskell:

• Генерация ограниченных данных с равномерным распределением, Claessen и др., FLOPS'14 ( PDF). Я полагаю, что ленивый поиск в пакете Haskell имеет большинство механизмов, описанных в статье, но, похоже, он нацелен на перечисление, а не на случайную генерацию.

• Создание случайных суждений: автоматическая генерация хорошо типизированных терминов из определения системы типов, Fetscher et al., ESOP'15 ( PDF), название говорит само за себя. Я не знаю о реализации на Haskell; Вы можете спросить авторов.

• Удача новичка: язык для генераторов на основе свойств, Лампропулос и др., POPL'17 ( PDF) (отказ от ответственности: я соавтор). Язык свойств (точнее, функций T -> Boolнапример, проверка типов), которая может быть интерпретирована как случайные генераторы (Gen T). Синтаксис языка сильно вдохновлен Haskell, но есть еще несколько отличий. Реализация имеет интерфейс для извлечения сгенерированных значений в Haskell ( github repo).

• Генерация хороших генераторов для индуктивных отношений Лампропулосом и соавт. POPL'18 ( PDF). Это в Coq QuickChick, но привязка его к Haskell QuickCheck путем извлечения кажется разумно выполнимой.