递归类型类的子集中的类型类(或递归类型中的类型)

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

我给出了一个答案，因为它很长，而且我想要格式化。真的，我会认为这是一个评论，因为它更多的是一种观点而不是一种解决方案。

看起来你想要可扩展的/模块化的语法，尽管你从一般到具体来表达你的需求-大多数关于可扩展语法的文章采取了另一种观点，并考虑增加额外的案例来使“小”语法更大。

在Haskell中实现可扩展语法的方法有很多，例如“最终无标记”风格1或There和Pasalic的两级types2。

然而，在实践中，获得模块化语法的“协议”代码是复杂和重复的，并且您会失去常规Haskell数据类型的良好特性，特别是模式匹配。你也失去了lot的清晰度。最后一点至关重要--模块化语法对清晰度来说是一种“负担”，几乎不值得使用。通常情况下，最好使用与当前问题完全匹配的数据类型，如果以后需要扩展它们，可以编辑源代码。

1

2