这个Haskell程序提供了“自由定理”（Theorems for free）的一个例子吗？

Question

这个Haskell程序提供了“自由定理”（Theorems for free）的一个例子吗？

3

关于清单1，需要满足类型层次公理。

(t a) = (t (getUI(t a)))

每个特定类型类实例都应该能够推导出一个定理。

test 函数的编译是否证明了程序中特定类型的类型级公理成立？编译是否提供了免费的定理！的示例？

清单1

{-# LANGUAGE MultiParamTypeClasses #-}
data Continuant a = Continuant a  deriving (Show,Eq)

class UI a where

instance UI Int where

class Category t a where
   getUI :: (UI a) => (t a) -> a

 instance Category Continuant Int where
    getUI (Continuant a) = a

 -- axiom (t a) = (t (getUI(t a))) holds for given types?
 test :: Int -> Bool
 test x =  (Continuant x) == (Continuant (getUI (Continuant x)))

附加背景

这段代码基于一篇论文，其中提到：

对于 getUI 的所有实现，我们可以要求公理 (t a) = (t (getUI (t a))) 成立。必须证明每个特定类型类实例声明都符合这个公理。对于有限类型，可以通过一个枚举所有可能性的程序来完成。对于无限类型，必须通过归纳证明手动完成。

清单1 是我的尝试证明。在解决方案1的光芒下，也许我错误地认为这需要自由定理！

- Patrick Browne

1

我认为“我该如何证明这个问题”是一个非常不同的问题，而且似乎在SO上会受到欢迎。请随意开启一个单独的问题。你可以先谷歌搜索“等式推理”（或者“等式推理 Haskell”）来看看是否阅读一些相关内容能够给你足够的提示让你自己取得进展。 - Daniel Wagner

@Daniel，我已经提出了建议的后续问题。 - Patrick Browne

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Daniel Wagner · Accepted Answer

不，它是一个类并不能仅凭类型就保证公理的正确性。例如，以下替代实例可以通过类型检查，但违反了您的公理：

instance Category Continuant Int where
    getUI _ = 42

要完全明确，我们的对手可以选择例如t=Continuant和a=6*9来违反公理。这滥用了类实例化程序可以选择包含类型的事实。我们可以通过删除该参数来删除该能力：

class Category t where
    getUI :: UI a => t a -> a

哎呀，即使这样还不够。我们可以编写：

data Pair a = Pair a a

然后自由定理告诉我们，对于 Category Pair 实例，我们必须编写以下两个定义之一：

getUI (Pair x y) = x
-- OR
getUI (Pair x y) = y

无论我们选择哪个，我们的对手都可以选择一个 t ，向我们展示我们的公理是错误的。

Our choice                 Adversary's choice
getUI (Pair x y) = x       t y = Pair 42 y; a = 6*9
getUI (Pair x y) = y       t x = Pair x 42; a = 6*9

好的，这种方法利用了类实例化器可以选择 t 的事实。如果我们删除了这个能力呢...？

class Category where
    getUI :: UI a => t a -> a

这会严重限制Category的实例化方法。实际上，过于严格了：除了无限循环等方式外，无法实现getUI。

我怀疑将您希望的公理编码为只能由满足其条件的事物所占据的类型将非常困难。