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

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中,每个元素节点只能出现在正确的上下文中,并且每个元素对应于其子元素的不同上下文.例如:

• 像img这样的无效元素有一个空的上下文模型,不允许有任何子元素.
• 具有文本内容模型的元素(例如标题)只能将文本节点作为子元素(不允许嵌套标记)
• div元素不能出现在Phrasing上下文中,因此不允许作为span元素的后代.

所以我的问题是:

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

   我想我们可能必须为不同的上下文创建许多不同的数据类型,但我不知道如何以原则和清晰的方式执行此操作.我怎么能这样做而不会迷路,折叠功能最终会是什么样的？

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

   我有预感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.

使用GADT,可以更有效地编码某些内容,并且可以在数据类型上编写可以强制执行更强不变量的函数.

当您开始使越来越多的属性可以进行静态验证时,对不变量进行编码可能会变得更加复杂.那时GADT,类型系列和其他扩展可以开始提供帮助.