haskell - 自动导出 SBV 中记录谓词的可证明

Question

我的数据类型如下

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`

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

Answer 1

至少可以减少出错的可能性:

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

不过还是很乏味。