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

Question

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

Каждый узел в графе представляют собой вопрос:

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

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

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

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

Пример

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

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

В моей модели, Edge s подключить Node 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 

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's 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's 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 может быть просто неправильно. Я не должен придерживаться этого.

Answer 1

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

---

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

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

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

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