Haskell，定义类型多态的函数的特化

Question

在hedgehog 中使用状态机时，我必须定义一个函数来更新我的模型状态。它的类型应该是forall v. Ord1 v => state v -> input v -> Var output v -> state v（参见Callback的Update构造函数）。

现在，我想访问output，但我发现的唯一函数是concrete，但它指定了我的更新函数的v。

如何定义满足Update 类型的更新函数，同时仍让我获得输出（大概是通过使用concrete）？

Answer 1

啊，我明白了。您想要做的是在您的 Hedgehog 模型状态和输入（AKA 转换）中使用 Vars，只要状态组件依赖于早期操作。然后，您可以抽象地根据这些变量更新状态（即，以一种可以象征性和具体地工作的方式）。只有当您执行命令时，您才能使这些变量具体化。

让我给你看一个例子。我已经使用了以下导入和扩展，如果你想继续的话：

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RecordWildCards #-}
{-# OPTIONS_GHC -Wall #-}

import Control.Monad
import Control.Monad.IO.Class
import Data.IORef
import Data.Map.Strict as Map
import Data.Map.Strict (Map)
import Data.Set as Set
import Data.Set (Set)
import System.IO.Unsafe

import Hedgehog
import Hedgehog.Gen as Gen
import Hedgehog.Range as Range

假设我们有以下使用全局 IORefs 的模拟 Web API：

type UUID = Int
type Content = String

uuidRef :: IORef UUID
uuidRef = unsafePerformIO (newIORef 0)

newUuid :: IO UUID
newUuid = do
  n <- readIORef uuidRef
  writeIORef uuidRef (n+1)
  return n

dbRef :: IORef (Map UUID Content)
dbRef = unsafePerformIO (newIORef Map.empty)

resetDatabase :: IO ()
resetDatabase = writeIORef dbRef Map.empty

postFoo :: Content -> IO UUID
postFoo bdy = do
  uuid <- newUuid
  modifyIORef dbRef (Map.insert uuid bdy)
  return uuid

getFoo :: UUID -> IO (Maybe Content)
getFoo uuid = Map.lookup uuid <$> readIORef dbRef

deleteFoo :: UUID -> IO ()
deleteFoo uuid =
  modifyIORef dbRef (Map.delete uuid)

在构建 Hedgehog 模型时，我们需要记住 UUID 将由postFoo 操作生成作为输出，以用于后续（获取和删除）操作。后期操作对早期操作​​的这种依赖性意味着这些 UUID 应该在状态中显示为变量。

在我们的状态中，我们将跟踪 Map 的 UUID（作为变量）到 Content 以模拟数据库的内部状态。我们还将跟踪所有看到的 UUID 集合，甚至那些不再在数据库中的 UUID，因此我们可以测试已删除 UUID 的提取。

data ModelState (v :: * -> *)
  = S { uuids :: Set (Var UUID v)             -- UUIDs ever returned
      , content :: Map (Var UUID v) Content   -- active content
      }
  deriving (Eq, Ord, Show)

initialState :: ModelState v
initialState = S Set.empty Map.empty

现在，我们要对 post、get 和 delete 命令进行建模。要“发布”，我们需要以下“输入”（或转换，或其他），它发布给定的内容：

data Post (v :: * -> *) = Post Content
  deriving (Eq, Show)

对应的命令如下：

s_post :: (MonadGen n, MonadIO m, MonadTest m) => Command n m ModelState
s_post =
  let
    gen _state = Just $ Post <$> Gen.string (Range.constant 0 100) Gen.alpha
    execute (Post bdy) = liftIO $ postFoo bdy
  in
    Command gen execute [
        Update $ \S{..} (Post bdy) o -> S { uuids = Set.insert o uuids
                                          , content = Map.insert o bdy content }
      ]

请注意，无论当前状态如何，始终可以创建新帖子，因此gen 会忽略当前状态并生成随机帖子。 execute 将此操作转换为实际 API 上的 IO 操作。注意Update 回调接收postFoo 的结果作为变量。也就是说，o 将具有类型 Var UUID v。这很好，因为我们的Update 只需要在状态中存储一个Var UUID v——它不需要具体的UUID 值，因为我们构建ModelState 的方式。

我们还需要HTraversable 的Post 实例来进行类型检查。由于Post 没有任何变量，所以这个实例很简单：

instance HTraversable Post where
  htraverse _ (Post bdy) = pure (Post bdy)

对于“get”输入和命令，我们有：

data Get (v :: * -> *) = Get (Var UUID v)
  deriving (Eq, Show)

s_get :: (MonadGen n, MonadIO m, MonadTest m) => Command n m ModelState
s_get =
  let
    gen S{..} | not (Set.null uuids) = Just $ Get <$> Gen.element (Set.toList uuids)
              | otherwise            = Nothing
    execute (Get uuid) = liftIO $ getFoo $ concrete uuid
  in
    Command gen execute [
        Require $ \S{..} (Get uuid) -> uuid `Set.member` uuids
      , Ensure $ \before _after (Get uuid) o ->
          o === Map.lookup uuid (content before)
      ]

在这里，gen 查询当前状态以获取一组一直观察到的 UUID（技术上，作为符号变量）。如果集合为空，我们没有任何有效的 UUID 可供测试，因此不可能有Get，并且gen 返回Nothing。否则，我们会为集合中的随机 UUID（作为符号变量）生成一个 Get 请求。这可能是仍在数据库中的 UUID 或已被删除的 UUID。 execute 方法然后对实际 API 执行 IO 操作。最后，在这里，我们可以将变量具体化（我们需要为 API 获取一个实际的 UUID）。

注意回调——我们 Require 指出 UUID 变量是当前状态下 UUID 变量集的成员（以防它在收缩期间失效），并且在操作执行后，我们 Ensure我们可以检索此 UUID 的适当内容。请注意，我们可以在Ensure 中将变量具体化，但在这种情况下我们不需要这样做。这里不需要Update，因为Get 不会影响状态。

我们还需要HTraversable 的Get 实例。因为它有一个变量，所以实例稍微复杂一点：

instance HTraversable Get where
  htraverse f (Get uuid) = Get <$> htraverse f uuid

“删除”输入和命令的代码与“获取”的代码非常相似，只是它有一个Update 回调。

data Delete (v :: * -> *) = Delete (Var UUID v)
  deriving (Eq, Show)
instance HTraversable Delete where
  htraverse f (Delete uuid) = Delete <$> htraverse f uuid

s_delete :: (MonadGen n, MonadIO m, MonadTest m) => Command n m ModelState
s_delete =
  let
    gen S{..} | not (Set.null uuids) = Just $ Delete <$> Gen.element (Set.toList uuids)
              | otherwise            = Nothing
    execute (Delete uuid) = liftIO $ deleteFoo $ concrete uuid
  in
    Command gen execute [
        Require $ \S{..} (Delete uuid) -> uuid `Set.member` uuids
      , Update $ \S{..} (Delete uuid) _o -> S { content = Map.delete uuid content, .. }
      , Ensure $ \_before after (Delete uuid) _o ->
          Nothing === Map.lookup uuid (content after)
      ]

我们要测试的属性是这些操作的随机集合的顺序应用。请注意，由于我们的 API 具有全局状态，因此我们需要在每次测试开始时resetDatabase，否则事情会变得很奇怪：

prop_main :: Property
prop_main =
  property $ do
    liftIO $ resetDatabase
    actions <- forAll $
      Gen.sequential (Range.linear 1 100) initialState
          [ s_post, s_get, s_delete ]
    executeSequential initialState actions

最后，那么：

main :: IO ()
main = void (check prop_main)

运行它会给出：

> main
✓ <interactive> passed 100 tests.
>

请注意，我们在上面忘记检查一件事，即 API 在发布时确实提供了唯一的 UUID。例如，如果我们故意破坏我们的 UUID 生成器：

newUuid :: IO UUID
newUuid = do
  n <- readIORef uuidRef
  writeIORef uuidRef $ (n+1) `mod` 2
  return n

测试仍然通过 - API 为我们提供了重复的 UUID，我们尽职尽责地覆盖了模型状态中的旧数据，以匹配损坏的 API。

为了检查这一点，我们想向s_post 添加一个Ensure 回调，以确保每个新的UUID 都不是我们以前见过的。但是，如果我们写：

, Ensure $ \before _after (Post _bdy) o ->
    assert $ o `Set.notMember` uuids before

这不会进行类型检查，因为o 是一个实际的、具体的UUID 输出值（即，不是Var），但uuids before 是一组具体变量。我们可以映射集合以从变量中提取具体值：

, Ensure $ \before _after (Post _bdy) o ->
    assert $ o `Set.notMember` Set.map concrete (uuids before)

或者，我们可以为值o 构造一个具体变量，如下所示：

, Ensure $ \before _after (Post _bdy) o ->
    assert $ Var (Concrete o) `Set.notMember` uuids before

两者都可以正常工作并捕获上面的错误 newUuid 实现。

供参考，完整代码为：

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RecordWildCards #-}
{-# OPTIONS_GHC -Wall #-}

import Control.Monad
import Control.Monad.IO.Class
import Data.IORef
import Data.Map.Strict as Map
import Data.Map.Strict (Map)
import Data.Set as Set
import Data.Set (Set)
import System.IO.Unsafe

import Hedgehog
import Hedgehog.Gen as Gen
import Hedgehog.Range as Range

-- * Mock API

type UUID = Int
type Content = String

uuidRef :: IORef UUID
uuidRef = unsafePerformIO (newIORef 0)

newUuid :: IO UUID
newUuid = do
  n <- readIORef uuidRef
  writeIORef uuidRef $ (n+1)
  return n

dbRef :: IORef (Map UUID Content)
dbRef = unsafePerformIO (newIORef Map.empty)

resetDatabase :: IO ()
resetDatabase = writeIORef dbRef Map.empty

postFoo :: Content -> IO UUID
postFoo bdy = do
  uuid <- newUuid
  modifyIORef dbRef (Map.insert uuid bdy)
  return uuid

getFoo :: UUID -> IO (Maybe Content)
getFoo uuid = Map.lookup uuid <$> readIORef dbRef

deleteFoo :: UUID -> IO ()
deleteFoo uuid =
  modifyIORef dbRef (Map.delete uuid)

-- * Hedgehog model state

data ModelState (v :: * -> *)
  = S { uuids :: Set (Var UUID v)             -- UUIDs ever returned
      , content :: Map (Var UUID v) Content   -- active content
      }
  deriving (Eq, Ord, Show)

initialState :: ModelState v
initialState = S Set.empty Map.empty

-- * Post input/command

data Post (v :: * -> *) = Post Content
  deriving (Eq, Show)
instance HTraversable Post where
  htraverse _ (Post bdy) = pure (Post bdy)

s_post :: (MonadGen n, MonadIO m, MonadTest m) => Command n m ModelState
s_post =
  let
    gen _state = Just $ Post <$> Gen.string (Range.constant 0 100) Gen.alpha
    execute (Post bdy) = liftIO $ postFoo bdy
  in
    Command gen execute [
        Update $ \S{..} (Post bdy) o -> S { uuids = Set.insert o uuids
                                          , content = Map.insert o bdy content }
    , Ensure $ \before _after (Post _bdy) o ->
        assert $ Var (Concrete o) `Set.notMember` uuids before
      ]

-- * Get input/command

data Get (v :: * -> *) = Get (Var UUID v)
  deriving (Eq, Show)
instance HTraversable Get where
  htraverse f (Get uuid) = Get <$> htraverse f uuid

s_get :: (MonadGen n, MonadIO m, MonadTest m) => Command n m ModelState
s_get =
  let
    gen S{..} | not (Set.null uuids) = Just $ Get <$> Gen.element (Set.toList uuids)
              | otherwise            = Nothing
    execute (Get uuid) = liftIO $ getFoo $ concrete uuid
  in
    Command gen execute [
        Require $ \S{..} (Get uuid) -> uuid `Set.member` uuids
      , Ensure $ \before _after (Get uuid) o ->
          o === Map.lookup uuid (content before)
      ]

-- * Delete input/command

data Delete (v :: * -> *) = Delete (Var UUID v)
  deriving (Eq, Show)
instance HTraversable Delete where
  htraverse f (Delete uuid) = Delete <$> htraverse f uuid

s_delete :: (MonadGen n, MonadIO m, MonadTest m) => Command n m ModelState
s_delete =
  let
    gen S{..} | not (Set.null uuids) = Just $ Delete <$> Gen.element (Set.toList uuids)
              | otherwise            = Nothing
    execute (Delete uuid) = liftIO $ deleteFoo $ concrete uuid
  in
    Command gen execute [
        Require $ \S{..} (Delete uuid) -> uuid `Set.member` uuids
      , Update $ \S{..} (Delete uuid) _o -> S { content = Map.delete uuid content, .. }
      , Ensure $ \_before after (Delete uuid) _o ->
          Nothing === Map.lookup uuid (content after)
      ]

-- * Run the tests

prop_main :: Property
prop_main =
  property $ do
    liftIO $ resetDatabase
    actions <- forAll $
      Gen.sequential (Range.linear 1 100) initialState
          [ s_post, s_get, s_delete ]
    executeSequential initialState actions

main :: IO ()
main = void (check prop_main)