问题描述
关于清单1 ,要求类型级别的公理
With respect Listing 1, it is required that the type level axiom
(t a) = (t (getUI(t a)))
应作为每个特定类型类实例的一个定理推导.
should derivable as a theorem for every specific type class instance.
test
函数的编译是否证明类型级公理对于程序中的特定类型成立?汇编是否提供了免费的定理!的示例! ?
Does the compilation of the test
function prove the type level axiom holds for the particular types in the program? Does the compilation provide an example of Theorems for free!?
列出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)))
其他上下文
该代码基于 /p>
The code is based on a paper where it is stated:
清单1 是我的证明尝试.根据解决方案1,也许我错误地认为这需要定理免费!
Listing 1 was my attempt at a proof. In the light of Solution 1, perhaps I mistakenly thought this required Theorems for free!
推荐答案
不,它是一类,这一事实给您一个单独的类型留出了太多的回旋余地,无法保证该公理.例如,以下替代实例进行类型检查,但违反了您的公理:
No, the fact that it's a class gives you far too much leeway for the type alone to guarantee that axiom. For example, the following alternate instance typechecks but violates your axiom:
instance Category Continuant Int where
getUI _ = 42
(完全明确地说,我们的对手可以选择例如t=Continuant
和a=6*9
来违反公理.)这滥用了类实例化程序选择包含类型的事实.我们可以通过删除类的参数来删除该能力:
(Being completely explicit, our adversary could choose for example t=Continuant
and a=6*9
to violate the axiom.) This abuses the fact that the class instantiator gets to choose the contained type. We can remove that ability by removing that argument to the class:
class Category t where
getUI :: UI a => t a -> a
A,这还不够.我们可以写
Alas, even this is not enough. We can write
data Pair a = Pair a a
然后自由定理告诉我们,对于instance Category Pair
,我们必须编写以下两个定义之一:
and then the free theorem tells us that for instance Category Pair
, we must write one of the following two definitions:
getUI (Pair x y) = x
-- OR
getUI (Pair x y) = y
无论我们选择什么,我们的对手都可以选择t
,这表明我们的公理是错误的.
Whichever we choose, our adversary can choose a t
which shows us that our axiom is wrong.
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
的事实.如果我们删除了该功能,该怎么办...?
Okay, this abuses the fact that the class instantiator gets to choose t
. What if we removed that ability...?
class Category where
getUI :: UI a => t a -> a
这大大限制了Category
的实例化器.实际上,太多了:getUI
除了作为无限循环之类的东西之外,无法实现.
This restricts the instantiator of Category
quite a lot. Too much, in fact: getUI
can't be implemented except as an infinite loop or the like.
我怀疑很难将您希望的公理编码为只能由满足其要求的事物所居住的类型.
I suspect it will be very difficult to encode the axiom you wish for as a type which can only be inhabited by things that satisfy it.
这篇关于此Haskell程序是否提供“免费定理!"的示例?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!