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与其他s进行交互IsTall,就像它们一样Bool,除非他们不会在没有明确演员的情况下与Bools和IsAlives进行交互.

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

---

ps我认为我已经通过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

如果稍微更改数据类型,可以将其作为Functor的实例,然后可以使用fmap对Boolean执行操作

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.

我不确定高度上的布尔运算是否有意义.你如何证明"高而短等于短"但"高或短等于高"的结论？

我建议你为你的连接词寻找不同的名字,然后你可以超载.

PS Haskell总是得到新的功能,所以我能说的最好的是,如果你可以超载,if我不知道它.要说Haskell"不能做到这样的事情"总是危险的......

Answer 3

你可以在某种程度上这一点,使用newtypeS和一类,如果你导入的前奏隐藏你想与你使用布尔函数IsTall和IsAlive值.您重新定义布尔函数作为类方法,为你做,然后为实例的所有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以帮助缓解此类问题.