确保数据的正确性

Question

我已经在 Haskell 编程几个月了，我真的很享受。我觉得我对 monad、函子、纯度等有很好的掌握。既然我一直在使用这个很好的类型系统，那么表达不正确的东西的想法对我来说听起来很可怕。 Haskell 允许您有时通过将数据的属性移动到类型系统中来解决这个问题。例如，使用 GADT，您可以定义不能以不平衡方式构建的平衡树：

因此，您保证在树上实现的任何函数都将生成正确的树。但在其他情况下，我看不出如何在类型级别约束数据。

下面是我具体考虑的情况。我想表示一个图，其中每个边都指向一个存在的节点。因此，例如，如果仅存在节点 1-4，则您不能定义通往节点 5 的边。我知道 DAG 样式图有这样的东西，但没有看到有周期的图有这样的东西。我将如何去表达这样的东西？

Answer 1

通常将（小）有向图表示为邻接矩阵。如果您创建一个 Bool 的 n*n 矩阵，您可以准确地表示所有具有 n 个节点的图。当然你需要一个好的矩阵库来表示这个（不是 [[Bool]]，它可以有无效的值），最好是用类型级数字编码大小的东西，这样你就可以要求它们是正方形的。

一个小例子来说明这一点：

Matrix.hs:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Matrix (Matrix, fromLists, toLists, Proxy(..)) where

import GHC.TypeLits

-- Yeah, I just said "don't use [[Bool]]"
-- But the Matrix constructor is not exported, the only way
-- users of this API can construct matrices is by using the
-- fromLists function, which only accepts [[a]] when the size
-- matches the expected matrix.
-- It's a bad choice for memory-consumption, but keeps the
-- example simple.
data Matrix (n :: Nat) (m :: Nat) a = Matrix [[a]]
    deriving (Show)

-- We use these proxies so we can pass the type-level numbers
-- as arguments.
data Proxy (a :: k) = Proxy

fromLists :: (KnownNat n, KnownNat m)
          => Proxy n
          -> Proxy m
          -> [[a]]
          -> Maybe (Matrix n m a)
fromLists proxyN proxyM lists
    -- "Downgrade" the type-level numbers to value level integers
    -- and verify that the input is sound.
    | fromIntegral (length lists) == natVal proxyN
    , all (\list -> fromIntegral (length list) == natVal proxyM) lists
    = Just (Matrix lists)
fromLists _ _ _
    = Nothing

toLists :: Matrix n m a -> [[a]]
toLists (Matrix lists) = lists

Graph.hs:

{-# LANGUAGE DataKinds #-}

import Matrix
import GHC.TypeLits

-- Represents a graph with n vertices.
type Graph n = Matrix n n Bool

-- Turns a graph back into an adjacency list.
toEdgeList :: (KnownNat n) => Graph n -> [(Integer, [Integer])]
toEdgeList graph
    = let
        adjecency = toLists graph
      in zipWith (\i row -> (i, map fst $ filter snd $ zip [0..] row)) [0..] adjecency

main = do
    case fromLists (Proxy :: Proxy 4) (Proxy :: Proxy 4)
        [ [True,  False, False, True ]
        , [False, True,  False, False]
        , [False, False, False, False]
        , [True,  True,  True,  True ]
        ] of
        (Just graph) -> print (toEdgeList graph)

结果：

[(0,[0,3]),(1,[1]),(2,[]),(3,[0,1,2,3])]

这种方法并没有使无效图无法表示，它只是通过隐藏 Matrix 构造函数并仅将 fromLists 公开为 "smart constructor" 使它们无法构造。只要从 Matrix.hs 导出的所有函数都保持不变量，这是安全的。

当图很大但很稀疏并且不可能在内存中构造整个邻接矩阵时，您可以退回到邻接表。我们可以使用相同的类型级技巧来创建可以在这里使用的有界自然数：

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
import GHC.TypeLits

data BoundedInteger (n :: Nat) = BoundedInteger Integer

instance Show (BoundedInteger n) where
    show (BoundedInteger i) = show i

data Proxy (n :: k) = Proxy

boundedFromInteger :: (KnownNat n) => Proxy n -> Integer -> Maybe (BoundedInteger n)
boundedFromInteger proxy n
    | 0 <= n
    , n <= natVal proxy
    = Just (BoundedInteger n)
boundedFromInteger _ _ = Nothing

同样，只有智能构造函数 boundedFromInteger 被导出，而不是 BoundedInteger。有了这个，我们可以定义一个图：

type Graph n = Map (BoundedInteger n) (Set (BoundedInteger n))

Answer 2

如果您不编号您的节点，而是通过一些合适的有限（或可能是无限！）类型完全索引它们，则可以很好地完成此操作。要在这样的图中存储每个节点的数据，您可以使用类似 memotries.

的东西

newtype GraphNodes i d = GraphNodes { getGraphNodes :: i :->: d }

那么，有向边的类型就是一个元组(i,i)。因为节点集合恰好是i中所有可能值的集合，所以保证在图中。

这种类型的完整图的有效存储只是 Map 从节点到节点：

newtype GraphEdges i = GraphEdges { getGraphEdges :: Map.Map i i }

确保数据的正确性

Ensuring correctness of data

haskell

graph

types

gadt