这个Haskell程序是否提供了"免费定理"的例子？

Question

关于清单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的所有实现,可能要求公理(ta)=(t(getUI(ta)))成立.必须证明这适用于每个特定类型类实例声明.对于有限类型,这可以通过枚举所有可能性的程序来完成.对于无限类型,必须通过感应证明手动完成.

清单1是我尝试证明的.根据解决方案1,也许我错误地认为这需要免费定理!

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除了作为无限循环之外,不能实现.

我怀疑将你希望的公理编码为一种只能满足它的东西的类型是非常困难的.