haskell - 这个 Haskell 程序是否提供 "Theorems for free!"的示例？

Question

关于 list 1，需要类型级公理

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

应该作为每个特定类型类实例的定理可推导。

test 函数的编译是否证明类型级公理适用于程序中的特定类型？编译是否提供了Theorems for free!的例子？

list 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)))

其他上下文

代码基于 paper声明的地方:

For all implementations of getUI one may require that the axiom (t a) = (t (getUI (t a))) holds. This must be proven to hold for every specific type class instance declaration. For finite types this can be done by a program that enumerates all possibilities. For infinite types this must be done manually via proofs by induction.

list 1 是我的证明尝试。根据解决方案 1，也许我错误地认为这需要 Theorems for free!

Answer 1

不，它是一个类的事实给了你太多的回旋余地来单独保证该公理。例如，以下替代实例类型检查但违反了您的公理:

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

然后自由定理告诉我们，对于instance 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 只能作为无限循环之类的实现。

我怀疑将您希望的公理编码为只能由满足它的事物所居住的类型来编码是非常困难的。