Question Flux de type sécurisé (State Machine)


J'essaie de créer un flux de questions-réponses sûr dans Haskell. Je modélise QnA comme un graphe orienté, similaire à un FSM.

Chaque nœud du graphique représente une question:

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

s est l'état d'entrée, a est la réponse à la question et s' est l'état de sortie. Les nœuds dépendent de l'état d'entrée s, ce qui signifie que pour traiter la réponse, nous devons être dans un état particulier avant.

Question a représenter une simple question / réponse produisant une réponse de type a.

Par type-safe, je veux dire par exemple avec un nœud Node2 :: si -> a -> s2, si si dépend de s1 alors tous les chemins se terminant par Node2 doit passer par un nœud qui produit s1 premier. (Si s1 == si alors tous les prédécesseurs de Node2  doit produire s1).

Un exemple

QnA: Dans un site de vente en ligne, nous devons demander à l'utilisateur la taille de son corps et sa couleur préférée.

  1. e1: demandez à l'utilisateur s'il connaît sa taille. Si oui, alors allez à e2 sinon aller à e3
  2. e2: demander à l'utilisateur la taille et aller à ef demander la couleur.
  3. e3: (l'utilisateur ne sait pas leur taille), demander le poids de l'utilisateur et aller à e4.
  4. e4: (après e3) demander à l'utilisateur la taille et calculer sa taille et aller à ef.
  5. ef: demander à la couleur préférée de l'utilisateur et terminer le flux avec le Final résultat.

Dans mon modèle, Edges connect Nodes les uns aux autres:

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 est le résultat final du QnA, à savoir: (Bool, Size, Color).

L'état QnA à chaque instant peut être représenté par un tuple: (s, EdgeId). Cet état est sérialisable et nous devrions pouvoir continuer un QnA simplement en connaissant cet état.

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

Flow for determining user's dress size

Code complet:

{-# 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

Il est important pour moi de garder les bords sûrs. Ce qui signifie par exemple un lien incorrect e2 à e3 doit être une erreur de type: e2 = Edge E2 n2 (const $ const ef) est bien par e2 = Edge E2 n2 (const $ const e3) doit être une erreur.

J'ai indiqué mes questions avec --TOOD:

  • Compte tenu de mes critères de protection des arêtes, Edge s sf doit avoir une variable de type d'entrée (s) alors comment puis-je créer getEdge :: EdgeId -> Edge s sf fonction?

  • Comment puis-je créer le respond fonction qui compte tenu de l'état actuel s et bord actuel Edge s sf, retournera soit l'état final (si le bord actuel est Final) ou le prochain état et le prochain bord (s', Edge s' sf)?

Mon design de Node s a s' et Edge s sf pourrait être simplement faux. Je n'ai pas à m'en tenir à cela.


13
2017-09-05 10:03


origine


Réponses:


Pour avoir un exemple simple à expliquer, je vais vous montrer une solution qui n'a pas de support naturel pour suspendre, persister et reprendre des calculs. À la fin, je vous donnerai l'essentiel de la manière d'ajouter cela - j'espère que vous serez en mesure de comprendre les détails concrets de votre travail.


Voici le soi-disant état indexé monade:

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

IStateT est comme un transformateur monad d'état normal, sauf que le type de l'état implicite est autorisé à changer au cours d'un calcul. Les actions de séquençage dans la monade d'état indexée nécessitent que l'état de sortie d'une action corresponde à l'état d'entrée de la suivante. Ce genre de séquençage de type domino est ce que Atkey monade paramétrée (ou monade indexée) est pour.

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 est la classe des choses de type monade qui décrivent un chemin à travers un graphique indexé. Le type de (>>>=) dit "Si vous avez un calcul qui va de i à j et un calcul de j à k, Je peux les joindre pour vous faire un calcul i à k".

Nous devrons également lever les calculs des monades classiques en monades indexées:

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

Notez que le code pour IStateT est le même que le code pour le monad normal - ce ne sont que les types qui sont plus intelligents.

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)

L'idée est que les actions monadiques aiment askSize et askWeight (ci-dessous) ajouter des données à l'environnement implicite, en développant son type. Je vais donc construire l'environnement implicite à partir de n-uplets imbriqués, en les traitant comme des listes de types au niveau du type. Les n-uples imbriqués sont plus flexibles (mais moins efficaces) que les n-uplets plats, car ils vous permettent de faire un résumé sur la fin de la liste. Cela vous permet de construire des tuples de taille arbitraire.

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

Mon implémentation diffère légèrement de vos spécifications. Vous dites que ça devrait être impossible demander la taille de l'utilisateur puis demander son poids. Je dis que cela devrait être possible - le résultat n'aura pas forcément le type que vous vouliez (parce que vous avez ajouté deux choses à l'environnement, pas une). Cela vient utile ici, où askOrCalculateSize est juste une boîte noire qui ajoute un Size (et rien d'autre) à un environnement. Parfois, il le fait en demandant directement la taille; parfois il le calcule en demandant d'abord la taille et le poids. Peu importe le vérificateur de type.

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))

Il reste une question: comment peut-on CV un calcul à partir d'un état persistant? Vous ne connaissez pas statiquement le type de l’environnement d’entrée (bien qu’il soit sûr de supposer que la sortie est toujours (Colour, Size)) car elle varie tout au long du calcul et vous ne le savez pas tant que vous n’avez pas chargé l’état persistant.

L'astuce consiste à utiliser un peu de preuve GADT sur laquelle vous pouvez faire correspondre apprendre quel était le type Stage représente l'endroit où vous pourriez vous engager dans le processus, et il est indexé par le type que l'environnement devrait avoir à ce stade. Suspended jumeler un Stage avec les données réelles qui étaient dans l'environnement au moment où le calcul a été suspendu.

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

Vous pouvez maintenant ajouter des points de suspension au calcul:

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

resume fonctionne, mais il est assez moche et a beaucoup de duplication de code. C'est parce qu'une fois que vous avez mis en place une monade d'état, vous ne pouvez plus la démonter pour la regarder à l'intérieur. Vous ne pouvez pas intervenir à un moment donné dans le calcul. C'est le grand avantage de votre conception originale, dans laquelle vous représentez la machine d'état en tant que structure de données pouvant être interrogée afin de déterminer comment reprendre le calcul. Ceci s'appelle un initiale l'encodage, alors que mon exemple (représentant la machine d'état en tant que fonction) est un final codage. Les encodages finaux sont simples mais les encodages initiaux sont flexibles. J'espère que vous pouvez voir comment adapter une approche initiale à la conception de monade indexée.


6
2017-09-05 12:57