HASKELL：验证打字机中的函数的每个实现都是交换的

发布于 2025-02-10 02:15:56 字数 893 浏览 2 评论 0原文

假设我们有一个函数f ::（t a）=＆gt; a - ＆gt; a - ＆gt; a - ＆gt;在Typeclass t中，类型类别具有多种类型的实例。假设我们希望此功能不管给定类型的实现如何，即 ∀a，b∈X：（tx，eq x）=＆gt; ∃f x - ＆gt; X - ＆GT; x，fab == fb a 如果我要验证更具体的情况的通勤性，请说（+）和int，我可以写下这样的内容：

import Test.Quickcheck (quickCheck)

commutativityProperty :: Eq a => (a -> a -> a) -> a -> a -> Bool
commutativityProperty f a b = f a b == f b a

main :: IO ()
main = do
  quickCheck (commutativityProperty (+) :: Int -> Int -> Bool)

QuickCheck不适合模棱两可的类型变量，因此我无法写下这样的内容： QuickCheck（commutativityproperty（+）::（num a，eq a）=＆gt; a - ＆gt; a - ＆gt; bool） 或者，对于更一般的情况： QuickCheck（commutativityProperty f ::（t a，eq a）=＆gt; a - ＆gt; a - ＆gt; bool） 问题是：在类似的上下文中，我知道此功能必须保持通勤性，而不论特定类型的实现如何，我如何验证这确实是正确的，而无需为实现F的每种类型编写Quickcheck行并必须维护该代码（即，每当创建具有T的新类型时，我都必须回来为该特定类型编写新行）吗？

原文

Suppose we have a function f :: (T a) => a -> a -> a -> in a typeclass T, typeclass which has instances in numerous types.
Suppose we want this function to be commutative regardless of its implementation for a given type, i. e.
∀ a, b ∈ X: (T X, Eq X) => ∃ f X -> X -> X, f a b == f b a
If I were to verify commutativity for a more concrete case, let`s say (+) and Int, I could write something like this:

import Test.Quickcheck (quickCheck)

commutativityProperty :: Eq a => (a -> a -> a) -> a -> a -> Bool
commutativityProperty f a b = f a b == f b a

main :: IO ()
main = do
  quickCheck (commutativityProperty (+) :: Int -> Int -> Bool)

quickCheck does not work with ambiguous type variables, so I could not write something like this:
quickCheck (commutativityProperty (+) :: (Num a, Eq a) => a -> a -> Bool)
Or, for the more general case:
quickCheck (commutativityProperty f :: (T a, Eq a) => a -> a -> Bool)
The Question is:
In a similar context, where I know this function must hold commutativity regardless of implementation for a specific type, how can I verify that this is indeed true without having to write a line of quickCheck for every type that implements f and have to maintain that code (i.e. every time a new type with an instance of T is created, I would have to come back and write a new line for that specific type)?

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

゛时过境迁 2025-02-17 02:15:56

想到了两种方法：

使用GADT生成随机类型

，您可以尝试生成“随机类型”，并将其用于测试您的多态函数。这并不是完全容易的，但是根据您的类型，它仍然可行。

给您一个非常粗略的草图：

data Ty t where
    TInt :: Ty Int
    TPair :: Ty a -> Ty b -> Ty (a,b)

data SomeType where
    ST :: Ty t -> SomeType

test :: SomeType -> (forall a . (T a) => a -> a -> a) -> Bool
test (ST TInt) f = f 4 2  -- actually, these should be generated randomly
test (ST (TPair x y)) f = ...

测试非全能类型的类型可能是免费的！

每当我们具有（终止）多态功能时，我们都会知道它可以满足一个称为 免费定理 （口号是“免费的”定理！”）。例如，如果我们具有f :: a-＆gt; a必须是身份，而g :: a-＆gt; a-＆gt; a必须是<代码> \ x y-＆gt; x 或\ x y-＆gt; y。添加像您的t a这样的类型约束使其更加复杂，但是仍然可以生成免费定理。

使用这种免费定理，您可能会证明，如果您的属性保留了整数，则必须在类t中保留任何类型的类型。我给你一个例子。

假设f :: ord a =＆gt; [a] - ＆gt; [a]正确分类整数。然后，通过自由定理，它也对任何其他完全有序的类型进行分类。直观地，这是因为f无法真正检查输入列表的元素，除了使用比较（＆lt;，比较，...）。因此，如果将列表元素替换为具有完全相同的比较结果的合适整数，则f必须在两个列表上执行“相同”操作。

您可能可以根据t类实际允许的方式玩相同的技巧。

Two approaches come to mind:

Generate random types

Using GADTs, you could try to generate a "random type" and use that for testing your polymorphic function. This is not entirely easy, but it could be still feasible depending on your typeclass.

To give you a very rough sketch:

data Ty t where
    TInt :: Ty Int
    TPair :: Ty a -> Ty b -> Ty (a,b)

data SomeType where
    ST :: Ty t -> SomeType

test :: SomeType -> (forall a . (T a) => a -> a -> a) -> Bool
test (ST TInt) f = f 4 2  -- actually, these should be generated randomly
test (ST (TPair x y)) f = ...

Testing non-integer types might come for free!

Every time we have a (terminating) polymorphic function, we know it satisfies a property called free theorem (the slogan is "theorems for free!"). E.g. if we have f :: a->a it has to be the identity, while g :: a->a->a has to be \x y->x or \x y->y. Adding a typeclass constraint like your T a makes it more complex, but a free theorem can still be generated.

It is likely that, using such a free theorem, you can prove that if your property hold for integers it has to hold for any type in class T. I'll give you an example.

Assume f :: Ord a => [a] -> [a] correctly sorts integers. Then, by the free theorem, it also sorts any other totally ordered type. Intuitively, this is because f can not really inspect the elements of the input list except using comparisons (<, compare,...). Hence, if you replace the list elements with suitable integers that have exactly the same comparison results, f must perform the "same" operation on both lists.

It is possible that you can play the same trick depending on what your T class actually allows.

回复收藏 0 原文