如何根據Haskell中的輸入值限制類型？

Question

我是Haskell的新手。很抱歉，如果這個問題有明顯的答案。

我

data Tmp = Foo Int 
     | Bar Int 
     | Baz Int 

和

data Test = A Tmp Tmp 

構造A Tmp Tmp可以採取任何Tmp構造除了 A (Baz i) (Baz j)其中i和j是任意Int秒。如果第一個Tmp已經是Baz，我有什麼辦法可以 限制第二個Tmp從Baz？A Tmp Tmp？

Answer 1

答案取決於您希望如何執行限制：在運行時或編譯時。

要在運行時強制執行限制，可以添加一個函數（比如makeA），該函數檢查限制，然後調用構造函數。這樣做的功能，做一些東西，然後調用構造函數，也稱爲智能構造函數。如果您僅從模塊中導出智能構造函數makeA而不是真正的構造函數A，則可以確保其他模塊使用智能構造函數，因此始終檢查限制。

例子：

module Test (Tmp (Foo, Bar, Baz), Test(), makeA) where 
    data Tmp 
    = Foo Int 
    | Bar Int 
    | Baz Int 

    data Test = A Tmp Tmp 

    makeA :: Tmp -> Tmp -> Tmp 
    makeA (Baz _) (Baz _) = error "makeA: two baz problem" 
    makeA tmp1 tmp2 = A tmp1 tmp2 

這種技術的好處是，你不必改變你的數據類型的。缺點是限制只在運行時執行。

要在編譯時執行限制，您需要以某種方式更改您的數據類型。當前數據類型的問題是類型檢查程序無法區分由Foo和Bar構造的值以及由Baz構造的值。對於類型檢查器，這些值都是Tmp，因此類型檢查器無法強制執行某些Tmp值正常，而其他值不正確。所以我們必須改變數據類型來編碼類型中的Tmp值的「Bazness」。

在類型編碼Bazness一個選項將重組Tmp如下：

data TmpNotBaz 
    = Foo Int 
    | Bar Int 

data Tmp 
    = NotBaz TmpNotBaz 
    | Baz Int 

現在很明顯，TmpNotBaz類型的值不能Baz，但Tmp類型的值可以是Baz。這個想法的好處是它只使用基本的Haskell功能。一個小缺點是您需要將NotBaz撥打到您的代碼中。一個主要的缺點是，我們仍然不能直接表達「如果另一個不是」A的參數之一可以是Baz的想法。我們會寫的A多個版本：

data Test 
    = A1 TmpNotBaz Tmp 
    | A2 Tmp TmpNotBaz 

現在我們可以通過A1或A2根據需要選擇表達所有我們想要的值，我們無法用語言表達A (Baz ...) (Baz ...)了，因爲需要。這種解決方案的一個問題是過去存在多種表示形式，例如，A (Foo 1) (Foo 2)：A1 (Foo 1) (NotBaz (Foo 2))和A2 (NotBaz (Foo 1)) (Foo 2)都表示此值。

您可以嘗試使用像這樣的數據類型的結構，並創建適用於您的情況的版本。

在類型編碼Bazness將註釋位的類型級信息到Tmp類型和使用類型級編程來思考這種級別的信息的另一種選擇。這個想法的缺點是它使用更高級的Haskell功能。實際上，有很多新興的方法可以做這種事情，而且不清楚哪一個最終會被認爲是「標準」高級Haskell。這就是說，這裏是一個辦法：

{-# LANGUAGE GADTs, TypeFamilies, DataKinds #-} 

data Bazness = IsBaz | NotBaz 

data BothBazOrNot = BothBaz | NotBothBaz 

type family AreBothBaz (b1 :: Bazness) (b2 :: Bazness) :: BothBazOrNot where 
    AreBothBaz 'IsBaz 'IsBaz = 'BothBaz 
    AreBothBaz _ _ = 'NotBothBaz 

data Tmp (b :: Bazness) :: * where 
    Foo :: Int -> Tmp 'NotBaz 
    Bar :: Int -> Tmp 'NotBaz 
    Baz :: Int -> Tmp 'IsBaz 

data Test where 
    A :: AreBothBaz b1 b2 ~ 'NotBothBaz => Tmp b1 -> Tmp b2 -> Test 

注意如何構造函數的類型簽名Foo，Bar和Baz說說構造是否造成一些IsBaz或NotBaz。以及A的型號簽名如何選擇b1和b2以便NotBothBaz。

使用此代碼，我們可以寫出如下的表達式：

• A (Foo 1) (Bar 2)
• A (Foo 1) (Baz 2)
• A (Baz 1) (Bar 2)

但是，如果我們嘗試寫A (Baz 1) (Baz 2)，類型檢查抱怨：

Couldn't match type 'BothBaz with 'NotBothBaz 
    arising from a use of A 
In the expression: A (Baz 1) (Baz 2) 

所以類型檢查想通了，在這種情況下，參數A是BothBaz，但我們註釋的A類型只接受那些NotBothBaz參數，所以類型檢查抱怨BothBaz從NotBothBaz不同。