haskell - 如何对每种节点可以出现的位置进行限制的树数据结构建模？

Question

在 Haskell 中，为递归树创建数据类型很简单，就像我们对 XML 文档所做的那样:

data XML = 
    Text String       -- Text of text node
  | Elem String [XML] -- Tagname; Child nodes

及其相关的折叠:

-- Simple fold (Child trees don't see the surrounding context.)
foldt :: (String -> a) -> (String -> [a] -> a) -> XML -> a
foldt fT fE (Text text) = fT text
foldt fT fE (Elem tagname ts) = fE tagname (map (foldt fT fE) ts)

-- Threaded fold for streaming applications.
-- See http://okmij.org/ftp/papers/XML-parsing.ps.gz
foldts :: (a -> String -> a) -> (a -> String -> a) ->  (a -> a -> String -> a) -> a -> XML -> a
foldts fT fE_begin fE_end = go
  where
    go seed (Text text) = fT seed text
    go seed (Elem tag children) = 
        let seed' = fE_begin seed tag in
        let seed'' = foldl go seed' children in
        fE_end seed seed'' tag

我现在的问题是我不知道如何向我的树数据类型添加一些额外的限制以便为 HTML 建模。在 HTML 中每个元素节点只能出现在正确的 contexts 中每个元素对应于其子元素的不同上下文。例如:

• 空元素，如 img有一个空的上下文模型，并且不允许有任何 child 。
• 具有文本内容模型的元素，例如 title , 只能有文本节点作为子节点(不允许嵌套标签)
• div元素不能出现在短语上下文中，因此不允许成为 span 的后代元素。

所以我的问题是:

1. 要在 Haskell98 中模拟这些限制，我需要做什么？ (我问这个是因为我猜 Haskell98 模型应该更好地翻译成其他编程语言)

   我想我们可能必须为不同的上下文创建许多不同的数据类型，但我不知道如何以一种有原则和清晰的方式来做到这一点。我怎样才能做到这一点而不迷路，折叠函数最终会是什么样子？

2. 如果允许我们使用 GADT 等现代 GHC 功能，模型会是什么样子？

   我有一种预感，GADT 可能有助于将限制插入类型检查器，使折叠功能保持简单，但我对它们没有太多经验...

我不需要 100% 有效的解决方案，因为这显然超出了 Stack Overflow 讨论的范围。我只需要能够更好地掌握 GADT 之类的东西，并能够自己完成剩下的事情。

Answer 1

这不需要 GADT(至少现在不需要)。你只需要告诉编译器更多关于你的树类型的信息。

data HTML
    = HTML HTMLHeader HTMLBody

data HTMLHeader
    = Header String

data HTMLBody
    = Body [HTMLContent]

data HTMLContent
    = Text HTMLText
    | Title HTMLText
    | Img  String
    | Elem String [HTML]

data HTMLText
    = Literal String
    | Bold String
    | Italic String
    | TextElems [HTMLText]

现在你得到了一些不变量:

-- Must have header and body. titles can't contain images.

x = HTML
        (Header "TEST") $ Body [
             Title (Literal "Title")
            ,Text (Bold "Content")
        ]

派生这棵树的原则性方法是从特定的 HTML 语法 - 例如XML EBNF 也许 - http://www.w3.org/TR/2006/REC-xml11-20060816/#sec-well-formed .

使用 GADTs 可以更有效地编码一些东西，你可以写针对您的数据类型的函数可以强制执行更强的不变量。

随着您开始使越来越多的属性可静态验证，对不变量进行编码可能会变得更加复杂。这就是 GADT、类型族和其他扩展可以开始提供帮助的时候。