Может ли тип действительных графиков быть закодирован в Dhall?

Я хотел бы представить вики (набор документов, содержащих ориентированный граф) в 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

Как видно из этого примера, этот тип допускает значения, которые не соответствуют действительным графам (нет узла с идентификатором «b», но узел с идентификатором «a» предусматривает соседа с идентификатором «b»). Более того, невозможно сгенерировать список этих проблем, сворачивая соседей каждого узла, потому что Dhall не поддерживает сравнение строк по конструкции.

Есть ли какое-либо представление, которое позволило бы либо вычислить список неработающих ссылок, либо исключить неработающие ссылки через систему типов?

ОБНОВЛЕНИЕ: Я только что обнаружил, что Naturals сопоставимы в Dhall. Поэтому я полагаю, что можно было бы написать функцию для идентификации любых недопустимых ребер («неработающие ссылки») и дублирования использования идентификатора, если идентификаторы были Naturals.

Оригинальный вопрос о том, можно ли определить тип графика, остается.

Да, вы можете смоделировать безопасный по типу направленный, возможно, циклический граф в 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представление на самом деле является OUR 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работа заключается в том, что вы можете дать им «один слой» желаемого рекурсивного или «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), который мы используем в качестве заполнителя для всех рекурсивных / corecursive вхождений типа.

Теперь, оснащенный ListF, мы можем определить рекурсивные и corecursive списки следующим образом:

type List a = LFix (ListF a)

type CoList a = GFix (ListF a)

... где:

• List рекурсивный список, реализованный без языковой поддержки рекурсии
• CoList это список corecursive, реализованный без поддержки языка для corecursion

Оба эти типа эквивалентны («изоморфны») [], что означает, что:

• Вы можете конвертировать обратно и вперед между 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 ] })

Теперь это начинает выглядеть как тип Dhall для a Graph, особенно если мы заменим xна node:

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

Тем не менее, есть еще одна сложная часть, которая заключается в том, как перевести ExistentialQuantificationиз Хаскелла в Далла. Оказывается, что вы всегда можете перевести экзистенциальную квантификацию в универсальную квантификацию (то есть forall), используя следующую эквивалентность:

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

Я считаю, что это называется "сколемизация"

Для более подробной информации смотрите:

• Википедия - экзистенциальная квантификация

... и этот последний трюк дает вам тип 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в предыдущей формуле.