Как статически проверить достоверность графика?

Question

Рассмотрим приведенный ниже код.

newtype NodeAT = NodeAT String deriving (Show,Read,Eq,Ord)
newtype NodeBT = NodeBT String deriving (Show,Read,Eq,Ord)
newtype NodeCT = NodeCT String deriving (Show,Read,Eq,Ord)
newtype NodeDT = NodeDT String deriving (Show,Read,Eq,Ord)

nodeA = NodeAT "nodeA" 
nodeB = NodeBT "nodeB"
nodeC = NodeCT "nodeC"
nodeD = NodeDT "nodeD"


data Graph n m = Graph
 { vertices :: n
  , edges :: m
 }

graph1 = Graph  (nodeA,nodeB,nodeC,nodeD)  ((nodeA,nodeC),(nodeB,nodeC),(nodeA, nodeC))

Есть ли возможность использовать систему типов для проверки того, что пары ребер являются экземплярами узлов, принадлежащих кортежу вершин? Это сделало бы конструкцией

graph2 = Graph (nodeA, nodeB) (nodeA, nodeC)

недопустимой и потерпевшей неудачу во время компиляции?

Answer 1

Не уверен, что он соответствует вашим потребностям, но вы можете пройти долгий путь с небольшим количеством программирования на уровне типов.

Конечно, необходимы некоторые расширения:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

Здесь является семейством закрытых типов для проверки того, является ли тип членом списка типов на уровне типов:

type family Elem a as :: Bool where
  Elem a '[] = False
  Elem a (a : as) = True
  Elem a (b : as) = Elem a as

Теперь давайте определим типы вершин и ребер, в которых вершины выводятся из заданного списка вершин. типы:

data Vertex :: [*] -> * where
  V :: Elem a as ~ True => a -> Vertex as

type Edge as = (Vertex as, Vertex as)

Затем мы можем определить тип графиков, в которых вершины хранятся в своем типе, а его ребра - в конструкторе данных:

data Graph :: [*] -> * where
  G :: [Edge as] -> Graph as

Вот некоторые типы вершин :

data NodeA = NodeA
data NodeB = NodeB
data NodeC = NodeC

При этом хорошо набирается следующий график:

graph1 :: Graph [NodeA, NodeB]
graph1 = G [(V NodeA, V NodeB)]

Но нет:

graph2 :: Graph [NodeA, NodeB]
graph2 = G [(V NodeA, V NodeC)]

Сбой при:

  error:
    • Couldn't match type ‘'False’ with ‘'True’
        arising from a use of ‘V’
    • In the expression: V NodeC
      In the expression: (V NodeA, V NodeC)
      In the first argument of ‘G’, namely ‘[(V NodeA, V NodeC)]’