¿Se puede codificar el tipo de gráficos válidos en Dhall?

Me gustaría representar una wiki (un conjunto de documentos que comprende un gráfico dirigido) en Dhall. Estos documentos se representarán en HTML y me gustaría evitar que se generen enlaces rotos. A mi entender, esto podría lograrse haciendo gráficos no válidos (gráficos con enlaces a nodos no existentes) no representables a través del sistema de tipos o escribiendo una función para devolver una lista de errores en cualquier gráfico posible (por ejemplo, "En un gráfico posible X, el Nodo A contiene un enlace a un Nodo B inexistente ").

Una representación ingenua de la lista de adyacencia podría verse así:

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

Como este ejemplo hace evidente, este tipo admite valores que no corresponden a gráficos válidos (no hay ningún nodo con una identificación de "b", pero el nodo con la identificación "a" estipula un vecino con la identificación "b"). Además, no es posible generar una lista de estos problemas doblando los vecinos de cada Nodo, porque Dhall no admite la comparación de cadenas por diseño.

¿Hay alguna representación que permita el cálculo de una lista de enlaces rotos o la exclusión de enlaces rotos a través del sistema de tipos?

ACTUALIZACIÓN: Acabo de descubrir que los productos naturales son comparables en Dhall. Así que supongo que se podría escribir una función para identificar cualquier borde no válido ("enlaces rotos") y usos duplicados de un identificador si los identificadores fueran naturales.

Sin embargo, la pregunta original es si se puede definir un tipo de Gráfico.

Sí, puede modelar un gráfico de tipo seguro, dirigido, posiblemente cíclico, en Dhall, así:

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

Esta representación garantiza la ausencia de bordes rotos.

También convertí esta respuesta en un paquete que puedes usar:

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

Editar: Aquí hay recursos relevantes y explicaciones adicionales que pueden ayudar a iluminar lo que está sucediendo:

Primero, comience desde el siguiente tipo de Haskell para un árbol :

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

Puede pensar en este tipo como una estructura de datos perezosa y potencialmente infinita que representa lo que obtendría si siguiera visitando vecinos.

Ahora, supongamos que la Treerepresentación anterior en realidad es nuestra Graphsimplemente cambiando el nombre del tipo de datos a Graph:

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

... pero incluso si quisiéramos usar este tipo, no tenemos una forma de modelar directamente ese tipo en Dhall porque el lenguaje Dhall no proporciona soporte incorporado para estructuras de datos recursivas. ¿Asi que que hacemos?

Afortunadamente, en realidad hay una manera de integrar estructuras de datos recursivas y funciones recursivas en un lenguaje no recursivo como Dhall. De hecho, hay dos maneras!

• Álgebras F : se utilizan para implementar la recursividad
• F-coalgebras - Utilizado para implementar "corecursion"

Lo primero que leí que me presentó este truco fue el siguiente borrador de Wadler:

• Tipos recursivos gratis!

... pero puedo resumir la idea básica usando los siguientes dos tipos de Haskell:

{-# LANGUAGE RankNTypes #-}

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

... y:

{-# LANGUAGE ExistentialQuantification #-}

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

La forma LFixy el GFixtrabajo es que puede darles "una capa" de su tipo recursivo o "corecursive" deseado (es decir, el f) y luego le dan algo tan poderoso como el tipo deseado sin necesidad de soporte de idioma para la recursión o corecursion .

Usemos las listas como ejemplo. Podemos modelar "una capa" de una lista usando el siguiente ListFtipo:

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

Compare esa definición con la forma en que normalmente definiríamos un OrdinaryListuso de una definición de tipo de datos recursiva ordinaria:

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

La principal diferencia es que ListFtoma un parámetro de tipo adicional ( next), que usamos como marcador de posición para todas las ocurrencias recursivas / corecursive del tipo.

Ahora, equipados con ListF, podemos definir listas recursivas y corecursive como esta:

type List a = LFix (ListF a)

type CoList a = GFix (ListF a)

... dónde:

• List es una lista recursiva implementada sin soporte de idioma para la recursividad
• CoList es una lista corecursive implementada sin soporte de lenguaje para corecursion

Ambos tipos son equivalentes a ("isomorfo a") [], lo que significa que:

• Puede convertir reversiblemente de ida y vuelta entre Listy[]
• Puede convertir reversiblemente de ida y vuelta entre CoListy[]

¡Probemos eso definiendo esas funciones de conversión!

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

Entonces, el primer paso para implementar el tipo Dhall fue convertir el Graphtipo recursivo :

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

... a la representación 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)

... aunque para simplificar un poco los tipos, creo que es más fácil especializarse GFixen el caso donde f = GraphF:

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

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

Haskell no tiene registros anónimos como Dhall, pero si los tuviera, podríamos simplificar aún más el tipo al incluir la definición de GraphF:

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

Ahora esto comienza a parecerse al tipo Dhall para a Graph, especialmente si lo reemplazamos xcon node:

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

Sin embargo, todavía hay una última parte difícil, que es cómo traducir el ExistentialQuantificationde Haskell a Dhall. Resulta que siempre puedes traducir la cuantificación existencial a la cuantificación universal (es decir forall) usando la siguiente equivalencia:

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

Creo que esto se llama "skolemization"

Para más detalles, ver:

• Wikipedia - Cuantificación existencial

... y ese truco final te da el tipo Dhall:

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

... donde forall (Graph : Type)juega el mismo papel que forall xen la fórmula anterior y forall (Node : Type)juega el mismo papel que forall yen la fórmula anterior.