使用類型來強制正確性

Question

假設我們有一個商店管理應用程序。它有Customer s並且可以chargeFee()。它應該這樣做，但只適用於活動的Customer。

我已經看到這種情況（Java /僞代碼）的常用方法是這樣的：

class Customer { 
    String name 
    StatusEnum status // 1=active, 2=inactive 
}  

// and this is how the customers are charged 
for (c:Customer.listByStatus(StatusEnum.1)) { 
    c.chargeFee() 
} 

這是確定的，但它不會從無效Customer收取費用阻止別人。即使chargeFee()檢查Customer的狀態，這是一個運行時錯誤/事件。因此，保持整個'使非法狀態不能代表'的事情在腦海中，人們會如何處理這個應用程序的設計（例如在Haskell中）？如果有人試圖向非活動客戶收費，我需要編譯錯誤。

---

我在想這樣的事情，但我還是不允許我限制chargeFee使無效Customer無法充電。

data CustomerDetails = CustomerDetails { name :: String } 
data Customer a = Active a | Inactive a 

chargeFee :: Active a -> Int -- this doesn't work, do I need DataKinds? 

Answer 1

你總是可以讓chargeFee回報Maybe或Either爲非法行爲：

chargeFee :: Customer a -> Maybe Int 
chargeFee (Inactive _) = Nothing 
chargeFee (Active cust) = ... 

Answer 2

可以完成與幻影類型的這樣一件事：

module Customer 
    (CustomerKind(..), Customer, {- note: MkCustomer is not exported -}  
    makeCustomer, activate, chargeFee) where 

data CustomerKind = Active | Inactive 
data Customer (x :: CustomerKind) = MkCustomer String 

mkCustomer :: String -> Customer Inactive 
mkCustomer = MkCustomer 

-- perhaps `IO (Customer Active)' or something else 
activate :: Customer Inactive -> Maybe (Customer Active) 
activate = ... 

chargeFee :: Customer Active -> Int 
chargeFee = ... 

這裏activate會以某種方式確保給定的客戶可以是m積極（並且這樣做），生產所述活躍的客戶。但試圖撥打chargeFee (mkCustomer ...)是一種類型錯誤。

注意DataKinds沒有嚴格要求 - 以下是等價的：

data Active 
data Inactive 
-- everything else unchanged 

同樣可以在不幻象類型通過簡單的聲明兩種類型來完成， - ActiveCustomer和InactiveCustomer - 但幻象類型的方法可以讓你寫不關心客戶的類型功能：

customerName :: Customer a -> String 
customerName (MkCustomer a) = ... 

Answer 3

一個基本的方法是使用一個單獨的類型

data ActiveCustomer = AC String -- etc. 
data InactiveCustomer = IC String -- etc. 
data Customer = Active ActiveCustomer | Inactive InactiveCustomer 

-- only works on active 
chargeFee :: ActiveCustomer -> IO() 
chargeFee (AC n) = putStrLn ("charged: " ++ n) 

-- works on anyone 
getName :: Customer -> String 
getName (Active (AC n)) = n 
getName (Inctive (IC n)) = n 

這或多或少都可以在OOP語言中完成：只爲不活躍的客戶使用不同的類，可能繼承一個通用的接口/超類。

對於代數類型，您可以得到封閉世界假設的好處，即沒有其他子類型Customer，但通常沒有其他類型。

---

更高級的方法是使用GADT。 DataKinds是可選的，但更好，恕我直言。（警告：未經測試）

{-# LANGUAGE GADTs, DataKinds #-} 

data CustomerType = Active | Inactive 
data Customer (t :: CustomerType) where 
    AC :: String -> Customer Active 
    IC :: String -> Customer Inactive 

-- only works on active 
chargeFee :: Customer Active -> IO() 
chargeFee (AC n) = putStrLn ("charged: " ++ n) 

-- works on anyone 
getName :: Customer any -> String 
getName (AC n) = n 
getName (IC n) = n 

另外，分解出的標籤與單：

data CustomerType = Active | Inactive 
data CustomerTypeSing (t :: CustomerType) where 
    AC :: CustomerTypeSing Active 
    IC :: CustomerTypeSing Active 
data Customer (t :: CustomerType) where 
    C :: CustomerTypeSing t -> String -> Customer t 

-- only works on active 
chargeFee :: Customer Active -> IO() 
chargeFee (C _ n) = putStrLn ("charged: " ++ n) 

-- works on anyone 
getName :: Customer any -> String 
getName (C _ n) = n 

-- how to build a new customer 
makeActive :: String -> Customer Active 
makeActive n = C AC n 

Answer 4

所有的需要的是標記與工作狀態的類型。我看不需要單獨的構造函數。這很容易做到，像這樣：

{-# LANGUAGE GADTs #-} 

data Active = Active 
data Inactive = Inactive 

data Customer a where 
    Customer :: String -> Int -> Customer a 

（PS我已經添加了一個Int到您的數據類型來表示信用，所以實際上你可以以某種方式向客戶收取。）

所以Customer Active代表和「主動」客戶，同樣Customer Inactive代表「不活躍」客戶。

然後，我們可以 「創造」 的客戶，像這樣：

create :: String -> Int -> Customer a 
create = Customer 

createByStatus :: a -> String -> Int -> Customer a 
createByStatus _ = Customer 

創建方便的方法很簡單：

createActive :: String -> Int -> Customer Active 
createActive = create 
createInactive :: String -> Int -> Customer Inactive 
createInactive = create 

注意，使用create直接可以創建傻類型，如Customer Int。你有幾個選項來阻止這個，

1. 只露出方便的方法給你的用戶
2. 將約束上a在create型類。

我稍後會通過選項2。

現在我們可以寫一些方法對我們的工作類型：

getName :: Customer a -> String 
getName (Customer name _) = name 

getCredit :: Customer a -> Int 
getCredit (Customer _ credit) = credit 

chargeCustomer :: Customer Active -> Int -> Customer Active 
chargeCustomer (Customer name credit) charge = Customer name (credit - charge) 

注意chargeCustomer僅適用於活躍的客戶。否則你會得到一個類型錯誤。

現在我要寫一個效用函數castCustomer。

castCustomer :: Customer a -> Customer b 
castCustomer (Customer name credit) = Customer name credit 

castCustomer所做的只是將任何類型的客戶改爲任何類型的客戶。把它看作C中不安全的轉換，你不應該把它暴露給你的用戶。但它是有用的寫你的其他功能：

setActiveStatus :: statusToCheck -> Customer currentStatus -> Customer statusToCheck 
setActiveStatus _ = castCustomer 

所以，你可以做setActiveStatus Inactive customer，你會回來customer但無效。它只使用castCustomer，適用於所有演員，但setActiveStatus的自己的類型適當限制castCustomer。

還有還有這些簡單實用的功能：

當然，現在可以寫的便利功能中：

setActive :: (LegalStatus a) => Customer a -> Customer Active 
setActive = castCustomer 

setInactive :: (LegalStatus a) => Customer a -> Customer Inactive 
setInactive = castCustomer 

最後，人們可能會想這樣的功能：

getByStatus :: b -> Customer a -> Maybe (Customer b) 

哪裏我們傳遞一個狀態和一個客戶，並且如果它們與狀態匹配，則返回該客戶，否則返回Nothing。

根據類型的不同，我們需要不同的實現，所以我們需要一個類。

我們可以編寫一個類如class GetByStatus a b，但問題是使用此類的任何函數在其類型簽名約束子句中必須有一個醜陋的GetByStatus a b。

所以我們準備做一個簡單的類：

class LegalStatus a where ... 

這是將有兩個實例：

instance LegalStatus Active where ... 
instance LegalStatus Inactive where ... 

這裏是LegalStatus類的定義：

class LegalStatus a where 
    get :: (LegalStatus b) => Customer b -> Maybe (Customer a) 
    getActive :: Customer a -> Maybe (Customer Active) 
    getInactive :: Customer a -> Maybe (Customer Inactive) 

這可能看起來很混亂，但讓我們看看實例：

instance LegalStatus Active where 
    get = getActive 
    getActive = Just . castCustomer 
    getInactive _ = Nothing 

instance LegalStatus Inactive where 
    get = getInactive 
    getActive _ = Nothing 
    getInactive = Just . castCustomer 

我們在這裏做的是一個面嚮對象的技術，稱爲https://en.wikipedia.org/wiki/Double_dispatch。這意味着我們不會使我們的簽名複雜化。現在，我們可以縮小功能，如：

getByStatus :: (LegalStatus a, LegalStatus b) => a -> Customer b -> Maybe (Customer a) 
getByStatus _ = get 

使用這些功能和catMaybe，這是比較容易編寫函數說，把客戶的列表，只返回活躍的：

getAll :: (LegalStatus a, LegalStatus b) => [Customer a] -> [Customer b] 
getAll = catMaybes . map get 

getAllByStatus :: (LegalStatus a, LegalStatus b) => a -> [Customer b] -> [Customer a] 
getAllByStatus _ = getAll 

getAllActive :: (LegalStatus a) => [Customer a] -> [Customer Active] 
getAllActive = getAll 

getAllInactive :: (LegalStatus a) => [Customer a] -> [Customer Inactive] 
getAllInactive = getAll 

值得指出了神奇getAll是如何的（事實上，Haskell中的許多其他類似功能）。執行getAll list，如果您將活動客戶列入活動客戶列表，則只會獲得列表中的活躍客戶，同樣，如果您將其列入非活動客戶列表中，您將只在列表中獲得非活動客戶。

我將通過下面的函數，其將客戶的名單誰的狀態未知到活躍客戶名單和不活躍的客戶名單illstrate這樣的：

splitCustomers :: (LegalStatus a) => [Customer a] -> ([Customer Active], [Customer Inactive]) 
splitCustomers l = (getAll l, getAll l) 

綜觀splitCustomers實施，看起來這一對的第一和第二個元素是相同的。確實他們看起來完全一樣。但他們不是，他們有不同的類型，因此最終調用不同的實例並得到完全不同的結果。

如果你真的想要關閉，還有另外一件事。您可能想要公開類LegalStatus，因爲用戶可能希望將其用作其類型簽名中的約束，但這意味着他們可以編寫LegalStatus的實例。像

instance LegalStatus Int where ... 

他們會很愚蠢的做到這一點，但你可以阻止他們，如果你喜歡。最簡單的方法是這樣的：

{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE ConstraintKinds #-} 

type family RestrictLegalStatus a where 
    RestrictLegalStatus Active =() 
    RestrictLegalStatus Inactive =() 

type IsLegalStatus a = (RestrictLegalStatus a ~()) 

class (IsLegalStatus a) => LegalStatus a where ... 

任何企圖使一個新的實例，現在將失敗IsLegalStatus約束和失敗。

這可能是過度設計在這一點上，你將不再需要這一切，但我將它顯示有關類型推斷的一些要點：

所以，供大家參考，這裏的所有附加代碼如下：

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE ConstraintKinds #-} 

module Main where 

import Data.Maybe (catMaybes) 

main = return() 

data Active = Active 
data Inactive = Inactive 

type family RestrictLegalStatus a where 
    RestrictLegalStatus Active =() 
    RestrictLegalStatus Inactive =() 

type IsLegalStatus a = (RestrictLegalStatus a ~()) 

data Customer a where 
    Customer :: String -> Int -> Customer a 

class (IsLegalStatus a) => LegalStatus a where 
    get :: (LegalStatus b) => Customer b -> Maybe (Customer a) 
    getActive :: Customer a -> Maybe (Customer Active) 
    getInactive :: Customer a -> Maybe (Customer Inactive) 

instance LegalStatus Active where 
    get = getActive 
    getActive = Just . castCustomer 
    getInactive _ = Nothing 

instance LegalStatus Inactive where 
    get = getInactive 
    getActive _ = Nothing 
    getInactive = Just . castCustomer 

getByStatus :: (LegalStatus a, LegalStatus b) => a -> Customer b -> Maybe (Customer a) 
getByStatus _ = get 

create :: String -> Int -> Customer a 
create = Customer 

createByStatus :: a -> String -> Int -> Customer a 
createByStatus _ = Customer 

createActive :: String -> Int -> Customer Active 
createActive = Customer 

createInactive :: String -> Int -> Customer Inactive 
createInactive = Customer 

getName :: Customer a -> String 
getName (Customer name _) = name 

getCredit :: Customer a -> Int 
getCredit (Customer _ credit) = credit 

chargeCustomer :: Customer Active -> Int -> Customer Active 
chargeCustomer (Customer name credit) charge = Customer name (credit - charge) 

castCustomer :: Customer a -> Customer b 
castCustomer (Customer name credit) = Customer name credit 

setActiveStatus :: (LegalStatus statusToCheck, LegalStatus currentStatus) => statusToCheck -> Customer currentStatus -> Customer statusToCheck 
setActiveStatus _ = castCustomer 

setActive :: (LegalStatus a) => Customer a -> Customer Active 
setActive = castCustomer 

setInactive :: (LegalStatus a) => Customer a -> Customer Inactive 
setInactive = castCustomer 

getAll :: (LegalStatus a, LegalStatus b) => [Customer a] -> [Customer b] 
getAll = catMaybes . map get 

getAllByStatus :: (LegalStatus a, LegalStatus b) => a -> [Customer b] -> [Customer a] 
getAllByStatus _ = getAll 

getAllActive :: (LegalStatus a) => [Customer a] -> [Customer Active] 
getAllActive = getAll 

getAllInactive :: (LegalStatus a) => [Customer a] -> [Customer Inactive] 
getAllInactive = getAll 

splitCustomers :: (LegalStatus a) => [Customer a] -> ([Customer Active], [Customer Inactive]) 
splitCustomers l = (getAll l, getAll l) 

編輯：

其他人指出使用DataKinds限制狀態。無可否認，這可能比我的「對班級的約束」方法更清潔。請注意，您必須更改一些函數，因爲類的參數不再是普通類型，而只是一種類型，只有普通類型纔可以作爲函數的參數，所以必須在構造函數中包裝原始狀態函數。

與DataKind方法注意你不能再稱之爲getByStatus Active ...因爲Active不再是一個值，你需要做的：

getByStatus (Proxy :: Proxy Active) ... 

但隨時定義：

active :: Proxy Active 
active = Proxy 

，然後您可以撥打：

getByStatus active 

完整的代碼在下方。

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE DataKinds #-} 

module Main where 

import Data.Maybe (catMaybes) 
import Data.Proxy (Proxy) 

main = return() 

data LegalStatusKind = Active | Inactive 

data Customer (a :: LegalStatusKind) where 
    Customer :: String -> Int -> Customer a 

class LegalStatus (a :: LegalStatusKind) where 
    get :: (LegalStatus b) => Customer b -> Maybe (Customer a) 
    getActive :: Customer a -> Maybe (Customer Active) 
    getInactive :: Customer a -> Maybe (Customer Inactive) 

instance LegalStatus Active where 
    get = getActive 
    getActive = Just . castCustomer 
    getInactive _ = Nothing 

instance LegalStatus Inactive where 
    get = getInactive 
    getActive _ = Nothing 
    getInactive = Just . castCustomer 

getByStatus :: (LegalStatus a, LegalStatus b) => Proxy a -> Customer b -> Maybe (Customer a) 
getByStatus _ = get 

create :: String -> Int -> Customer a 
create = Customer 

createByStatus :: Proxy a -> String -> Int -> Customer a 
createByStatus _ = Customer 

createActive :: String -> Int -> Customer Active 
createActive = Customer 

createInactive :: String -> Int -> Customer Inactive 
createInactive = Customer 

getName :: Customer a -> String 
getName (Customer name _) = name 

getCredit :: Customer a -> Int 
getCredit (Customer _ credit) = credit 

chargeCustomer :: Customer Active -> Int -> Customer Active 
chargeCustomer (Customer name credit) charge = Customer name (credit - charge) 

castCustomer :: Customer a -> Customer b 
castCustomer (Customer name credit) = Customer name credit 

setActiveStatus :: (LegalStatus statusToCheck, LegalStatus currentStatus) => Proxy statusToCheck -> Customer currentStatus -> Customer statusToCheck 
setActiveStatus _ = castCustomer 

setActive :: (LegalStatus a) => Customer a -> Customer Active 
setActive = castCustomer 

setInactive :: (LegalStatus a) => Customer a -> Customer Inactive 
setInactive = castCustomer 

getAll :: (LegalStatus a, LegalStatus b) => [Customer a] -> [Customer b] 
getAll = catMaybes . map get 

getAllByStatus :: (LegalStatus a, LegalStatus b) => Proxy a -> [Customer b] -> [Customer a] 
getAllByStatus _ = getAll 

getAllActive :: (LegalStatus a) => [Customer a] -> [Customer Active] 
getAllActive = getAll 

getAllInactive :: (LegalStatus a) => [Customer a] -> [Customer Inactive] 
getAllInactive = getAll 

splitCustomers :: (LegalStatus a) => [Customer a] -> ([Customer Active], [Customer Inactive]) 
splitCustomers l = (getAll l, getAll l)