Dhall 中是否能够编码有效图的类型？

Question

我想在Dhall中代表一个维基（由有向图组成的一组文档）。这些文档将呈现为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不支持字符串比较设计。

是否存在一种表示方式，既可以计算出损坏链接的列表，也可以通过类型系统排除损坏链接？

更新：我刚刚发现，Dhall中的自然数是可比较的。因此，如果标识符是自然数，则可以编写一个函数来识别任何无效边缘（“损坏链接”）和标识符的重复使用。

然而，关于是否可以定义Graph类型的原始问题仍然存在。

- Bjørn Westergard

---

将图形表示为边的列表。节点可以从现有的边推断出来。每条边都由源节点和目标节点组成，但为了容纳未连接的节点，目标节点可以是可选的。 - chepner

Answer 1

是的，你可以用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" ]

这种表示方式可以保证边不会断裂。

我还将这个答案转化为一个可以使用的包：

• https://github.com/Gabriel439/graph

编辑:下面是相关资源和额外的解释，可以帮助说明正在发生什么:

首先，从以下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）中嵌入递归数据结构和递归函数。事实上，有两种方法！

• F-代数 - 用于实现递归
• F-余代数 - 用于实现“核递归”

我读到的第一篇介绍这个技巧的文章是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）的“一层”，然后它们会为您提供与所需类型一样强大的东西，而无需语言支持递归或核递归。

我们以列表为例。 我们可以使用以下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 是一种没有核递归语言支持的核递归列表实现

这两种类型都等同于 ("同构于") []，这意味着:

• 您可以在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 ] })

现在这看起来像是关于Graph的Dhall类型，特别是如果我们用node代替x：

data Graph a = forall node . MakeGraph node (node -> { id :: a, neighbors :: [ node ] })

然而，还有最后一个棘手的部分，就是如何将Haskell中的ExistentialQuantification翻译成Dhall。事实证明，您始终可以使用以下等价关系将存在量词翻译为全称量词（即forall）：

exists y . f y ≅ forall x . (forall y . f y -> x) -> x

我相信这被称为“Skolem化”。

更多细节请参见：

• 维基百科 - 存在量词

...并且这个最后的技巧给你了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相同。

- Gabriella Gonzalez

---

非常感谢您的回答，以及为开发Dhall所需的所有辛勤工作！您能否建议一些材料供新手阅读，以更好地了解您在这里所做的事情，以及可能存在的其他图形表示形式？我想能够通过深度优先搜索从您的Graph类型的任何值中生成邻接列表表示形式的函数来扩展您在这里所做的工作。 - Bjørn Westergard

谢谢您的选择！以下是我翻译后的结果：@BjørnWestergard：不用谢！我编辑了我的回答，解释了它背后的理论，并包括有用的参考资料。 - Gabriella Gonzalez