將正確性約束直接編碼到Haskell類型系統中？

Question

在閱讀由matt的書寫的article的同時，我看到了下面的感覺。

有經驗的程序員能熟練地直接編碼正確性約束到Haskell的類型系統

有人能解釋一下這句話的意思，或者提供一個簡短的例子？

Answer 1

這可以涵蓋真的各種不同的技術。最簡單的基本上是不可避免的：如果你想要一個可以爲null的值，這可以取決於可變狀態或用戶輸入，你必須用類型系統標記。這分別是Maybe,ST和IO。因此，如果您有上述三種類型中的某一種不具備，則您必須知道該參數必須是透明的值，不能爲空。

上述技巧對語言來說非常基礎，基本上是不可避免的。但是，還有其他一些方法可以使用類型系統來提高安全性和正確性，這些方法更有趣一些。

一個有用的示例是阻止SQL注入。 SQL注入是Web應用程序中的常見問題 - 對於基本思想，請查看this XKCD cartoon。我們實際上可以使用類型系統來確保傳遞給數據庫的任何字符串已被清理。其基本思想是創建「原始」的字符串一個新的類型：

newtype Raw a = Raw a 

然後，請確保您的所有功能，從用戶獲得的回報輸入Raw值而不是正常的字符串。最後，你只需要一個淨化功能：

sanitize :: Raw String -> String 

由於正常功能接受String而非Raw，你將無法在unsanitized串意外通過。由於我們使用newtype定義了Raw，因此它根本沒有運行時間開銷。

Yesod，Haskell的主要Web框架之一，使用了一種類似的技術來防止SQL注入。它還有一些其他很酷的方法，比如使用類型系統來防止數據庫中斷開的鏈接;你應該檢查一下。

在真正極端的情況下，您甚至可以使用類型系統來確保矩陣的大小合適。這是一個非常簡單的方法來做到這一點。首先，我們需要的類型級號：（我們在type level使用Peano Arithmetic這裏）

data Z 
data S n 

的想法很簡單：Z爲0，S是後繼功能，所以S Z是1，S (S Z)是2等等。

現在，我們可以寫一個安全的矩陣乘法功能：

matMul :: Mat a b -> Mat b c -> Mat a c 

該功能只會讓你乘矩陣如果內部尺寸相匹配，並確保所產生的基質在其類型正確的尺寸。

Type-safe matrix multiplication有更多細節。

Answer 2

嗯，在我看來，像你所見過的那些展覽往往無法表達的東西之一就是這種類型的正確性往往是不會「自然地」發生的東西，而是來自使用技術來設計您的類型，這對於來自其他語言的程序員來說並不明顯。我最喜歡的例子之一來自the Haskell Wiki page on phantom types;如果你看一下第1部分在該網頁上，他們有這樣的例子（IMO應該是一個newtype聲明，而不是data）：

data FormData a = FormData String 

有什麼a在做什麼？那麼，它的作用就是人爲地讓FormData "foo" :: FormData Validated和FormData "foo" :: FormData Unvalidated，儘管它們「真的」是相同的，現在有不兼容的類型，因此你可以強制你的代碼不混合一個和另一個。那麼，讓我不要重複頁面所說的內容，閱讀起來相對容易（至少在第1部分）。

，我一直在用我的和小康的一個項目一個更復雜的例子：OLAP立方體可以看作是一種陣列由整數索引沒有編號，而是由類似人的數據模型對象，天，產品系列等：

-- | The type of Hypercubes. 
data Hypercube point value = ... 

-- | Access a data point in a hypercube. 
get :: Eq point => Hypercube point value -> point -> value 

-- | This is totally pseudocode... 
data Salesperson = Mary | Joe | Irma deriving Eq 
data Month = January | February | ... | December deriving Eq 
data ProductLine = Widget | Gagdet | Thingamabob 

-- Pseudo-example: compute sales numbers grouped by Salesperson, Month and 
-- ProductLine for the combinations specified as the "frame" 
salesResult :: HyperCube (Salesperson, Month, ProductLine) Dollars 
salesResult = execute salesQuery frame 
    where frame = [Joe, Mary] `by` [March, April] `by` [Widgets, Gadgets] 
      salesQuery = ... 

-- Read from salesResult how much Mary sold in Widgets on April. 
example :: Dollars 
example = get salesResult (Mary, April, Widgets) 

我希望這比我擔心它更有意義。無論如何，該點的例子如下的問題：get的類型，都在這了，讓你問一個Hypercube告訴你一個點的價值也沒有：

badExample :: Dollar 
badExample = get salesResult (Irma, January, Thingamabob) 

一種可能對此的解決方案是使get操作返回Maybe value而不僅僅是value。但我們其實可以做得更好;我們可以設計一個API，其中Hypercube只能被問及它包含的值。關鍵是類似於FormData的例子，但更復雜的變體。首先我們介紹的這款幻影類型：

data Cell tag point = Cell { getPoint :: point } deriving Eq 

現在我們重新制定Hypercube和get是標籤敏感。在這個重新構造的例子中，我實際上要更具體一些。我們先從這一點：

{-# LANGUAGE ExistentialTypes #-} 

data AuxCube tag point value = 
    AuxCube { getFrame :: [Cell tag point] 
      , get :: Cell tag point -> value } 

-- This is using a type system extension called ExistentialTypes: 
data Hypercube point value = forall tag. Hypercube (AuxCube tag point value) 

-- How to use one of these cubes. Suppose we have: 
salesResult :: Hypercube (Salesperson, Month, ProductLine) Dollars 
salesResult = execute salesQuery points 
    where points = [Joe, Mary] `by` [March, April] `by` [Widgets, Gadgets] 
      salesQuery = ... 

-- Now to read values, we have to do something like this: 
example = case salesResult of 
       Hypercube (AuxCube frame getter) -> getter (head frame) 

我道歉，如果使用ExistentialTypes這裏混淆了你，但要長話短說，它的作用在這個例子中，基本上每個Hypercube包含AuxCube了一個獨特的匿名標籤type參數，所以現在沒有兩個Hypercube可以具有相同類型的Cell。由於這個原因，如果我們使用模塊系統來阻止呼叫者構建Cell s，呼叫者不可能要求Hypercube找到Cell它沒有值。

Credits：I learned this technique by asking here in Stack Overflow。