Да, вы можете смоделировать безопасный по типу направленный, возможно, циклический c граф в 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" ]
Это представление гарантирует отсутствие ломаных ребер.
Я также превратил этот ответ в пакет, который вы можете использовать:
Редактировать: Вот соответствующие ресурсы и дополнительные объяснения, которые могут помочь осветить происходящее:
Сначала начните со следующего Haskell типа для дерева :
data Tree a = Node { id :: a, neighbors :: [ Tree a ] }
Вы можете думать об этом типе как о ленивой и потенциально бесконечной структуре данных, представляющей то, что вы получили бы, если бы просто продолжали посещать соседей.
Теперь давайте представим, что вышеприведенное представление Tree на самом деле равно наших Graph, просто переименовав тип данных в Graph:
data Graph a = Node { id :: a, neighbors :: [ Graph a ] }
... но даже если мы хотим использовать этот тип, у нас нет способа напрямую смоделировать этот тип в Dhall, потому что язык Dhall не предоставляет встроенную поддержку для рекурсивного Та структуры. Так что же нам делать?
К счастью, на самом деле есть способ встроить рекурсивные структуры данных и рекурсивные функции в нерекурсивный язык, такой как Dhall. На самом деле, есть два способа!
- F-алгебры - Используется для реализации рекурсии
- F-коалгебры - Используется для реализации corecursion
Первое, что я прочитал и познакомил меня с этим трюком, было следующее черновое сообщение Wadler:
... но я могу суммировать основную идею c, используя следующие два типа 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 - рекурсивный список, реализованный без поддержки языка для recursion CoList - это список corecursive, реализованный без поддержки языка для corecursion
Оба эти типа эквивалентны ("isomorphi c to") [], что означает что:
- Вы можете конвертировать назад и вперед между
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 для Graph, особенно если мы заменим x на node:
data Graph a = forall node . MakeGraph node (node -> { id :: a, neighbors :: [ node ] })
Однако есть еще одна сложная часть, которая заключается в том, как перевести ExistentialQuantification из Haskell для Далла Оказывается, что вы всегда можете перевести экзистенциальную квантификацию в универсальную квантификацию (т.е. 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 в предыдущей формуле.