打印教堂布尔值 [英] Printing Church Booleans

问题描述

以下代码旨在将布尔型的Church编码打印为Haskell的Bool:

The following code is meant to print Church encoding of booleans as Haskell's Bool:

{-#LANGUAGE FlexibleInstances #-}

instance Show (t -> t -> t) where
  show b = show $ b True False

哪个会导致此错误:

<interactive>:4:21: error:
• Couldn't match expected type ‘t’ with actual type ‘Bool’
  ‘t’ is a rigid type variable bound by
    the instance declaration at <interactive>:3:10-27
• In the first argument of ‘b’, namely ‘True’
  In the second argument of ‘($)’, namely ‘b True False’
  In the expression: show $ b True False
• Relevant bindings include
    b :: t -> t -> t (bound at <interactive>:4:8)
    show :: (t -> t -> t) -> String (bound at <interactive>:4:3)

如何使其工作?

推荐答案

问题是show :: (t -> t -> t) -> String应该适用于 any 类型的 any 函数，而t .您假设t是布尔值，这是非法的，因为(根据GHC)"t是刚性类型变量"并且不能与专用类型统一.

The problem is that show :: (t -> t -> t) -> String should work for any function working on any type t. You are assuming that t is Boolean which is illegal, because (according to GHC) "t is a rigid type variable" and cannot be unified with specialized type.

一种可能的解决方案是通过Bool(必须使用FlexibleInstances)来专门化您的实例

One possible solution would be to specialize your instance by Bool (FlexibleInstances are necessary)

{-#LANGUAGE FlexibleInstances #-}

instance Show (Bool -> Bool -> Bool) where
  show b = show $ b True False

但是，这将降低您的教堂布尔值的通用性.

But this will reduce generality of your Church's boolean.

不可能定义适用于任何类型的灵活解决方案，因为您将需要具有该类型的两个代表来描述 true 和 false 情况，还有像Void这样的类型，它们没有(定义的)值.

It is impossible to define flexible solution that would work on any type, because you will need to have two representatives of that type that would describe true and false cases, and there are types such like Void which have no (defined) values.

我想到的一个非常普遍的想法是向t添加更多的类约束:

An idea that comes to my mind and is quite universal is to add few more class constraints to t:

{-#LANGUAGE FlexibleInstances #-}
import Data.Boolean

instance (Show t, Boolean t) => Show (t -> t -> t) where
  show b = show $ b true false

Boolean类收集在某些术语中可以理解为逻辑值的类型.例如Bool:

The Boolean class collects types that can be understood as logic values in some terms. For example for Bool:

instance Boolean Bool where
  true = True
  false = False
  notB = not
  (||*) = (||)
  (&&*) = (&&)

现在我们可以确保

• t是您实际上可以show
• 至少有两个类型为true和false的有效和不同的t值

• t is a thing that you can actually show
• There are at least two valid and different values of type t that appear as true and false

在哪种情况下才能真正以这种方式实现show此类签名的功能.

Which are the required circumstances to actually be able to show a function of such signature in this way.

重要

以下示例不起作用:

show (true :: (Show t, Boolean t) => t -> t -> t) 

问题在于类型检查器不会猜测您将在这里使用哪个t.该解决方案提供有效且有效的实例，但仅适用于完全实例化的类型.如果出现歧义错误，则需要指定什么是t:

The problem is that typechecker won't guess which t are you going to have here. This solution provides valid and working instance, but only for fully instantiated types. If you get ambiguity error, you will need to specify what is t:

show (true :: Bool -> Bool -> Bool)
>>> "True"

show (true :: Int -> Int -> Int)  -- assuming Boolean instance
>>> "1"

---

编辑:

但评论中提到了另一个想法.解决方案是用Rank2Type包裹您的Church布尔值:

Yet another idea was mentioned in the comments. The solution would be to wrap your Church boolean with Rank2Type:

{-# LANGUAGE Rank2Types #-}

newtype ChBool = ChBool (forall t. t -> t -> t)

这将使t是与上下文无关的任何类型.然后，您可以这样定义临时实例:

Which will let t be any type independent of the context. Then you may define casual instance like this:

instance Show ChBool where
  show (ChBool f) = show $ f True False

这篇关于打印教堂布尔值的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！