此Haskell程序是否提供“免费定理！"的示例? [英] Does this Haskell program provide an example of "Theorems for free!"?

问题描述

关于清单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)))

其他上下文

该代码基于

The code is based on a paper where it is stated:

对于getUI的所有实现，可能需要公理(t a) =(t(getUI(t a)))成立.必须证明这适用于每个特定的类型类实例声明.对于有限类型，可以是 由列举所有可能性的程序完成.对于无限 类型，必须通过归纳证明手动完成.

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.

清单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程序是否提供“免费定理！"的示例?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！