来自递归类型类子集的类型类（或来自递归类型的类型）
如何创建一个递归类型类，其行为类似于另一个递归类型类，但实例数量不如“父”类那么多？
这是一个示例：
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
因此我需要一个工具来表示这个层次结构。
How do I create a recursive type class which behaves like another recursive type class but has not as many instances as the "parent" class?
Here is an example:
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
That code compiles just fine but when I add a function which converts an instance of the super type class to one of the sub type class
formulaToSubFormula :: (Formula a, SubFormula b) => a -> b
formulaToSubFormula _ = Atom
I get an error
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
My original intent was to do this with normal types but with type classes the problem seems more approachable and generally more flexible.
For example:
data Formula = Atom | Negation Formula | Conjunction Formula Formula
data SubFormula = Atom | Negation SubFormula
Edit
To clarify what I try to achieve: I want to verify on the type level that an operation on the input type will return only a subset of that type as the result.
Extended example (propositional logic; no valid Haskell syntax):
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
At a later point I may have a formula in the conjunctive normal form (no valid Haskell syntax)
data CNF = CNFElem
| Conjunction CNF CNF
data CNFElem = Atom
| Negation Atom
| Disjunction CNFElem CNFElem
Therefore I need a tool to represent this hierarchy.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（5）
我将此作为答案，因为它很长并且我想要格式化。真的，我认为这是一条评论，因为它更多的是一种意见而不是解决方案。
看起来您想要可扩展/模块化语法，尽管您将您的需求从一般表述为特定 - 大多数有关可扩展语法的文章都采取另一种观点并考虑添加额外的内容案例使“小”语法变得更大。
有多种方法可以在 Haskell 中实现可扩展语法，例如“Finally Tagless”样式 [1] 或 Sheard 和 Pasalic 的两级类型 [2]。
但实际上，获得模块化语法的“协议”代码是复杂且重复的，并且您会失去常规 Haskell 数据类型的良好功能，特别是模式匹配。您还会失去很多的清晰度。最后一点至关重要 - 模块化语法对清晰度来说是一种“负担”，因此很少值得使用。通常最好使用与当前问题完全匹配的数据类型，如果以后需要扩展它们，可以编辑源代码。
[1] http://www.cs.rutgers.edu/~ccshan/ tagless/jfp.pdf
[2] http://homepage.mac.com/pasalic/p2/papers/JfpPearl.pdf
I've made this an answer because it's quite long and I wanted formatting. Really, I'd consider it a comment as it's more of an opinion than a solution.
It looks like you are wanting extensible / modular syntax although you are phrasing your needs from the general to the specific - most writing about extensible syntax takes the other view and considers adding extra cases to make "small" syntax larger.
There are ways to achieve extensible syntax in Haskell e.g. the "Finally Tagless" style [1] or Sheard and Pasalic's two level types[2].
In practice, though, the "protocol" code to get modular syntax is complicated and repetitive and you lose nice features of regular Haskell data types, particularly pattern matching. You also lose a lot of clarity. This last bit is crucial - modular syntax is such a "tax" on clarity that it is rarely worth using. You are usually better off using data types that exactly match your current problem, if you need to extend them later you can edit the source code.
[1] http://www.cs.rutgers.edu/~ccshan/tagless/jfp.pdf
[2] http://homepage.mac.com/pasalic/p2/papers/JfpPearl.pdf
您的代码的问题在于，在
formulaToSubFormula _ = Atom中，输出是使用Atom构造函数创建的，因此它始终是Atom类型，而类型签名将其声明为具有SubFormula实例的任何类型。一种选择是向SubFormula类添加一个函数：当然，如果您只有一个子类型实例，则可以完全省去该类：
另请注意，
可能不会执行以下操作你想要的。其目的大概是只有
Formula a类型可以被求反，并且始终具有可用的Formula上下文，但这意味着任何时候您使用Negation a您将需要提供一个Formula a上下文，即使它没有被使用。您可以通过使用 GADT 语法：The problem with your code is that in
formulaToSubFormula _ = Atom, the output is created with theAtomconstructor, so it is always of typeAtom, whereas the type signature declares it to be any type with aSubFormulainstance. One option is to add a function to theSubFormulaclass:Of course, if you will only have one instance of the subtype, you can dispense with the class entirely:
Also note that
probably doesn't do what you want. The intention is presumably that only
Formula atypes can be negated and will always have theFormulacontext available, but instead this means that any time you use aNegation ayou will need to provide aFormula acontext, even if it isn't used. You can get the desired result by writing this with GADT syntax:这里可能发生很多事情，我怀疑其中是否涉及类型类的引入。 （这里可能即将出现的奇特事物是 GADT。）以下内容非常简单；它只是为了让你更清楚地说出你想要的东西......
这是一个多态类型，就像你原来的那样。由于它是多态的，因此您可以使用任何东西来表示原子公式。
这是一个提取所有子公式的函数：
如果您没有考虑很多原子命题，则可以使用以下类型：
这里有一些随机助手：
让我们制作布尔原子！：
为什么不使用一个简单的评估函数？
一些随机结果：
稍后添加：请注意，
Formula是一个Functor，具有明显的实例，如果将 Functor 添加到派生子句和语言，则 GHC 可以推断出该实例pragma{-#LANGUAGE DeriveFunctor#-}。然后你可以使用任何函数f :: a -> Bool作为真值的赋值：There are many things that might be going on here, I doubt that any involves the introduction of type classes. (The fancy thing that might be in the offing here is a GADT.) The following is very simple-minded; it is just intended to get you to say what you want more clearly....
Here is a polymorphic type like the one you had originally. Since it is polymorphic you can use anything to represent the atomic formulas.
Here is a function that extracts all subformulas:
Here is a type to use if you aren't contemplating very many atomic propositions:
Here are some random helpers:
Lets make Boolean Atoms!:
Why not a simple evaluation function?
a few random results:
Added later: note that
Formulais aFunctorwith an obvious instance that can be inferred by the GHC if you add Functor to the deriving clause and the language pragma{-#LANGUAGE DeriveFunctor#-}. Then you can use any functionf :: a -> Boolas an assignment of truth values:我发现表示数据类型中的嵌套约束的唯一方法是通过类型类的某种规则系统，如下所示：
您提到的论文，尤其是 数据类型按菜单点菜，确实很有帮助。
The only way I found to represent the nesting constraints in the data types is some kind of rule system via type classes like this:
The papers you mentioned, especially Data types a la cart, were really helpful though.
Haskell 类型类不会这样工作。
它们不提供强制或子类型化。返回
Atom的函数只能是Atom返回类型，因为它返回构建Atom值的显式构造函数。对于像这样的建模表达式语言，代数数据类型（或者有时，广义代数数据类型）是压倒性的首选：
可以使用参数化类型任意表达，或者GADT，取决于您的应用程序。
Haskell typeclasses don't work like this.
They don't provide coercions or subtyping. Your function returning an
Atomcan only be ofAtomreturn type, since it returns an explicit constructor that buildsAtomvalues.For modelling expression languages like this, algebraic data types (or sometimes, generalized algebraic data types) are the overwhelmingly preferred option:
which can be made arbitrarily expressive with parameterized types, or GADTs, depending on your application.