2

我处于一种数据类型的情况

data X = X {foo :: SInteger, bar :: SInteger}

我想证明例如

forAll_ $ \x -> foo x + bar x .== bar x + foo x

使用haskell的sbv。这不会编译，因为X -> SBool它不是 Provable 的实例。我可以用例如使它成为一个实例

instance (Provable p) => Provable (X -> p) where
  forAll_ k = forAll_ $ \foo bar -> forAll_ $ k $ X foo bar
  forAll (s : ss) k =
    forAll ["foo " ++ s, "bar " ++ s] $ \foo bar -> forAll ss $ k $ X foo bar
  forAll [] k = forAll_ k
  -- and similarly `forSome_` and `forSome`

但这很乏味且容易出错（例如，在应该使用forSome时forAll使用）。有没有办法Provable为我的类型自动派生？

4

2 回答 2

4

它至少可以减少出错的可能性：

onX :: (((SInteger, SInteger) -> a) -> b) -> ((X -> a) -> b)
onX f g = f (g . uncurry X)

instance Provable p => Provable (X -> p) where
    forAll_  = onX forAll_
    forSome_ = onX forSome_
    forAll   = onX . forAll
    forSome  = onX . forSome

还有一个可推广的模式，以防 SBV 现有的最多 7 个元组的实例不够用。

data Y = Y {a, b, c, d, e, f, g, h, i, j :: SInteger}
-- don't try to write the types of these, you will wear out your keyboard
fmap10 = fmap . fmap . fmap . fmap . fmap . fmap . fmap . fmap . fmap . fmap
onY f g = f (fmap10 g Y)

instance Provable p => Provable (Y -> p) where
    forAll_  = onY forAll_
    forSome_ = onY forSome_
    forAll   = onY . forAll
    forSome  = onY . forSome

不过还是很乏味。

于 2016-10-11T18:45:17.140 回答
1

如果您真的想直接在 lambda 表达式中使用量词，丹尼尔的回答是“尽其所能”。Provable但是，我强烈建议free您为您的类型定义一个变体，而不是创建一个实例：

freeX :: Symbolic X
freeX = do f <- free_
           b <- free_
           return $ X f b

现在你可以像这样使用它：

test = prove $ do x <- freeX
                  return $ foo x + bar x .== bar x + foo x

这更容易使用，并且与约束很好地组合在一起。例如，如果您的数据类型具有两个组件都是正数的额外约束，并且第一个大于第二个，那么您可以这样编写freeX：

freeX :: Symbolic X
freeX = do f <- free_
           b <- free_
           constrain $ f .> b
           constrain $ b .> 0
           return $ X f b

请注意，这将在prove和sat上下文中正常工作，因为free知道如何在每种情况下正确表现。

我认为这更具可读性和更易于使用，即使它强制您使用 do-notation。您还可以创建一个接受名称的版本，如下所示：

freeX :: String -> Symbolic X
freeX nm = do f <- free $ nm ++ "_foo"
              b <- free $ nm ++ "_bar"
              constrain $ f .> b
              constrain $ b .> 0
              return $ X f b

test = prove $ do x <- freeX "x"
                  return $ foo x + bar x .== bar x * foo x

现在我们得到：

*Main> test
Falsifiable. Counter-example:
  x_foo = 3 :: Integer
  x_bar = 1 :: Integer

您还可以X通过 SBV 使“可解析”。在这种情况下，完整的代码如下所示：

data X = X {foo :: SInteger, bar :: SInteger} deriving Show

freeX :: Symbolic X
freeX = do f <- free_
           b <- free_
           return $ X f b

instance SatModel X where
  parseCWs xs = do (x, ys) <- parseCWs xs
                   (y, zs) <- parseCWs ys
                   return $ (X (literal x) (literal y), zs)

以下测试演示：

test :: IO (Maybe X)
test = extractModel `fmap` (prove $ do
                x <- freeX
                return $ foo x + bar x .== bar x * foo x)

我们有：

*Main> test >>= print
Just (X {foo = -4 :: SInteger, bar = -5 :: SInteger})

现在，您可以根据需要对反例进行后处理。

于 2016-11-23T05:15:37.850 回答