Question

При использовании конечных автоматов в еж Я должен определить функцию, которая обновляет мое состояние модели.Его тип должен быть forall v. Ord1 v => state v -> input v -> Var output v -> state v (см. Update конструктор Callback).

Теперь я хочу получить output, но единственная функция, которую я нашелconcrete, однако он определяет v моей функции обновления.

Как определить функцию обновления, которая удовлетворяет типу для Update, и в то же время позволяет мне добраться довывод (предположительно с использованием concrete)?

K. A. Buhr · Answer 1 · 04 июня 2019

Ах, понятно. То, что вы хотите сделать, это использовать 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

Предположим, у нас есть следующий фиктивный веб-API с использованием глобальных IORefs:

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.

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

Теперь нам нужно смоделировать команды отправки, получения и удаления. Чтобы «опубликовать», нам понадобится следующий «ввод» (или переход, или что-то еще), который публикует данный контент:

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 переводит это действие в IO-действие на реальном API. Обратите внимание, что обратный вызов 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. В противном случае мы генерируем запрос Get для случайного UUID (в качестве символической переменной) в наборе. Это может быть UUID, который все еще находится в базе данных, или тот, который был удален. Затем метод execute выполняет действие ввода-вывода для фактического API. Здесь, наконец, мы можем сделать конкретную переменную (что нам нужно для фактического UUID для API).

Обратите внимание на обратные вызовы - мы Require считаем, что переменная UUID является членом набора переменных UUID в текущем состоянии (в случае, если это было недействительно во время сжатия), и после выполнения действия мы Ensure мы можем получить соответствующий контент для этого UUID. Обратите внимание, что нам разрешено делать переменные конкретными в Ensure, но в этом случае нам это не нужно. Update здесь не нужно, поскольку Get не влияет на состояние.

Нам также нужен экземпляр HTraversable для Get. Поскольку у него есть переменная, экземпляр немного сложнее:

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

Код для ввода «delete» и команды практически такой же, как и для «get», за исключением того, что у них есть обратный вызов 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 выходное значение (т. Е. Не 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)

Haskell, определите специализацию функции, которая полиморфна по типу

Пожалуйста, войдите или зарегистрируйтесь чтобы ответить на этот вопрос.

1 Ответ

Пожалуйста, войдите или зарегистрируйтесь что бы добавить комментарий.

Haskell, определите специализацию функции, которая полиморфна по типу

Пожалуйста, войдите или зарегистрируйтесь чтобы ответить на этот вопрос.

1 Ответ

Пожалуйста, войдите или зарегистрируйтесь что бы добавить комментарий.

Похожие темы