小编Bjø*_*ard的帖子

可以在 Dhall 中编码有效图形的类型吗?

我想在 Dhall 中表示一个 wiki(一组包含有向图的文档)。这些文档将呈现为 HTML,我想防止生成断开的链接。在我看来,这可以通过使无效图(带有指向不存在节点的链接的图)无法通过类型系统表示或编写一个函数来返回任何可能图中的错误列表(例如“在可能的图中X,节点 A 包含指向不存在的节点 B 的链接”)。

一个简单的邻接列表表示可能看起来像这样:

let Node : Type = {
    id: Text,
    neighbors: List Text
}
let Graph : Type = List Node
let example : Graph = [
    { id = "a", neighbors = ["b"] }
]
in example
Run Code Online (Sandbox Code Playgroud)

正如这个例子所表明的那样,这种类型接受与有效图不对应的值(没有 id 为“b”的节点,但 id 为“a”的节点规定了一个 id 为“b”的邻居)。此外,不可能通过折叠每个节点的邻居来生成这些问题的列表,因为 Dhall 设计上不支持字符串比较。

是否有任何表示可以允许计算断开的链接列表或通过类型系统排除断开的链接?

更新:我刚刚发现 Naturals 在 Dhall 中具有可比性。所以我想可以编写一个函数来识别任何无效的边缘(“断开的链接”),如果标识符是自然的,则重复使用标识符。

但是,是否可以定义 Graph 类型的原始问题仍然存在。

graph adjacency-list dhall

11
推荐指数
1
解决办法
1108
查看次数

标签 统计

adjacency-list ×1

dhall ×1

graph ×1