Czy typ prawidłowych wykresów można zakodować w Dhall?

Chciałbym reprezentować wiki (zestaw dokumentów zawierający ukierunkowany wykres) w Dhall. Te dokumenty zostaną wyrenderowane w formacie HTML i chciałbym zapobiec generowaniu niedziałających linków. Moim zdaniem można to osiągnąć albo przez to, że nieprawidłowe wykresy (wykresy z linkami do nieistniejących węzłów) nie będą reprezentowalne przez system typów, albo przez napisanie funkcji zwracającej listę błędów na dowolnym możliwym wykresie (np. „Na możliwym wykresie” X, Węzeł A zawiera łącze do nieistniejącego Węzła B ”).

Naiwna reprezentacja listy przylegania może wyglądać mniej więcej tak:

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

Jak pokazuje ten przykład, ten typ dopuszcza wartości, które nie odpowiadają prawidłowym wykresom (nie ma węzła o identyfikatorze „b”, ale węzeł o identyfikatorze „a” określa sąsiada o identyfikatorze „b”). Co więcej, nie jest możliwe wygenerowanie listy tych problemów poprzez złożenie sąsiadów każdego węzła, ponieważ Dhall nie obsługuje porównania ciągów według projektu.

Czy istnieje jakakolwiek reprezentacja, która pozwoliłaby na obliczenie listy uszkodzonych łączy lub wykluczenie uszkodzonych linków przez system typów?

AKTUALIZACJA: Właśnie odkryłem, że Naturals są porównywalne w Dhall. Podejrzewam więc, że można by napisać funkcję identyfikującą wszelkie nieprawidłowe krawędzie („zepsute linki”) i powielającą użycie identyfikatora, gdyby były to Naturals.

Pozostaje jednak pierwotne pytanie, czy można zdefiniować typ wykresu.

Tak, możesz modelować wykres typu bezpieczny, ukierunkowany, być może cykliczny w Dhall, w następujący sposób:

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

Ta reprezentacja gwarantuje brak złamanych krawędzi.

Zmieniłem również tę odpowiedź w pakiet, którego możesz użyć:

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

Edycja: Oto odpowiednie zasoby i dodatkowe wyjaśnienia, które mogą pomóc wyjaśnić, co się dzieje:

Najpierw zacznij od następującego typu Haskell dla drzewa :

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

Możesz myśleć o tym typie jako o leniwej i potencjalnie nieskończonej strukturze danych reprezentującej to, co byś otrzymał, gdybyś tylko odwiedzał sąsiadów.

Teraz udawajmy, że powyższa Treereprezentacja faktycznie jest nasza Graph, zmieniając po prostu nazwę typu danych na Graph:

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

... ale nawet gdybyśmy chcieli użyć tego typu, nie mamy możliwości bezpośredniego modelowania tego typu w Dhall, ponieważ język Dhall nie zapewnia wbudowanej obsługi struktur danych rekurencyjnych. Więc co robimy?

Na szczęście istnieje sposób na osadzenie struktur danych rekurencyjnych i funkcji rekurencyjnych w nierekurencyjnym języku, takim jak Dhall. W rzeczywistości istnieją dwa sposoby!

• Algebry F - Służy do realizacji rekurencji
• F-carbongebras - Używany do implementacji „corecursion”

Pierwszą rzeczą, którą przeczytałem, która zapoznała mnie z tą sztuczką, był następujący szkic posta Wadlera:

• Rodzaje rekurencyjne za darmo!

... ale mogę podsumować podstawowy pomysł, używając następujących dwóch typów Haskell:

{-# LANGUAGE RankNTypes #-}

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

... i:

{-# LANGUAGE ExistentialQuantification #-}

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

Sposób, że LFixi GFixpraca jest, że można dać im „jedną warstwę” żądanej rekursywne lub „corecursive” typ (tj f) i następnie daje coś, co jest tak potężny jak żądanego typu bez konieczności wsparcia językowego dla rekursji lub corecursion .

Użyjmy list jako przykładu. Możemy modelować „jedną warstwę” listy, używając następującego ListFtypu:

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

Porównaj tę definicję z tym, jak normalnie zdefiniowalibyśmy OrdinaryListzwykłą rekurencyjną definicję typu danych:

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

Główną różnicą jest to, że ListFpobiera jeden dodatkowy parametr type ( next), którego używamy jako symbolu zastępczego dla wszystkich rekurencyjnych / corecursive wystąpień tego typu.

Teraz, wyposażeni w ListF, możemy zdefiniować listy rekurencyjne i współbieżne w następujący sposób:

type List a = LFix (ListF a)

type CoList a = GFix (ListF a)

... gdzie:

• List to lista rekurencyjna zaimplementowana bez obsługi języka dla rekurencji
• CoList to lista Corecursive zaimplementowana bez obsługi języka dla Corecursion

Oba te typy są równoważne („izomorficzny z”) [], co oznacza, że:

• Możesz konwertować odwracalnie tam iz powrotem pomiędzy Listi[]
• Możesz konwertować odwracalnie tam iz powrotem pomiędzy CoListi[]

Udowodnijmy to, definiując funkcje konwersji!

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

Pierwszym krokiem w implementacji typu Dhall była konwersja Graphtypu rekurencyjnego :

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

... do równoważnej reprezentacji ko-rekurencyjnej:

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)

... chociaż trochę upraszczając typy, łatwiej jest specjalizować GFixsię w przypadku, w którym f = GraphF:

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

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

Haskell nie ma anonimowych rekordów takich jak Dhall, ale gdyby tak było, moglibyśmy jeszcze bardziej uprościć typ, wprowadzając definicję GraphF:

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

Teraz zaczyna to wyglądać typu Dhall dotyczący Graphzwłaszcza jeśli zastąpimy xz node:

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

Jednak jest jeszcze jedna trudna część, która polega na przetłumaczeniu ExistentialQuantificationHaskella na Dhall. Okazuje się, że zawsze można przełożyć kwantyfikację egzystencjalną na kwantyfikację uniwersalną (tj. forall), Stosując następującą równoważność:

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

Wierzę, że to się nazywa „skolemizacja”

Aby uzyskać więcej informacji, zobacz:

• Wikipedia - egzystencjalna kwantyfikacja

... a ta ostatnia sztuczka daje typ Dhalla:

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

... gdzie forall (Graph : Type)odgrywa taką samą rolę jak forall xw poprzedniej formule i forall (Node : Type)odgrywa taką samą rolę jak forall yw poprzedniej formule.