递归类型类的子类中的类型类（或递归类型的类型）

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