11

我想在 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 在设计上不支持字符串比较。

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

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

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

4

1 回答 1

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 这样的非递归语言中嵌入递归数据结构和递归函数。其实有两种方法！

  • F-代数- 用于实现递归
  • F- coalgebras - 用于实现“corecursion”

我读到的第一个让我了解这个技巧的东西是 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您可以为它们提供所需递归或“核心递归”类型的“一层”（即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是在没有语言支持的情况下实现的 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

... where与上一个公式中的作用相同，并且与上一个公式forall (Graph : Type)中的作用相同。forall xforall (Node : Type)forall y

于 2020-02-27T17:01:09.780 回答