遞歸類型類的子類中的類型類（或遞歸類型的類型）

Question

如何創建類似於另一個遞歸類型類但具有與「父類」類不同的實例的遞歸類型類？

下面是一個例子：

data Atom = Atom 
data (Formula a) => Negation a = Negation a 

class Formula a where 
instance Formula Atom where 
instance (Formula a) => Formula (Negation a) where 

class SubFormula a where 
instance SubFormula Atom where 

這代碼編譯就好了，但是當我加入其轉換超級類型的類的實例函數的子類型類

formulaToSubFormula :: (Formula a, SubFormula b) => a -> b 
formulaToSubFormula _ = Atom 

之一我得到一個錯誤

test.hs:12:25: 
    Could not deduce (b ~ Atom) 
    from the context (Formula a, SubFormula b) 
     bound by the type signature for 
       formulaToSubFormula :: (Formula a, SubFormula b) => a -> b 
     at test.hs:12:1-28 
     `b' is a rigid type variable bound by 
      the type signature for 
      formulaToSubFormula :: (Formula a, SubFormula b) => a -> b 
      at test.hs:12:1 
    In the expression: Atom 
    In an equation for `formulaToSubFormula': 
     formulaToSubFormula _ = Atom 

---

我最初的目的是用普通的類型來完成這個任務，但是對於類型類來說，這個問題似乎更容易理解，並且通常更加靈活。

例如：

data Formula = Atom | Negation Formula | Conjunction Formula Formula 
data SubFormula = Atom | Negation SubFormula 

---

編輯

爲了澄清什麼，我儘量做到：我想驗證的類型級別的輸入類型的操作將只返回一個子集作爲結果的那種類型。

擴展示例（命題邏輯;沒有有效Haskell語法）：

data Formula = Atom 
      | Negation Formula 
      | Disjunction Formula Formula 
      | Implication Formula Formula 
data SimpleFormula = Atom 
        | Negation SimpleFormula 
        | Disjunction SimpleFormula SimpleFormula 

-- removeImplication is not implemented correctly but shows what I mean 
removeImplication :: Formula -> SimpleFormula 
removeImplication (Implication a b) = (Negation a) `Disjunction` b 
removeImplication a = a 

在以後某個時候我可以具有在合取範式式（沒有有效Haskell語法）

data CNF = CNFElem 
     | Conjunction CNF CNF 
data CNFElem = Atom 
      | Negation Atom 
      | Disjunction CNFElem CNFElem 

因此我需要一個工具來表示這個層次結構。

Answer 1

我發現來表示數據類型的嵌套約束的唯一方法是經由類型類某種規則系統的這樣的：

data Formula t val = Formula val deriving Show 

-- formulae of type t allow negation of values of type a 

class Negatable t a 
instance Negatable Fancy a 
instance Negatable Normal a 
instance Negatable NNF Atom 
instance Negatable CNF Atom 
instance Negatable DNF Atom 

class Conjunctable t a 
instance Conjunctable Fancy a 
instance Conjunctable Normal a 
instance Conjunctable NNF a 
instance Conjunctable CNF a 
instance Conjunctable DNF Atom 
instance Conjunctable DNF (Negation a) 
instance Conjunctable DNF (Conjunction a b) 

--- 

negate :: (Negatable t a) => Formula t a -> Formula t (Negation a) 
negate (Formula x) = Formula $ Negation x 

conjunct :: (Conjunctable t a, Conjunctable t b) 
     => Formula t a -> Formula t b -> Formula t (Conjunction a b) 
conjunct (Formula x) (Formula y) = Formula $ Conjunction x y 

您提到的論文，特別是Data types a la cart，確實很有幫助。

Answer 2

超類型的類的實例轉換爲子類型類

Haskell的類型類不喜歡這個工作之一。

他們不提供強制或子類型。返回Atom的函數只能是Atom返回類型，因爲它返回一個顯式構造函數，它構建Atom值。

對於建模表達語言這樣，代數數據類型（或有時，廣義代數數據類型）是壓倒性優選選項：

data Proposition 
    = LITERAL Bool 
    | ALL (Set Proposition) 
    | ANY (Set Proposition) 
    | NOT Proposition 

其可以由與參數化的類型任意表達，或GADT，取決於您的應用程序。

Answer 3

與您的代碼的問題是，在formulaToSubFormula _ = Atom，輸出與Atom構造函數創建，所以它總是Atom類型，而類型簽名聲明它是任何類型的一個SubFormula實例。一種選擇是一個功能添加到SubFormula類：

formulaToSubFormula2 :: Formula a => a -> Atom 

還要注意：

class SubFormula a where 
    atom :: a 

instance SubFormula Atom where 
    atom = Atom 

formulaToSubFormula :: (Formula a, SubFormula b) => a -> b 
formulaToSubFormula _ = atom 

當然，如果你只會有亞型的一個實例，你可以完全類免除那

data (Formula a) => Negation a = Negation a 

可能不會做你想做的。我們的意圖大概是，只有Formula a類型可以否定，並且始終具有Formula上下文可用，但相反，這意味着只要您使用Negation a，即使未使用，也需要提供Formula a上下文。你可以通過GADT syntax寫這得到期望的結果：

data Negation a where 
    Negation :: Formula a => a -> Negation a 

Answer 4

有很多事情可能在這裏的時候，我懷疑任何包括引入類型的類。 （這裏可能會有一件奇怪的事情是一個GADT。）以下是非常簡單的;它只是想讓你說清楚你想要的更清楚。...

這是一個多態類型，就像你最初的那種。由於它是多態的，你可以使用任何東西來表示原子公式。

data Formula a = Atom a 
       | Negation (Formula a)  
       | Conjunction (Formula a) (Formula a) deriving (Show, Eq, Ord) 

這裏是提取所有子公式函數：

subformulas (Atom a) = [Atom a] 
subformulas (Negation p) = Negation p : subformulas p 
subformulas (Conjunction p q) = Conjunction p q : (subformulas p ++ subformulas q) 

這裏是一個類型，如果你不考慮非常多的原子命題的使用方法：

data Atoms = P | Q | R | S | T | U | V deriving (Show, Eq, Ord) 

這裏有一些隨機幫手：

k p q = Conjunction p q 
n p = Negation p 
p = Atom P 
q = Atom Q 
r = Atom R 
s = Atom S 

x --> y = n $ k x (n y) -- note lame syntax highlighting 

-- Main> ((p --> q) --> q) 
-- Negation (Conjunction (Negation (Conjunction (Atom P) (Negation (Atom Q)))) (Negation (Atom Q))) 
-- Main> subformulas ((p --> q) --> q) 
-- [Negation (Conjunction (Negation (Conjunction (Atom P) (Negation (Atom Q)))) (Negation (Atom Q))), 
--  Conjunction (Negation (Conjunction (Atom P) (Negation (Atom Q)))) (Negation (Atom Q)), 
--  Negation (Conjunction (Atom P) (Negation (Atom Q))), 
--  Conjunction (Atom P) (Negation (Atom Q)),Atom P, 
--  Negation (Atom Q),Atom Q,Negation (Atom Q),Atom Q] 

讓布爾原子！：

t = Atom True 
f = Atom False 

-- Main> t --> f 
-- Main> subformulas (t --> f) 
-- [Negation (Conjunction (Atom True) (Negation (Atom False))), 
--   Conjunction (Atom True) (Negation (Atom False)),  
--   Atom True,Negation (Atom False),Atom False] 

爲什麼不是一個簡單的評估函數？

eval :: Formula Bool -> Bool 
eval (Atom p) = p 
eval (Negation p) = not (eval p) 
eval (Conjunction p q) = eval p && eval q 

一些隨機的結果：

-- Main> eval (t --> f) 
-- False 
-- Main> map eval $ subformulas (t --> f) 
-- [False,True,True,True,False] 

後來補充：注意Formula是Functor與可由GHC如果添加函子來推導子句和語言來推斷一個明顯的例子雜注{-#LANGUAGE DeriveFunctor#-}。然後你可以使用任何功能f :: a -> Bool爲真值的分配：

-- *Main> let f p = p == P || p == R 
-- *Main> fmap f (p --> q) 
-- Negation (Conjunction (Atom True) (Negation (Atom False))) 
-- *Main> eval it 
-- False 
-- *Main> fmap f ((p --> q) --> r) 
-- Negation (Conjunction (Negation (Conjunction (Atom True) (Negation (Atom False)))) (Negation (Atom True))) 
-- *Main> eval it 
-- True 

Answer 5

我做了這樣的一個答案，因爲這是相當長的，我想格式化。真的，我認爲這是一個評論，因爲它比解決方案更重要。

看起來你是想擴展/模塊化的語法雖然你是從一般措辭您的需求給具體 - 約擴展句法最書寫採取另一種觀點，認爲增加額外的情況下，使「小」語法更大。有些方法可以在Haskell中實現可擴展的語法，例如， 「最後無標籤」風格[1]或Sheard和帕西里克的兩種類型[2]。

實際上，獲取模塊化語法的「協議」代碼是複雜且重複的，並且您失去了常規Haskell數據類型的很好功能，尤其是模式匹配。您也會失去清晰度的lot。最後一點是至關重要的 - 模塊化語法在清晰度上就是這樣的「稅」，它很少使用。如果您需要稍後擴展它們，則可以編輯源代碼，但通常情況下，您最好使用與當前問題完全匹配的數據類型。

[1] http://www.cs.rutgers.edu/~ccshan/tagless/jfp.pdf

[2] http://homepage.mac.com/pasalic/p2/papers/JfpPearl.pdf