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不是在 IsTall s 上定义的，因此只有 Bool s。

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

基本上，我希望IsTall s与其他IsTall进行交互，就像它们是Bool s一样，除了它们不会在没有显式强制转换的情况下与Bool和IsAlive进行交互。

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

---

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

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
newtype UserID = UserID Int deriving (Eq, Ord, Num)
newtype GroupID = GroupID Int deriving (Eq, Ord, Num)

(即用户 ID 和组 ID 不应交互(

但我似乎不能用 Bool s 做到这一点(派生布尔不起作用(。无论如何，我什至不确定以上是最好的方法。

Answer 1

如果你稍微改变你的数据类型，你可以使它成为函子的实例，然后你可以使用 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 2

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

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

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

无论如何，我不确定对高度的布尔运算是否有意义。你如何证明"高矮等于矮"但"高或矮等于高"的结论？

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

P.S. Haskell总是在获得新功能，所以我能说的最好的是，如果你能超载if我不知道。 说哈斯克尔"某某做不了"总是危险的......

Answer 3

如果你

导入 Prelude 隐藏要与IsTall一起使用的布尔函数和 IsAlive 值，则可以使用 newtype s 和一个类来实现这一点。您将布尔函数重新定义为类中的方法，然后为类中的所有 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方法，以帮助统一转换回常规Bool以帮助缓解此类问题。