無類型的術語解釋

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應該是一個簡單的練習。