Тип-безопасный поток (машина состояния)

Я пытаюсь создать в Haskell безопасный вопрос-ответный поток. Я моделирую QnA как ориентированный граф, похожий на FSM.

Каждый node на графике представляет вопрос:

data Node s a s' = Node {
  question :: Question a,
  process :: s -> a -> s'
}

s - это входное состояние, a - ответ на вопрос, а s' - состояние вывода. Узлы зависят от входного состояния s, что означает, что для обработки ответа мы должны быть в определенном состоянии раньше.

Question a представляют собой простой вопрос/ответ, создающий ответ типа a.

В качестве типа я имею в виду, например, для node Node2 :: si -> a -> s2, если si зависит от s1, тогда все пути, заканчивающиеся на Node2, должны проходить через node, который производит s1 сначала. (Если s1 == si, то все предшественники Node2 должны создавать s1).

Пример

QnA: на веб-сайте онлайн-покупок нам нужно задать размер тела пользователя и любимый цвет.

  • e1: спросите пользователя, знают ли они их размер. Если да, перейдите к e2 в противном случае перейдите к e3
  • e2: спросите размер пользователя и перейдите к ef, чтобы задать цвет.
  • e3: (пользователь не знает их размер), задайте вес пользователя и перейдите к e4.
  • e4: (после e3) задайте высоту пользователя и вычислите их размер и перейдите к ef.
  • ef: спросите пользовательский цвет и закончите поток с результатом Final.

В моей модели Edge соедините Node друг с другом:

data Edge s sf where
  Edge  :: EdgeId -> Node s a s' -> (s' -> a -> Edge s' sf) -> Edge s sf
  Final :: EdgeId -> Node s a s' -> (s' -> a -> sf) -> Edge s sf

sf является конечным результатом QnA, который здесь: (Bool, Size, Color).

Состояние QnA в каждый момент может быть представлено кортежем: (s, EdgeId). Это состояние сериализуемо, и мы должны иметь возможность продолжить QnA, просто зная это состояние.

saveState :: (Show s) => (s, Edge s sf) -> String
saveState (s, Edge eid n _) = show (s, eid)

getEdge :: EdgeId -> Edge s sf
getEdge = undefined --TODO

respond :: s -> Edge s sf -> Input -> Either sf (s', Edge s' sf)
respond s (Edge ...) input = Right (s', Edge ...)
respond s (Final ...) input = Left s' -- Final state

-- state = serialized (s, EdgeId)
-- input = user answer to the current question
main' :: String -> Input -> Either sf (s', Edge s' sf)
main' state input =
  let (s, eid) = read state :: ((), EdgeId) --TODO
      edge = getEdge eid
  in respond s input edge

Поток для определения размера платья пользователя

Полный код:

{-# LANGUAGE GADTs, RankNTypes, TupleSections #-}

type Input = String
type Prompt = String
type Color = String
type Size = Int
type Weight = Int
type Height = Int

data Question a = Question {
  prompt :: Prompt,
  answer :: Input -> a
}

-- some questions 
doYouKnowYourSizeQ :: Question Bool
doYouKnowYourSizeQ = Question "Do you know your size?" read

whatIsYourSizeQ :: Question Size
whatIsYourSizeQ = Question "What is your size?" read

whatIsYourWeightQ :: Question Weight
whatIsYourWeightQ = Question "What is your weight?" read

whatIsYourHeightQ :: Question Height
whatIsYourHeightQ = Question "What is your height?" read

whatIsYourFavColorQ :: Question Color
whatIsYourFavColorQ = Question "What is your fav color?" id

-- Node and Edge

data Node s a s' = Node {
  question :: Question a,
  process :: s -> a -> s'
}

data Edge s sf where
  Edge  :: EdgeId -> Node s a s' -> (s' -> a -> Edge s' sf) -> Edge s sf
  Final :: EdgeId -> Node s a s' -> (s' -> a -> sf) -> Edge s sf

data EdgeId = E1 | E2 | E3 | E4 | Ef deriving (Read, Show)

-- nodes

n1 :: Node () Bool Bool
n1 = Node doYouKnowYourSizeQ (const id)

n2 :: Node Bool Size (Bool, Size)
n2 = Node whatIsYourSizeQ (,)

n3 :: Node Bool Weight (Bool, Weight)
n3 = Node whatIsYourWeightQ (,)

n4 :: Node (Bool, Weight) Height (Bool, Size)
n4 = Node whatIsYourHeightQ (\ (b, w) h -> (b, w * h))

n5 :: Node (Bool, Size) Color (Bool, Size, Color)
n5 = Node whatIsYourFavColorQ (\ (b, i) c -> (b, i, c))


-- type-safe edges

e1 = Edge E1 n1 (const $ \ b -> if b then e2 else e3)
e2 = Edge E2 n2 (const $ const ef)
e3 = Edge E3 n3 (const $ const e4)
e4 = Edge E4 n4 (const $ const ef)
ef = Final Ef n5 const


ask :: Edge s sf -> Prompt
ask (Edge _ n _) = prompt $ question n
ask (Final _ n _) = prompt $ question n

respond :: s -> Edge s sf -> Input -> Either sf (s', Edge s' sf)
respond s (Edge _ n f) i =
  let a  = (answer $ question n) i
      s' = process n s a
      n' = f s' a
  in Right undefined --TODO n'

respond s (Final _ n f) i =
  let a  = (answer $ question n) i
      s' = process n s a
  in Left undefined --TODO s'


-- User Interaction:

saveState :: (Show s) => (s, Edge s sf) -> String
saveState (s, Edge eid n _) = show (s, eid)

getEdge :: EdgeId -> Edge s sf
getEdge = undefined --TODO

-- state = serialized (s, EdgeId) (where getEdge :: EdgeId -> Edge s sf)
-- input = user answer to the current question
main' :: String -> Input -> Either sf (s', Edge s' sf)
main' state input =
  let (s, eid) = undefined -- read state --TODO
      edge = getEdge eid
  in respond s edge input

Для меня важно, чтобы края были безопасными для типов. Значение, например, некорректная привязка e2 к e3 должна быть ошибкой типа: e2 = Edge E2 n2 (const $ const ef) в порядке e2 = Edge E2 n2 (const $ const e3) должна быть ошибкой.

Я задал свои вопросы с помощью --TOOD:

  • Учитывая мои критерии сохранения типов с типом, Edge s sf должен иметь переменную типа ввода (s), то как я могу создать функцию getEdge :: EdgeId -> Edge s sf?

  • Как создать функцию respond, которая задала текущее состояние s и текущий край Edge s sf, вернет либо конечное состояние (если текущее ребро Final), либо следующее состояние и следующий край (s', Edge s' sf)?

Мой дизайн Node s a s' и Edge s sf может быть просто неправильным. Я не должен придерживаться этого.

Ответы

Ответ 1

Чтобы объяснить простой пример, я покажу вам решение, которое не имеет естественной поддержки для приостановки, сохранения и возобновления вычислений. В конце я расскажу вам о том, как добавить это, надеюсь, вы сможете сами выяснить его.

Здесь так называемая монадированная статусная монада:

newtype IStateT m i o a = IStateT { runIState :: i -> m (o, a) }

IStateT похож на обычный государственный монадный трансформатор, за исключением того, что тип неявного состояния разрешается изменять на протяжении всего процесса вычисления. Действия секвенирования в монадии с индексированным состоянием требуют, чтобы состояние вывода одного действия соответствовало состоянию ввода следующего. Такой тип доминоподобного секвенирования - это Адаптированная монада монады (или индексированная монада) для.

class IMonad m where
    ireturn :: a -> m i i a
    (>>>=) :: m i j a -> (a -> m j k b) -> m i k b

(>>>) :: IMonad m => m i j a -> m j k b -> m i k b
mx >>> my = mx >>>= \_ -> my

IMonad - это класс монад-подобных вещей, которые описывают путь через индексированный граф. Тип (>>>=) говорит: "Если у вас есть вычисление, которое идет от i до j и вычисление от j до k, я могу присоединиться к ним, чтобы дать вам вычисление от i до k".

Нам также нужно будет поднять вычисления из классических монад в индексированные монады:

class IMonadTrans t where
    ilift :: Monad m => m a -> t m i i a

Обратите внимание, что код для IStateT такой же, как и код обычной монады состояния - это только те типы, которые получили умнее.

iget :: Monad m => IStateT m s s s
iget = IStateT $ \s -> return (s, s)

iput :: Monad m => o -> IStateT m i o ()
iput x = IStateT $ \_ -> return (x, ())

imodify :: Monad m => (i -> o) -> IStateT m i o ()
imodify f = IStateT $ \s -> return (f s, ())

instance Monad m => IMonad (IStateT m) where
    ireturn x = IStateT (\s -> return (s, x))
    IStateT f >>>= g = IStateT $ \s -> do
                                    (s', x) <- f s
                                    let IStateT h = g x
                                    h s'
instance IMonadTrans IStateT where
    ilift m = IStateT $ \s -> m >>= \x -> return (s, x)

Идея состоит в том, что монадические действия, такие как askSize и askWeight (ниже), добавят некоторые данные в неявную среду, увеличивая ее тип. Поэтому я собираюсь построить неявную среду из вложенных кортежей, рассматривая их как списки типов типов. Вложенные кортежи более гибкие (хотя и менее эффективные), чем плоские кортежи, потому что они позволяют вам абстрагироваться по хвосту списка. Это позволяет создавать кортежи произвольного размера.

type StateMachine = IStateT IO

newtype Size = Size Int
newtype Height = Height Int
newtype Weight = Weight Int
newtype Colour = Colour String

-- askSize takes an environment of type as and adds a Size element
askSize :: StateMachine as (Size, as) ()
askSize = askNumber "What is your size?" Size

-- askHeight takes an environment of type as and adds a Height element
askHeight :: StateMachine as (Height, as) ()
askHeight = askNumber "What is your height?" Height

-- etc
askWeight :: StateMachine as (Weight, as) ()
askWeight = askNumber "What is your weight?" Weight

askColour :: StateMachine as (Colour, as) ()
askColour =
    -- poor man do-notation. You could use RebindableSyntax
    ilift (putStrLn "What is your favourite colour?") >>>
    ilift readLn                                      >>>= \answer ->
    imodify (Colour answer,)

calculateSize :: Height -> Weight -> Size
calculateSize (Height h) (Weight w) = Size (h - w)  -- or whatever the calculation is

askNumber :: String -> (Int -> a) -> StateMachine as (a, as) ()
askNumber question mk =
    ilift (putStrLn question) >>>
    ilift readLn              >>>= \answer ->
    case reads answer of
        [(x, _)] -> imodify (mk x,)
        _ -> ilift (putStrLn "Please type a number") >>> askNumber question mk

askYN :: String -> StateMachine as as Bool
askYN question =
    ilift (putStrLn question) >>>
    ilift readLn              >>>= \answer ->
    case answer of
        "y" -> ireturn True
        "n" -> ireturn False
        _ -> ilift (putStrLn "Please type y or n") >>> askYN question

Моя реализация немного отличается от вашей спецификации. Вы говорите, что невозможно спросить размер пользователя, а затем попросить их вес. Я говорю, что это должно быть возможно - результат просто не обязательно будет иметь тот тип, который вам нужен (потому что вы добавили две вещи в среду, а не в одну). Это полезно здесь, где askOrCalculateSize - это просто черный ящик, который добавляет Size (и ничего больше) в среду. Иногда он делает это, запрашивая размер напрямую; иногда он вычисляет его, сначала запрашивая высоту и вес. Это не имеет значения в отношении проверки типов.

interaction :: StateMachine xs (Colour, (Size, xs)) ()
interaction =
    askYN "Do you know your size?" >>>= \answer ->
    askOrCalculateSize answer >>>
    askColour

    where askOrCalculateSize True = askSize
          askOrCalculateSize False =
            askWeight >>>
            askHeight >>>
            imodify (\(h, (w, xs)) -> ((calculateSize h w), xs))

Остается вопрос: как можно возобновить вычисление из постоянного состояния? Вы не статически знаете тип среды ввода (хотя безопасно считать, что вывод всегда (Colour, Size)), потому что он изменяется во всех вычислениях, и вы не знаете, пока не загрузите состояние, в котором оно было до.

Трюк состоит в том, чтобы использовать немного доказательств GADT, которые вы можете сопоставить с шаблонами, чтобы узнать, что это за тип. Stage представляет, где вы могли бы вступить в процесс, и индексируется по типу, который среда должна иметь на этом этапе. Suspended соединяет a Stage с фактическими данными, находящимися в среде в момент приостановки вычисления.

data Stage as where
    AskSize :: Stage as
    AskWeight :: Stage as
    AskHeight :: Stage (Weight, as)
    AskColour :: Stage (Size, as)

data Suspended where
    Suspended :: Stage as -> as -> Suspended

resume :: Suspended -> StateMachine as (Colour, (Size, as)) ()
resume (Suspended AskSize e) =
    iput e                                               >>>
    askSize                                              >>>
    askColour
resume (Suspended AskWeight e) =
    iput e                                               >>>
    askWeight                                            >>>
    askHeight                                            >>>
    imodify (\(h, (w, xs)) -> ((calculateSize h w), xs)) >>>
    askColour
resume (Suspended AskHeight e) =
    iput e                                               >>>
    askHeight                                            >>>
    imodify (\(h, (w, xs)) -> ((calculateSize h w), xs)) >>>
    askColour
resume (Suspended AskColour e) =
    iput e                                               >>>
    askColour

Теперь вы можете добавить точки подвески к вычислению:

-- given persist :: Suspended -> IO ()
suspend :: Stage as -> StateMachine as as ()
suspend stage =
    iget                                  >>>= \env
    ilift (persist (Suspended stage env))

resume работает, но он довольно уродлив и имеет много дублирования кода. Это связано с тем, что после того, как вы собрали государственную монаду, вы не сможете разобрать ее снова, чтобы заглянуть внутрь нее. Вы не можете прыгать в заданной точке вычисления. Это большое преимущество вашего оригинального дизайна, в котором вы представляли конечный автомат как структуру данных, которую можно запросить, чтобы выяснить, как возобновить вычисление. Это называется начальной кодировкой, тогда как мой пример (представляющий конечный автомат как функцию) является окончательной кодировкой. Окончательные кодировки просты, но начальные кодировки являются гибкими. Надеюсь, вы можете увидеть, как адаптировать первоначальный подход к индексированному дизайну монады.