O tipo de gráfico válido pode ser codificado em Dhall?

Eu gostaria de representar um wiki (um conjunto de documentos que inclui um gráfico direcionado) em Dhall. Esses documentos serão renderizados em HTML e eu gostaria de impedir que links quebrados sejam gerados. Na minha opinião, isso pode ser feito tornando gráficos inválidos (gráficos com links para nós inexistentes) não representáveis ​​através do sistema de tipos ou escrevendo uma função para retornar uma lista de erros em qualquer gráfico possível (por exemplo, "Em gráfico possível" X, Nó A contém um link para um Nó B inexistente ").

Uma representação ingênua da lista de adjacências pode se parecer com isso:

let Node : Type = {
    id: Text,
    neighbors: List Text
}
let Graph : Type = List Node
let example : Graph = [
    { id = "a", neighbors = ["b"] }
]
in example

Como este exemplo evidencia, esse tipo admite valores que não correspondem a gráficos válidos (não há nó com o ID "b", mas o nó com o ID "a" estipula um vizinho com o ID "b"). Além disso, não é possível gerar uma lista desses problemas dobrando os vizinhos de cada Nó, porque o Dhall não suporta comparação de cadeias por design.

Existe alguma representação que permita o cálculo de uma lista de links quebrados ou a exclusão de links quebrados através do sistema de tipos?

ATUALIZAÇÃO: Acabei de descobrir que os Naturals são comparáveis ​​em Dhall. Portanto, suponho que uma função possa ser escrita para identificar quaisquer arestas inválidas ("links quebrados") e duplicar os usos de um identificador se os identificadores fossem Naturals.

A questão original, no entanto, sobre se um tipo de gráfico pode ser definido, permanece.

Sim, você pode modelar um gráfico de tipo seguro, direcionado e possivelmente cíclico no Dhall, assim:

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" ]

Essa representação garante a ausência de arestas quebradas.

Também transformei esta resposta em um pacote que você pode usar:

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

Editar: Aqui estão recursos relevantes e explicações adicionais que podem ajudar a esclarecer o que está acontecendo:

Primeiro, comece pelo seguinte tipo de Haskell para uma árvore :

data Tree a = Node { id :: a, neighbors :: [ Tree a ] }

Você pode pensar nesse tipo como uma estrutura de dados lenta e potencialmente infinita, representando o que você obteria se apenas continuasse visitando vizinhos.

Agora, vamos fingir que a Treerepresentação acima é realmente nossa Graphapenas renomeando o tipo de dados para Graph:

data Graph a = Node { id :: a, neighbors :: [ Graph a ] }

... mas mesmo que desejássemos usar esse tipo, não temos como modelar diretamente esse tipo no Dhall porque a linguagem Dhall não fornece suporte interno para estruturas de dados recursivas. Então, o que fazemos?

Felizmente, existe realmente uma maneira de incorporar estruturas de dados recursivas e funções recursivas em uma linguagem não recursiva como Dhall. De fato, existem duas maneiras!

• Álgebras F - Usadas para implementar recursão
• F-coalgebras - Usado para implementar "corecursão"

A primeira coisa que li que me apresentou a esse truque foi o seguinte rascunho de Wadler:

• Tipos recursivos de graça!

... mas posso resumir a ideia básica usando os dois seguintes tipos de Haskell:

{-# LANGUAGE RankNTypes #-}

-- LFix is short for "Least fixed point"
newtype LFix f = LFix (forall x . (f x -> x) -> x)

... e:

{-# LANGUAGE ExistentialQuantification #-}

-- GFix is short for "Greatest fixed point"
data GFix f = forall x . GFix x (x -> f x)

A maneira que LFixe GFixtrabalho é que você pode dar-lhes "uma camada" de sua recursiva desejado ou tipo "corecursive" (ou seja, of ) e, em seguida, dar-lhe algo que é tão poderoso como o tipo desejado sem a necessidade de suporte de idioma para a recursividade ou corecursion .

Vamos usar listas como um exemplo. Podemos modelar "uma camada" de uma lista usando o seguinte ListFtipo:

-- `ListF` is short for "List functor"
data ListF a next = Nil | Cons a next

Compare essa definição com a forma como normalmente definiríamos uma OrdinaryListdefinição de tipo de dados recursivo comum:

data OrdinaryList a = Nil | Cons a (OrdinaryList a)

A principal diferença é que ListFleva um parâmetro de tipo extra (next ), que usamos como espaço reservado para todas as ocorrências recursivas / corecursivas do tipo.

Agora, equipado com ListF, podemos definir listas recursivas e corecursivas como esta:

type List a = LFix (ListF a)

type CoList a = GFix (ListF a)

... Onde:

• List é uma lista recursiva implementada sem suporte ao idioma para recursão
• CoList é uma lista corecursiva implementada sem suporte ao idioma para corecursão

Ambos os tipos são equivalentes a ("isomórfico para") [], significando que:

• Você pode converter e voltar reversivelmente entre Liste[]
• Você pode converter e voltar reversivelmente entre CoListe[]

Vamos provar que, definindo essas funções de conversão!

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

Portanto, o primeiro passo na implementação do tipo Dhall foi converter o Graphtipo recursivo :

data Graph a = Node { id :: a, neighbors :: [ Graph a ] }

... à representação co-recursiva equivalente:

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)

... embora para simplificar um pouco os tipos, acho mais fácil me especializar GFixno caso em que f = GraphF:

data GraphF a next = Node { id ::: a, neighbors :: [ next ] }

data Graph a = forall x . Graph x (x -> GraphF a x)

Haskell não possui registros anônimos como Dhall, mas, se o tivesse, poderíamos simplificar ainda mais o tipo ao incluir a definição de GraphF:

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

Agora, isso está começando a se parecer com o tipo Dhall para a Graph, especialmente se substituirmos xpor node:

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

No entanto, ainda há uma última parte complicada, que é como traduzir o ExistentialQuantificationde Haskell para Dhall. Acontece que você sempre pode converter quantificação existencial em quantificação universal (ou seja forall) usando a seguinte equivalência:

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

Eu acredito que isso se chama "skolemization"

Para mais detalhes, consulte:

• Wikipedia - Quantificação Existencial

... e esse truque final fornece o tipo de Dhall:

let Graph
    : Type
    =     forall (Graph : Type)
      ->  forall  ( MakeGraph
                  :     forall (Node : Type)
                    ->  Node
                    ->  (Node -> { id : Text, neighbors : List Node })
                    ->  Graph
                  )
      ->  Graph

... onde forall (Graph : Type)desempenha o mesmo papel que forall xna fórmula anterior e forall (Node : Type)desempenha o mesmo papel que forall yna fórmula anterior.