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

Question

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

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

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

Answer 1

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

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

{-# 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 应该在状态中显示为变量。

在我们的状态中，我们将跟踪MapUUID（作为变量）来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将有 type Var UUID v。这很好，因为我们Update只需要Var UUID v在状态中存储 a ——它不需要具体的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 来测试，所以 noGet是可能的，并gen返回Nothing。否则，我们Get会在集合中生成一个随机 UUID（作为符号变量）的请求。这可能是仍在数据库中的 UUID 或已被删除的 UUID。然后该execute方法对实际 API 执行 IO 操作。最后，在这里，我们可以将变量具体化（我们需要UUID为 API 获取一个实际的变量）。

注意回调——我们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 相匹配。

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

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

这不会进行类型检查，因为o它是一个实际的、具体的UUID输出值（即，不是 a 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)