haskell - 如何静态检查图形有效性？

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)]’