无类型的术语解释

Question

我有一个从单继续练习我的Haskell的主题，我一直在考虑以下几点：

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中定义的术语的评估者。有人可以向我解释吗？我的工作涉及我转换到这一点作为我已经做了GADTs：

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

现在，他们问我实现静态以下，并使其类型安全：

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

Answer 1

我认为你在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这是没有意义的（至少在哈斯克尔！）。

到目前为止，我们所看到的，除了编号6的表达，都具有一个值：expr1具有整数值42外，其余均为（对于expr第2至第5 True，False，True，False）布尔值。如您所见，这些值可以是整数或布尔值，因此可以表示为Value类型的值。

我们可以写一个评估器，它需要一个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)将被编译器拒绝（它可能值得尝试这一点），因为类型错误：ConInt 42是类型IntExpr并且您不能使用作为AndBool的第二个参数。

评估器还需要两个版本，一个用于整型表达式，一个用于布尔表达式;让我们写下它们！ IntExpr应该有Int值，并BoolExpr应该求Bool S：

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）或途径到表达式组合如两数相加，建设“如果”，其中的类型不是预先给定的表情，甚至变量...

---

这是GADTs进来！我们将不会为评估的每种可能的结果类型（上面的IntExpr和BoolExpr）分别使用一种表达式，而是将表达式类型本身与它将评估的类型进行“标记”。所以我们将确定评估类型Expr Int的值的结果将是一个Int和一个Expr Bool将给我们一个Bool。实际上，我们将让编译器为我们进行类型检查，而不是在运行时进行类型检查（如上面的函数logicalAndValue）。目前，我们只有两种构建表达式的方法：创建一个常量表达式，并将两个布尔值组合在一起。第一种方式是这样的：如果我们有一个Int，我们把它变成一个Expr Int，一个Bool变成Expr Bool等等。因此，对于“使常量表达式”构造类型签名将是：

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相当于未通过typechecker：这将是And (Con True) (Con 42)，但Con 42是Expr Int，因此不能被用作一个参数And - 它需要是一个Expr Bool。

现在评估者变得确实容易。给定一个Expr e（记住，这意味着它是一个表达式，其值为e），它返回一个e。常量表达式的值本身就是常量，逻辑“和”表达式的值是操作数值的“和”值，我们确信这些值是Bool s。这给：

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是无类型Expr的直接等同，它仍然会允许你建立“坏”的值，例如And (Con (BoolValue True)) (Con (IntValue 42))。

通过摆脱'Value'类型，我们可以更精确地说明表达式的类型是什么;不是说“表达式的类型是一个整数或布尔值，但我现在还不知道”，并且在评估表达式时遇到问题，我们从一开始就确信我们知道表达式值的类型而且我们不会以无意义的方式将它们结合起来。

我希望你到目前为止 - 所有在不同层次上的类型，值和表达式都会令人困惑！ - 并且你可以尝试一下，自己扩展Expr类型和评估器。

简单的事情要做的是做一个表达式，添加两个整数值，使用字符串或字符常量，或使一个'if-then-else'表达式接受三个参数：第一个布尔类型，第二个和相同类型的三分之一（但该类型可能是Int,Bool,Char或其他）。

Answer 2

的点使用GADTs将确保所有表达式的结构均为。这意味着如果你有一个Expr Int，你知道它是很好的类型，它的计算结果为Int。

要实施这一点，你需要确保常数表达式标记它们所包含的类型，从而使Con 0的类型为Expr Int，而Con True是Expr Bool。

Con :: v -> Expr v 

同样，你需要确保And只能在评估为Bool表达式中使用。

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

这样一来，像Con 0 `And` Con 1甚至不会编译，因为常量的类型Expr Int而And需要Expr Bool。

一旦你设置正确，实施est :: Expr e -> e应该是一个简单的练习。