如何模式匹配其實例是遞歸數據類型的類型類型？

Question

這個問題是關於How to pattern match against a typeclass value?的後續。

我開始了一階邏輯的寵物項目，並決定使用Haskell來達到此目的。我的第一個障礙是定義一個「一階邏輯的公式」，因此數據類型：

data Formula v = Belong v v      -- x in y 
       | Bot        -- False 
       | Imply (Formula v) (Formula v) -- p -> q 
       | Forall v (Formula v)   -- forall x, p 

但是，我不願意基礎上，實現細節來編寫代碼，而寧願抽象掉的細節，情況下，我改變了主意，或在情況下，我想用另一種實現重複使用的功能，因此，類型類：

class FirstOrder m where 
    belong :: v -> v -> m v 
    bot  :: m v 
    imply  :: m v -> m v -> m v 
    forall :: v -> m v -> m v 
    asFormula :: m v -> Formula v 

我已經添加了最後一個函數asFormula爲了使用ViewPatterns（如上面的鏈接提示），以便能夠對此類型類型的值進行模式匹配。

現在假設我想要定義一個簡單的函數：

subst :: (FirstOrder m) => (v -> w) -> m v -> m w 

其中替換變量的公式中作爲每一個給定的映射f::v -> w（感覺fmap），所以式belong x y被映射到belong (f x) (f y)等，然後使用ViewPatterns：

subst f (asFormula -> Belong x y) = belong (f x) (f y) 

到目前爲止好...

然而，當試圖寫subst f p->q = (subst f p) -> (subst f q)：

subst f (asFormula -> Imply p q) = imply (subst f p) (subst f q) 

我得到一個類型的錯誤，其未來想它非常有意義：模式匹配結合p和q來，而不是期望的類型Formula v類型的元素m v。

現在我可以看到問題了，甚至可以想辦法通過在類型類中添加fromFormula函數來轉換回m v類型，但我認爲這從性能角度來看是瘋狂的（就像asFormula一樣瘋狂），爲了保持代碼的通用性，付出巨大的代價。

因此，我現在試圖通過結構遞歸來定義一個簡單的函數，它是一個自由代數（遞歸數據類型），但是我希望將實現細節抽象出來（並且將類代碼寫入類型類型而不是數據類型）是讓我陷入似乎不可能的境地。

有沒有出路，或者我應該忘記抽象和使用遞歸數據類型？

Answer 1

這看起來是一個過度概括，但我們無視這個問題。

你可以用顯式的F-（co-）代數和固定點來解決這個問題。

data FormulaF v k 
    = Belong v v      -- x in y 
    | Bot        -- False 
    | Imply (k v) (k v)    -- p -> q 
    | Forall v (k v)     -- forall x, p 

newtype Formula v = Formula (FormulaF v Formula)  
    -- fixed point. You might not need it, but it's nice to have. 
    -- 

然後，你可以做

class FirstOrder m where 
    belong :: v -> v -> m v 
    bot  :: m v 
    imply  :: m v -> m v -> m v 
    forall :: v -> m v -> m v 
    asFormula :: m v -> FormulaF v m 

和

subst :: (FirstOrder m) => (v -> w) -> m v -> m w 
subst f (asFormula -> Belong x y) = belong (f x) (f y) 
subst f (asFormula -> Imply p q) = imply (subst f p) (subst f q) 

現在應該工作，因爲asFormula不整m v轉換成一個完整的公式遞歸，但它轉換成FormulaF v m它看起來像一個公式表面上（你模式匹配的第一個構造函數，如Imply），但內心深處仍然看s作爲m v。如果你真的想追求這種一般的方法，也許你應該看看recursion-schemes，F-代數和F-代數，以及它們相關的cata-/ana-/hylo-/para- /任何態射。

最後，我建議避免嘗試去適應FP中的OOP設計模式。有時候你可以用這種方式來強化某些東西，但它往往可以是單一的。例如，在Haskell中，我們非常習慣於具有固定數量的構造函數的類型（但是對它們進行操作的一組開放的函數），就像在OOP接口中有固定數量的方法（但是是一組開放的子類） 。人們可以嘗試概括這一點，但它很複雜，應該只在需要時才能完成。