Dhall에서 위키 (직접 그래프를 포함하는 문서 세트)를 나타내고 싶습니다. 이 문서는 HTML로 렌더링되며 깨진 링크가 생성되는 것을 막고 싶습니다. 내가 본 것처럼 이것은 유형 시스템을 통해 유효하지 않은 그래프 (존재하지 않는 노드에 대한 링크가있는 그래프)를 표현할 수 없게 만들거나 가능한 그래프에서 오류 목록을 반환하는 함수를 작성하여 수행 할 수 있습니다 (예 : “가능한 그래프에서) X, 노드 A는 존재하지 않는 노드 B에 대한 링크를 포함합니다 “).
순진한 인접 목록 표현은 다음과 같습니다.
let Node : Type = {
id: Text,
neighbors: List Text
}
let Graph : Type = List Node
let example : Graph = [
{ id = "a", neighbors = ["b"] }
]
in example
이 예에서 알 수 있듯이이 유형은 유효한 그래프에 해당하지 않는 값을 허용합니다 (ID가 “b”인 노드는 없지만 ID가 “a”인 노드는 ID가 “b”인 이웃을 지정 함). 또한 Dhall은 설계에 따라 문자열 비교를 지원하지 않기 때문에 각 노드의 이웃을 접어 이러한 문제 목록을 생성 할 수 없습니다.
끊어진 링크 목록을 계산하거나 유형 시스템을 통한 끊어진 링크를 제외 할 수있는 표현이 있습니까?
업데이트 : 방금 Naturals가 Dhall에서 비교할 수 있음을 발견했습니다. 따라서 식별자가 Naturals 인 경우 유효하지 않은 모서리 ( “깨진 링크”)를 식별하고 식별자의 중복 사용을 식별하기 위해 함수를 작성할 수 있다고 가정합니다.
그래도 그래프 유형을 정의 할 수 있는지에 대한 최초의 질문은 남아 있습니다.
답변
예, 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-coalgebras- “코 어커런스”구현에 사용
내가이 트릭을 처음 소개 한 것은 Wadler의 다음 초안이었다.
…하지만 다음 두 가지 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작업 방식은 원하는 재귀 또는 “핵심”유형의 “하나의 계층”(예 🙂 f을 제공 한 다음 재귀 또는 코어 큐 레이션에 대한 언어 지원 없이도 원하는 유형만큼 강력한 것을 제공하는 것입니다. .
리스트를 예로 들어 봅시다. 다음 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)를 사용 한다는 것입니다. 이 매개 변수 는 유형의 모든 재귀 적 / 핵심 적 발생에 대한 자리 표시 자로 사용합니다.
ListF이제을 갖추고 다음과 같이 재귀 및 핵심 재귀 목록을 정의 할 수 있습니다.
type List a = LFix (ListF a)
type CoList a = GFix (ListF a)
… 어디:
List재귀에 대한 언어 지원없이 구현 된 재귀 목록입니다.CoListcorecursion에 대한 언어 지원없이 구현 된 corecursive 목록입니다.
이 두 유형은 모두 ( “isomorphic 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 ] })
지금은 대한에게 달 유형처럼 보이기 시작한다 Graph우리가 대체 특히, x함께 node:
data Graph a = forall node . MakeGraph node (node -> { id :: a, neighbors :: [ node ] })
그러나 여전히 마지막으로 까다로운 부분이 있습니다. 이는 ExistentialQuantificationHaskell에서 Dhall 로 변환하는 방법 입니다. forall다음 동등성을 사용하여 실존 적 정량화를 범용 정량화 (즉, ) 로 항상 변환 할 수 있습니다 .
exists y . f y ≅ forall x . (forall y . f y -> x) -> x
이것이 “skolemization”이라고 믿습니다
자세한 내용은 다음을 참조하십시오.
… 그리고 그 마지막 트릭은 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합니다.
