Le type de graphiques valides peut-il être encodé dans Dhall?

Je voudrais représenter un wiki (un ensemble de documents comprenant un graphique dirigé) dans Dhall. Ces documents seront rendus au format HTML, et j'aimerais empêcher la création de liens rompus. Comme je le vois, cela pourrait être accompli soit en rendant les graphiques invalides (graphiques avec des liens vers des nœuds inexistants) non représentables via le système de type ou en écrivant une fonction pour renvoyer une liste d'erreurs dans tout graphique possible (par exemple, "Dans un graphique possible X, le nœud A contient un lien vers un nœud B inexistant ").

Une représentation de liste d'adjacence naïve pourrait ressembler à ceci:

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

Comme cet exemple le montre clairement, ce type admet des valeurs qui ne correspondent pas à des graphiques valides (il n'y a pas de nœud avec un identifiant "b", mais le nœud avec l'identifiant "a" stipule un voisin avec l'identifiant "b"). De plus, il n'est pas possible de générer une liste de ces problèmes en repliant les voisins de chaque nœud, car Dhall ne prend pas en charge la comparaison de chaînes par conception.

Existe-t-il une représentation qui permettrait soit le calcul d'une liste de liens rompus, soit l'exclusion de liens rompus via le système de types?

MISE À JOUR: Je viens de découvrir que les produits naturels sont comparables dans Dhall. Je suppose donc qu'une fonction pourrait être écrite pour identifier les bords non valides ("liens rompus") et les utilisations en double d'un identifiant si les identifiants étaient des produits naturels.

La question initiale, cependant, de savoir si un type de graphique peut être défini, demeure.

Oui, vous pouvez modéliser un graphique de type sécurisé, dirigé, éventuellement cyclique dans Dhall, comme ceci:

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

Cette représentation garantit l'absence de bords cassés.

J'ai également transformé cette réponse en un package que vous pouvez utiliser:

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

Modifier: Voici des ressources pertinentes et des explications supplémentaires qui peuvent aider à éclairer ce qui se passe:

Commencez d'abord par le type Haskell suivant pour un arbre :

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

Vous pouvez considérer ce type comme une structure de données paresseuse et potentiellement infinie représentant ce que vous obtiendriez si vous continuiez à visiter des voisins.

Maintenant, supposons que la Treereprésentation ci-dessus est réellement la notre Graphen renommant simplement le type de données en Graph:

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

... mais même si nous voulions utiliser ce type, nous n'avons pas de moyen de modéliser directement ce type dans Dhall parce que le langage Dhall ne fournit pas de support intégré pour les structures de données récursives. Alors que faisons-nous?

Heureusement, il existe en fait un moyen d'incorporer des structures de données récursives et des fonctions récursives dans un langage non récursif comme Dhall. En fait, il y a deux façons!

• Algèbres F - Utilisées pour implémenter la récursivité
• F-coalgebras - Utilisé pour implémenter la "corecursion"

La première chose que j'ai lue qui m'a présenté cette astuce a été le brouillon suivant de Wadler:

• Types récursifs gratuits!

... mais je peux résumer l'idée de base en utilisant les deux types Haskell suivants:

{-# LANGUAGE RankNTypes #-}

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

... et:

{-# LANGUAGE ExistentialQuantification #-}

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

La façon dont cela LFixet le GFixtravail sont que vous pouvez leur donner "une couche" de votre type récursif ou "corécursif" souhaité (c'est-à-dire le f) et ils vous donnent alors quelque chose qui est aussi puissant que le type souhaité sans nécessiter le support de la langue pour la récursivité ou la corécursion .

Prenons l'exemple des listes. Nous pouvons modéliser "une couche" d'une liste en utilisant le ListFtype suivant :

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

Comparez cette définition à la façon dont nous définirions normalement une OrdinaryListdéfinition de type de données récursive ordinaire:

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

La principale différence est qu'il ListFprend un paramètre de type supplémentaire ( next), que nous utilisons comme espace réservé pour toutes les occurrences récursives / corécursives du type.

Maintenant, équipé de ListF, nous pouvons définir des listes récursives et corécursives comme ceci:

type List a = LFix (ListF a)

type CoList a = GFix (ListF a)

... où:

• List est une liste récursive implémentée sans prise en charge linguistique pour la récursivité
• CoList est une liste corecursive implémentée sans prise en charge linguistique pour la corecursion

Ces deux types sont équivalents à ("isomorphic to") [], ce qui signifie que:

• Vous pouvez convertir et inverser de façon réversible entre Listet[]
• Vous pouvez convertir et inverser de façon réversible entre CoListet[]

Prouvons cela en définissant ces fonctions de conversion!

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

La première étape de la mise en œuvre du type Dhall a donc consisté à convertir le Graphtype récursif :

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

... à la représentation co-récursive équivalente:

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)

... bien que pour simplifier un peu les types, je trouve qu'il est plus facile de se spécialiser GFixdans le cas où f = GraphF:

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

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

Haskell n'a pas d'enregistrements anonymes comme Dhall, mais si c'était le cas, nous pourrions simplifier davantage le type en insérant la définition de GraphF:

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

Maintenant, cela commence à ressembler au type Dhall pour a Graph, surtout si nous le remplaçons xpar node:

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

Cependant, il y a encore une dernière partie délicate, qui est de savoir comment traduire ExistentialQuantificationHaskell en Dhall. Il s'avère que vous pouvez toujours traduire la quantification existentielle en quantification universelle (c'est-à-dire forall) en utilisant l'équivalence suivante:

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

Je crois que cela s'appelle la "skolémisation"

Pour plus de détails, voir:

• Wikipedia - Quantification existentielle

... et cette dernière astuce vous donne le type Dhall:

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

... où forall (Graph : Type)joue le même rôle que forall xdans la formule précédente et forall (Node : Type)joue le même rôle que forall ydans la formule précédente.