如何使用 Haskell 的类型系统来强制正确性，同时仍然能够进行模式匹配？

Question

假设我有一个代表某种树结构的 adt：

data Tree = ANode (Maybe Tree) (Maybe Tree) AValType
          | BNode (Maybe Tree) (Maybe Tree) BValType
          | CNode (Maybe Tree) (Maybe Tree) CValType

据我所知，没有办法针对类型构造函数进行模式匹配（或者匹配函数本身没有类型？），但我仍然想使用编译时类型系统消除了返回或解析树节点的错误“类型”的可能性。例如，CNode 可能只能是 ANode 的父节点。我可能有

parseANode :: Parser (Maybe Tree)

一个 Parsec 解析函数，用作我的 CNode 解析器的一部分：

parseCNode :: Parser (Maybe Tree)
parseCNode = try (
                  string "<CNode>" >>
                  parseANode >>= \maybeanodel ->
                  parseANode >>= \maybeanoder ->
                  parseCValType >>= \cval ->
                  string "</CNode>"
                  return (Just (CNode maybeanodel maybeanoder cval))
             ) <|> return Nothing

根据类型系统，parseANode 最终可能返回 Maybe CNode、Maybe BNode 或 Maybe ANode，但我真的想确保它只返回一个 Maybe ANode。请注意，这不是我想要做的数据模式值或运行时检查 - 我实际上只是想检查我为特定树模式编写的解析器的有效性。 IOW，我并不是要检查解析数据的架构正确性，我真正想做的是检查我的解析器的架构正确性 - 我只是想确保我不这样做有一天，不要搞砸 parseANode 返回 ANode 值以外的东西。

我希望，如果我与绑定变量中的值构造函数进行匹配，类型推断就会明白我的意思：

parseCNode :: Parser (Maybe Tree)
parseCNode = try (
                  string "<CNode>" >>
                  parseANode >>= \(Maybe (ANode left right avall)) ->
                  parseANode >>= \(Maybe (ANode left right avalr)) ->
                  parseCValType >>= \cval ->
                  string "</CNode>"
                  return (Just (CNode (Maybe (ANode left right avall)) (Maybe (ANode left right avalr)) cval))
             ) <|> return Nothing

但这有很多问题，其中最重要的是 parseANode 不再可以自由返回没有什么。而且它无论如何都不起作用 - 看起来绑定变量被视为模式匹配，并且当 parseANode 返回 Nothing 或 Maybe BNode 或其他内容时，运行时会抱怨非详尽的模式匹配。

我可以沿着这些思路做一些事情：

data ANode = ANode (Maybe BNode) (Maybe BNode) AValType
data BNode = BNode (Maybe CNode) (Maybe CNode) BValType
data CNode = CNode (Maybe ANode) (Maybe ANode) CValType

但这有点糟糕，因为它假设约束应用于所有节点 - 我可能对此不感兴趣 - 事实上，它可能只是 CNode 只能作为 ANode 的父节点。所以我想我可以这样做：

data AnyNode = AnyANode ANode | AnyBNode BNode | AnyCNode CNode

data ANode = ANode (Maybe AnyNode) (Maybe AnyNode) AValType
data BNode = BNode (Maybe AnyNode) (Maybe AnyNode) BValType
data CNode = CNode (Maybe ANode) (Maybe ANode) CValType

但这使得与 *Node 进行模式匹配变得更加困难 - 事实上这是不可能的，因为它们只是完全不同的类型。我想我可以在任何想要模式匹配的地方创建一个类型类

class Node t where
    matchingFunc :: t -> Bool

instance Node ANode where
    matchingFunc (ANode left right val) = testA val

instance Node BNode where
    matchingFunc (BNode left right val) = val == refBVal

instance Node CNode where
    matchingFunc (CNode left right val) = doSomethingWithACValAndReturnABool val

，无论如何，这看起来有点混乱。谁能想到一种更简洁的方法来做到这一点？

Answer 1

我不明白你反对你的最终解决方案。您仍然可以针对 AnyNode 进行模式匹配，如下所示：

f (AnyANode (ANode x y z)) = ...

它有点冗长，但我认为它具有您想要的工程属性。

Answer 2

我仍然想使用编译时类型系统来消除返回或解析错误的树节点“类型”的可能性

这听起来像是 GADT 的用例。

{-# LANGUAGE GADTs, EmptyDataDecls #-}
data ATag
data BTag
data CTag

data Tree t where
  ANode :: Maybe (Tree t) -> Maybe (Tree t) -> AValType -> Tree ATag
  BNode :: Maybe (Tree t) -> Maybe (Tree t) -> BValType -> Tree BTag
  CNode :: Maybe (Tree t) -> Maybe (Tree t) -> CValType -> Tree CTag

现在，当您不关心节点类型时，可以使用 Tree t ，或者当您关心节点类型时，可以使用 Tree ATag 。

Answer 3

基冈答案的延伸：对红/黑树的正确性属性进行编码是一个典型的例子。该线程的代码显示了 GADT 和嵌套数据类型解决方案： http:// /www.reddit.com/r/programming/comments/w1oz/how_are_gadts_useful_in_practical_programming/cw3i9