Bjø*_*ard 11 graph adjacency-list 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
正如这个例子所表明的那样，这种类型接受与有效图不对应的值（没有 id 为“b”的节点，但 id 为“a”的节点规定了一个 id 为“b”的邻居）。此外，不可能通过折叠每个节点的邻居来生成这些问题的列表，因为 Dhall 设计上不支持字符串比较。
是否有任何表示可以允许计算断开的链接列表或通过类型系统排除断开的链接？
更新：我刚刚发现 Naturals 在 Dhall 中具有可比性。所以我想可以编写一个函数来识别任何无效的边缘（“断开的链接”），如果标识符是自然的，则重复使用标识符。
但是，是否可以定义 Graph 类型的原始问题仍然存在。
Gab*_*lez 20
是的，您可以在 Dhall 中对类型安全、有向、可能是循环的图形进行建模，如下所示：
let List/map =
https://prelude.dhall-lang.org/v14.0.0/List/map sha256:dd845ffb4568d40327f2a817eb42d1c6138b929ca758d50bc33112ef3c885680
let Graph
: Type
= forall (Graph : Type)
-> forall ( MakeGraph
: forall (Node : Type)
-> Node
-> (Node -> { id : Text, neighbors : List Node })
-> Graph
)
-> Graph
let MakeGraph
: forall (Node : Type)
-> Node
-> (Node -> { id : Text, neighbors : List Node })
-> Graph
= \(Node : Type)
-> \(current : Node)
-> \(step : Node -> { id : Text, neighbors : List Node })
-> \(Graph : Type)
-> \ ( MakeGraph
: forall (Node : Type)
-> Node
-> (Node -> { id : Text, neighbors : List Node })
-> Graph
)
-> MakeGraph Node current step
let -- Get `Text` label for the current node of a Graph
id
: Graph -> Text
= \(graph : Graph)
-> graph
Text
( \(Node : Type)
-> \(current : Node)
-> \(step : Node -> { id : Text, neighbors : List Node })
-> (step current).id
)
let -- Get all neighbors of the current node
neighbors
: Graph -> List Graph
= \(graph : Graph)
-> graph
(List Graph)
( \(Node : Type)
-> \(current : Node)
-> \(step : Node -> { id : Text, neighbors : List Node })
-> let neighborNodes
: List Node
= (step current).neighbors
let nodeToGraph
: Node -> Graph
= \(node : Node)
-> \(Graph : Type)
-> \ ( MakeGraph
: forall (Node : Type)
-> forall (current : Node)
-> forall ( step
: Node
-> { id : Text
, neighbors : List Node
}
)
-> Graph
)
-> MakeGraph Node node step
in List/map Node Graph nodeToGraph neighborNodes
)
let {- Example node type for a graph with three nodes
For your Wiki, replace this with a type with one alternative per document
-}
Node =
< Node0 | Node1 | Node2 >
let {- Example graph with the following nodes and edges between them:
Node0 ? Node1
?
Node2
?
The starting node is Node0
-}
example
: Graph
= let step =
\(node : Node)
-> merge
{ Node0 = { id = "0", neighbors = [ Node.Node1, Node.Node2 ] }
, Node1 = { id = "1", neighbors = [ Node.Node0 ] }
, Node2 = { id = "2", neighbors = [ Node.Node2 ] }
}
node
in MakeGraph Node Node.Node0 step
in assert : List/map Graph Text id (neighbors example) === [ "1", "2" ]
这种表示保证不存在断边。
我还把这个答案变成了一个你可以使用的包：
编辑：以下是相关资源和其他解释，可以帮助阐明正在发生的事情：
首先，从树的以下 Haskell 类型开始：
data Tree a = Node { id :: a, neighbors :: [ Tree a ] }
您可以将这种类型视为一种惰性且可能无限的数据结构，表示如果您继续访问邻居，您会得到什么。
现在，让我们假设上面的Tree表示实际上是我们的Graph，只需将数据类型重命名为Graph：
data Graph a = Node { id :: a, neighbors :: [ Graph a ] }
...但即使我们想使用这种类型，我们也没有办法在 Dhall 中直接对该类型进行建模，因为 Dhall 语言不提供对递归数据结构的内置支持。那么我们该怎么办？
幸运的是，实际上有一种方法可以在像 Dhall 这样的非递归语言中嵌入递归数据结构和递归函数。其实有两种方法！
我读到的第一件事是让我了解这个技巧，这是 Wadler 的以下草稿：
...但我可以使用以下两种 Haskell 类型来总结基本思想：
{-# LANGUAGE RankNTypes #-}
-- LFix is short for "Least fixed point"
newtype LFix f = LFix (forall x . (f x -> x) -> x)
... 和：
{-# LANGUAGE ExistentialQuantification #-}
-- GFix is short for "Greatest fixed point"
data GFix f = forall x . GFix x (x -> f x)
的方式，LFix和GFix工作是，你可以给他们“一层”你想要的递归的或“corecursive”型（即f），然后他们给你的东西是一样强大的所需的类型，而不需要递归或corecursion语言支持.
让我们以列表为例。我们可以使用以下ListF类型对列表的“一层”建模：
-- `ListF` is short for "List functor"
data ListF a next = Nil | Cons a next
将该定义与我们通常OrdinaryList使用普通递归数据类型定义的方式进行比较：
data OrdinaryList a = Nil | Cons a (OrdinaryList a)
主要区别在于它ListF需要一个额外的类型参数 ( next)，我们将其用作所有递归/核心递归出现的类型的占位符。
现在，有了ListF，我们可以像这样定义递归和核心递归列表：
type List a = LFix (ListF a)
type CoList a = GFix (ListF a)
... 在哪里：
List 是在没有语言支持递归的情况下实现的递归列表CoList 是在没有对 corecursion 的语言支持的情况下实现的 corecursive 列表这两种类型都等价于 ("isomorphic to") []，意思是：
List和之间可逆地来回转换[]CoList和之间可逆地来回转换[]让我们通过定义这些转换函数来证明这一点！
fromList :: List a -> [a]
fromList (LFix f) = f adapt
where
adapt (Cons a next) = a : next
adapt Nil = []
toList :: [a] -> List a
toList xs = LFix (\k -> foldr (\a x -> k (Cons a x)) (k Nil) xs)
fromCoList :: CoList a -> [a]
fromCoList (GFix start step) = loop start
where
loop state = case step state of
Nil -> []
Cons a state' -> a : loop state'
toCoList :: [a] -> CoList a
toCoList xs = GFix xs step
where
step [] = Nil
step (y : ys) = Cons y ys
所以实现 Dhall 类型的第一步是转换递归Graph类型：
data Graph a = Node { id :: a, neighbors :: [ Graph a ] }
...到等效的共同递归表示：
data GraphF a next = Node { id ::: a, neighbors :: [ next ] }
data GFix f = forall x . GFix x (x -> f x)
type Graph a = GFix (GraphF a)
...虽然为了稍微简化类型，我发现专注GFix于以下情况更容易f = GraphF：
data GraphF a next = Node { id ::: a, neighbors :: [ next ] }
data Graph a = forall x . Graph x (x -> GraphF a x)
Haskell 没有像 Dhall 那样的匿名记录，但如果有，那么我们可以通过内联 的定义来进一步简化类型GraphF：
data Graph a = forall x . MakeGraph x (x -> { id :: a, neighbors :: [ x ] })
现在这开始看起来像 a 的 Dhall 类型Graph，特别是如果我们替换x为node：
data Graph a = forall node . MakeGraph node (node -> { id :: a, neighbors :: [ node ] })
然而，还有最后一个棘手的部分，就是如何将ExistentialQuantificationHaskell翻译成 Dhall。事实证明，您始终可以forall使用以下等价将存在量化转换为全称量化（即）：
exists y . f y ? forall x . (forall y . f y -> x) -> x
我相信这被称为“skolemization”
有关更多详细信息，请参阅：
...最后一个技巧为您提供了 Dhall 类型：
let Graph
: Type
= forall (Graph : Type)
-> forall ( MakeGraph
: forall (Node : Type)
-> Node
-> (Node -> { id : Text, neighbors : List Node })
-> Graph
)
-> Graph
...其中forall (Graph : Type)扮演着相同的角色forall x前面的公式中，并forall (Node : Type)扮演着相同的角色forall y以前的配方食品中。