Haskell：具有逻辑上不同布尔值的类型安全

Question

假设我有以下代码

type IsTall = Bool
type IsAlive = Bool

is_short_alive_person is_tall is_alive = (not is_tall) && is_alive

稍后再说，我有以下内容

a :: IsAlive
a = False

b :: IsTall
b = True

并调用以下命令，以错误的方式获取两个参数：

is_short_alive_person a b

不幸的是，这成功编译，并且在运行时会找到高个子死人而不是矮个子人。

我希望上面的例子不要编译。

我的第一次尝试是：

newtype IsAlive = IsAlive Bool
newtype IsTall = IsTall Bool

但是我不能做类似的事情。

switch_height :: IsTall -> IsTall
switch_height h = not h

因为not没有在IsTalls上定义，只有Bools。

我可以一直明确地提取Bools，但这在很大程度上违背了目的。

基本上，我希望 IsTalls 与其他 IsTalls 互动，就像他们是 Bools 一样，除了他们不会在没有明确演员表的情况下与 Bools 和 IsAlives 互动.

实现这一目标的最佳方法是什么。

---

附言我想我已经通过在 GHC 中的数字实现了这一点：

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

newtype UserID = UserID Int deriving (Eq, Ord, Num)
newtype GroupID = GroupID Int deriving (Eq, Ord, Num)

（即 UserID 和 GroupID 不应交互）

但我似乎无法使用 Bools 执行此操作（导出 Bool 不起作用）。无论如何，我什至不确定以上是最好的方法。

Answer 1

如果您导入 Prelude 隐藏您想要与您的 IsTall 和 IsAlive 值一起使用的布尔函数，您可以使用 newtypes 和一个类来实现这一点。您将布尔函数重新定义为类中的方法，然后为所有 3 个 Bool、IsTall 和 IsAlive 类型创建实例。如果您使用GeneralizedNewtypeDeriving，您甚至可以获得IsTall 和IsAlive 实例，而无需手动编写包装/展开样板。

这是我在 ghci 中实际尝试过的示例脚本：

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

import Prelude hiding ((&&), (||), not)
import qualified Prelude

class Boolish a where
    (&&) :: a -> a -> a
    (||) :: a -> a -> a
    not :: a -> a

instance Boolish Bool where
    (&&) = (Prelude.&&)
    (||) = (Prelude.||)
    not = Prelude.not

newtype IsTall = IsTall Bool
    deriving (Eq, Ord, Show, Boolish)

newtype IsAlive = IsAlive Bool
    deriving (Eq, Ord, Show, Boolish)

您现在可以使用&&、|| 和not 这三种类型中的任何一种值，但不能同时使用。而且它们是独立的类型，因此您的函数签名现在可以限制它们要接受的 3 个中的哪一个。

在其他模块中定义的高阶函数可以正常工作，如下所示：

*Main> map not [IsTall True, IsTall False]
[IsTall False,IsTall True]

但是您将无法将IsTall 传递给在其他地方定义的需要Bool 的任何其他函数，因为其他模块仍将使用布尔函数的Prelude 版本。像if ... then ... else ... 这样的语言结构也仍然是一个问题（尽管 hammar 对 Norman Ramsey 的回答的评论说你可以用另一个 GHC 扩展来解决这个问题）。我可能会在该类中添加一个 toBool 方法，以帮助统一转换回常规 Bools 以帮助缓解此类问题。

Answer 2

如果你稍微改变你的数据类型，你可以让它成为一个 Functor 的实例，然后你可以使用 fmap 对布尔值进行操作

import Control.Applicative

newtype IsAliveBase a = IsAlive a 
newtype IsTallBase a = IsTall a 

type IsAlive = IsAliveBase Bool
type IsTall = IsTallBase Bool

instance Functor IsAliveBase where
    fmap f (IsAlive b) = IsAlive (f b)

instance Functor IsTallBase where
    fmap f (IsTall b) = IsTall (f b)

switch_height :: IsTall -> IsTall 
switch_height h = not <$> h -- or fmap not h

-- 编辑

对于 && 之类的操作，您可以将其设为 Applicative 的实例

instance Applicative IsAliveBase where
    pure = IsAlive
    (IsAlive f) <*> (IsAlive x) = IsAlive (f x)

然后您可以使用 liftA2 执行 (&&)

示例：

*Main> let h = IsAlive True
*Main> liftA2 (&&) h h 
IsAlive True

您可以在http://en.wikibooks.org/wiki/Haskell/Applicative_Functors阅读更多相关信息

Answer 3

您的选择是定义代数数据类型，例如

data Height = Tall | Short
data Wiggliness = Alive | Dead

或定义新的运算符，例如&&&、|||、complement，并在您选择的类型上重载它们。但即使重载，您也无法将它们与if 一起使用。

我不确定对高度的布尔运算是否有意义。您如何证明“高和矮等于矮”但“高或短等于高”的结论？

我建议你为你的连接词寻找不同的名字，然后你可以重载它们。

附： Haskell 总是在获得新功能，所以我能说的最好的就是如果你可以超载if 我不知道。说 Haskell 说“不能做某事”总是很危险的……