1

对于我的 Haskell 主题，我有一个来自 uni 的延续练习，其中我得到了以下内容：

data Expr = Con Value
          | And Expr Expr

data Value = IntValue  Int
           | BoolValue Bool

est :: Expr -> Val
est (Con v) = v
est (And x y) = 
  case (est x, est y) of
    (BoolValue bool1, BoolValue bool2) -> BoolValue $ bool1 && bool2
    _                    -> error "And: expected Boolean arguments"

而且我不确定它的真正作用。它似乎是 中定义的术语的评估者Expr。有人可以向我解释一下吗？我的练习涉及我将其转换为我所做的 GADT：

data Expr e where
  Con :: Val -> Expr Val
  And :: Expr e -> Expr e -> Expr e

现在他们要求我静态实现以下内容并使其类型安全：

est :: Expr e -> e
est _ = -- implement this
4

2 回答 2

4

我认为您的 GADT 走错了路。要了解原因，我们将首先查看无类型版本Expr及其评估器（您问题的第一部分）。

Expr以下是您可以构造的几个类型值：

expr1 = Con (IntValue 42)
expr2 = Con (BoolValue True)
expr3 = Con (BoolValue False)

到目前为止，一切都很好：expr1表示整数常量 42，expr2以及expr3布尔常量True和False. Expr作为最外层构造函数的所有类型的值Con基本上都是这样的。

当我们将And构造函数添加到组合中时，事情开始变得有趣：

expr4 = And (Con (BoolValue True)) (Con (BoolValue True))
expr5 = And (Con (BoolValue True)) (And (Con (BoolValue False)) (Con (BoolValue False)))
expr6 = And (Con (BoolValue True)) (Con (IntValue 42))

expr4并且expr5很好；它们分别代表表达式True && True和True && (False && False)。我们希望他们能够评估True和False，但很快就会有更多。但是，expr6看起来很可疑：它代表了True && 42没有意义的表达式（至少在 Haskell 中！）。

到目前为止，我们看到的表达式，除了数字 6，都有一个值：expr1具有整数值 42，其余是布尔值（True对于s False2到5）。如您所见，这些值要么是整数，要么是布尔值，因此可以表示为 type 的值。TrueFalseexprValue

我们可以编写一个求值器，它接受一个Expr并返回它的Value. 换句话说，求值器应该返回一个常量表达式的值，如果表达式是一个逻辑“与”，它应该返回组成表达式的值的逻辑“与”，这需要是布尔值——你不能取and整数和布尔值或两个整数的逻辑。在代码中，这转化为

est :: Expr -> Value -- takes an Expr and returns its Value
est (Con value) = value -- the value of a constant expression is the wrapped value
est (And e1 e2) = let value1 = est e1 -- the value of the first operand
                      value2 = est e2 -- the value of the second operand
                  in logicalAndValue value1 value2

logicalAndValue :: Value -> Value -> Value
logicalAndValue (BoolValue b1) (BoolValue b2) = BoolValue (b1 && b2)
logicalAndValue (BoolValue b1) (IntValue i2)  = error "Can't take the logical 'and' of a boolean and an integer" 
logicalAndValue (IntValue i1)  (BoolValue b2) = error "Can't take the logical 'and' of an integer and a boolean"
logicalAndValue (IntValue i1)  (IntValue i2)  = error "Can't take the logical 'and' of two integers"

这只是第一个更详细的版本，将est两个评估表达式的逻辑“与”分离到一个单独的函数中，并提供更多信息的错误消息。

好的，希望这能回答您的第一个问题！问题归结为这样一个事实，即Expr值可以具有布尔值或整数值，并且您无法再“看到”该类型，因此可以将And两个表达式放在一起，这对此没有意义。

解决此问题的一种方法是拆分Expr为两种新的表达式类型，一种具有整数值，另一种具有布尔值。这看起来像（我也会给出expr上面使用的 s 的等价物）：

data IntExpr = ConInt Int
expr1 :: IntExpr
expr1 = ConInt 42

data BoolExpr = ConBool Bool
              | AndBool BoolExpr BoolExpr
expr2 :: BoolExpr
expr2 = ConBool True
expr3 = ConBool False
expr4 = AndBool (ConBool True) (ConBool True)
expr5 = AndBool (ConBool True) (AndBool (ConBool False) (ConBool False))

有两件事值得注意：我们已经摆脱了Value类型，现在不可能构造等价物expr6- 这是因为编译器会拒绝其明显的翻译AndBool (ConBool True) (ConInt 42)（可能值得尝试一下），因为of a type error: ConInt 42is of typeIntExpr并且您不能将其用作AndBool.

求值器还需要两个版本，一个用于整数表达式，一个用于布尔表达式；让我们写吧！IntExpr应该有Int值，并且BoolExpr应该评估为Bools：

 evalInt :: IntExpr -> Int
 evalInt (ConInt n) = n

 evalBool :: BoolExpr -> Bool
 evalBool (ConBool b) = b
 evalBool (AndBool e1 e2) = let v1 = evalBool e1 -- v1 is a Bool
                                v2 = evalBool e2 -- v2 as well
                            in v1 && v2

可以想象，当您添加更多类型的表达式（如、Char列表、Double提前...

这就是 GADT 的用武之地！我们不会为评估的每个可能的结果类型（IntExpr及BoolExpr以上）创建单独的表达式类型，而是将表达式类型本身“标记”为它将评估为的类型。因此，我们将确定评估类型值的结果Expr Int将是 anInt并且 aExpr Bool将给我们 a Bool。实际上，我们将让编译器为我们进行类型检查，而不是在运行时进行（如logicalAndValue上面的函数）。

目前，我们只有两种构造表达式的方法：创建一个常量表达式，以及将两个布尔值“和”在一起。第一种方式是这样工作的：如果我们有一个Int，我们把它变成 a Expr Int，aBool变成 aExpr Bool等等。因此，“make constant expression”构造函数的类型签名将是：

Con :: v -> Expr v

第二个构造函数接受两个表示布尔值的表达式（因此这两个表达式的类型为Expr Bool）并返回另一个具有布尔值的表达式，即此构造函数的类型是

And :: Expr Bool -> Expr Bool -> Expr Bool

将这些部分放在一起，我们得到以下Expr类型：

data Expr e where
    Con :: v -> Expr v
    And :: Expr Bool -> Expr Bool -> Expr Bool

一些示例值：

expr1 :: Expr Int
expr1 = Con 42
expr2 :: Expr Bool
expr2 = Con True
expr3 :: Expr Bool
expr3 = Con False
expr4 :: Expr Bool
expr4 = And (Con True) (Con True)
expr5 :: Expr
expr5 = And (Con True) (And (Con False) (Con False))

再一次，等效的expr6没有通过类型检查器：它会是And (Con True) (Con 42)，但是Con 42是 a Expr Int，因此不能用作参数And- 它必须是 a Expr Bool。

评估器现在变得非常容易。给定一个Expr e（记住，这意味着它是一个具有 type 值的表达式e）它返回一个e. 常量表达式的值是常量本身，逻辑“与”表达式的值是操作数值的“与”，我们确信这些值是Bools。这给出了：

est :: Expr e -> e
est (Con v) = v
est (And e1 e2) = let b1 = est e1 -- this will be a Bool, since e1 is an Expr Bool
                      b2 = est e2 -- likewise
                  in b1 && b2

您给出的 GADT 直接等效于 untyped Expr，它仍然允许您构造“坏”值，例如And (Con (BoolValue True)) (Con (IntValue 42)).

通过去掉“Value”类型，我们可以更准确地说明表达式的类型；而不是说“表达式的类型是整数或布尔值，但我还不知道”并在评估表达式时遇到问题，我们从一开始就确保我们知道表达式值的类型并且我们不会以没有意义的方式将它们组合在一起。

我希望你已经做到了——所有这些类型、值和不同级别的表达式都会让人感到困惑！- 并且您将能够尝试Expr自己扩展类型和评估器。

简单的尝试是创建一个添加两个整数值的表达式，使用字符串或字符常量，或者创建一个带有三个参数的“if-then-else”表达式：第一个是布尔类型，第二个和第三个是相同的类型（但该类型可以是Int,Bool或Char其他类型）。

于 2012-04-28T10:25:53.783 回答
2

使用 GADT 的目的是确保所有表达式都通过构造进行良好类型化。这意味着如果你有一个Expr Int，你就知道它的类型是正确的并且它的计算结果是一个Int。

要强制执行此操作，您需要确保使用它们包含的类型标记常量表达式，以便Con 0具有类型Expr Intwhile Con Trueis Expr Bool。

Con :: v -> Expr v

同样，您需要确保And只能用于计算结果为 的表达式Bool。

And :: Expr Bool -> Expr Bool -> Expr Bool

这样，类似的东西Con 0 `And` Con 1甚至不会编译，因为常量的类型为Expr Intwhile Andrequires Expr Bool。

正确设置后，实施est :: Expr e -> e应该是一项微不足道的练习。

于 2012-04-28T09:53:15.163 回答