Typsicherer Fluss (Zustandsmaschine)

Question

Ich versuche, in Haskell einen typsicheren Frage-Antwort-Fluss zu erstellen. Ich modelliere QnA als gerichteten Graph, ähnlich einem FSM.

Jeder Knoten in dem Graphen stellt eine Frage:

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

s ist der Eingangszustand, a ist die Antwort auf die Frage und s' ist der Ausgangszustand. Knoten hängen vom Eingangszustand s ab, was bedeutet, dass wir für die Verarbeitung der Antwort in einem bestimmten Zustand vorher sein müssen.

Question a stellen eine einfache Frage/Antwort dar, die eine Antwort vom Typ a erzeugt.

Durch typsichere I bedeuten, zum Beispiel einen Knoten Node2 :: si -> a -> s2 gegeben, wenn auf sis1 hängt dann alle endende Pfade mit Node2 müssen durch einen Knoten sein, die Weitergabe s1 ersten produziert. (Wenn s1 == si, dann müssen alle Vorgänger von Node2s1 produzieren).

Ein Beispiel

QnA: In einer Online-Shopping-Website, müssen wir den Körper des Benutzers Größe und Lieblingsfarbe fragen.

1. e1: fragen Sie den Benutzer, ob er seine Größe kennt. Wenn ja, gehen Sie zu e2, gehen Sie andernfalls zu e3
2. e2: fragen Sie die Größe des Benutzers und gehen Sie zu ef, um die Farbe zu fragen.
3. e3: (Benutzer kennt ihre Größe nicht), fragen Sie das Gewicht des Benutzers und gehen Sie zu e4.
4. e4: (nach e3) fragt Höhe des Benutzers und ihre Größe berechnen und gehen Sie zu ef.
5. ef: Benutzer der Lieblingsfarbe stellen und den Fluss mit dem Final Ergebnis beenden.

In meinem Modell, schließen Edge s Node s zueinander:

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 ist das Endergebnis der QnA, das hier ist: (Bool, Size, Color).

Der QnA-Status zu jedem Zeitpunkt kann durch ein Tupel dargestellt werden: (s, EdgeId). Dieser Zustand ist serialisierbar und wir sollten in der Lage sein, einen QnA fortzusetzen, indem wir nur diesen Zustand kennen.

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 

Voll Code:

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

Es ist wichtig für mich, die Kanten typsicher zu halten.Bedeutung zum Beispiel falsch Verknüpfung e2 zu e3 muss ein Typ Fehler sein: e2 = Edge E2 n2 (const $ const ef) ist in Ordnung durch e2 = Edge E2 n2 (const $ const e3) muss ein Fehler sein.

Ich habe meine Fragen mit --TOOD angegeben:

• meine Kriterien Gegeben für Kanten typsicher, halten Edge s sf muss einen Eingabetyp Variable (s) haben wie kann ich dann getEdge :: EdgeId -> Edge s sf Funktion erstellen?

• Wie kann ich die respond Funktion, die den aktuellen Zustand s und aktuellen Rand Edge s sf entweder kehrt den Endzustand (wenn die aktuellen Rand ist Final) oder den nächsten Zustand und die nächste Flanke (s', Edge s' sf) gegeben schaffen?

Mein Design von Node s a s' und Edge s sf könnte einfach falsch. Ich muss nicht dabei bleiben.

Answer 1

Um ein einfaches Beispiel zu erklären, werde ich Ihnen eine Lösung zeigen, die keine natürliche Unterstützung für das Aussetzen, Fortsetzen und Fortsetzen von Berechnungen bietet. Am Ende gebe ich Ihnen den Grund, wie Sie das hinzufügen können - hoffentlich können Sie das Wesentliche selbst herausfinden.

---

Hier ist die sogenannte indiziert Zustand Monade:

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

IStateT ist wie ein normaler Monade Transformator Zustand, mit der Ausnahme, dass die Art des impliziten Staates darf im Verlauf der Änderungen eine Berechnung. Sequenzierungsaktionen in der Monade des indizierten Zustands erfordern, dass der Ausgabezustand einer Aktion mit dem Eingabezustand der nächsten übereinstimmt. Diese Art von Domino-ähnlicher Sequenzierung ist das, was Atkey's parameterised monad (oder indexed monad) ist.

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 ist die Klasse der Monade artige Dinge, die einen Weg durch eine indizierte Graph beschreiben. Der Typ von (>>>=) sagt "Wenn Sie eine Berechnung haben, die von i zu j und eine Berechnung von j zu k geht, kann ich ihnen beitreten, um Ihnen eine Berechnung von i zu k zu geben".

Wir brauchen auch Berechnungen aus der klassischen Monaden in indexierte Monaden heben:

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

Beachten Sie, dass der Code für IStateT ist genau das gleiche wie der Code für den regulären Zustand Monade - es ist nur die Typen, die sind schlauer geworden.

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) 

Die Idee ist, dass monadischen Aktionen wie askSize und askWeight (unten) werden , wachsen seine Art, einige Daten zu der impliziten Umgebung hinzuzufügen. Daher werde ich die implizite Umgebung aus verschachtelten Tupeln erstellen und sie als Typenlisten auf Typenebene behandeln. Verschachtelte Tupel sind flexibler (wenn auch weniger effizient) als flache Tupel, da sie es ermöglichen, über das Ende der Liste hinaus zu abstrahieren. Auf diese Weise können Tupel beliebiger Größe erstellt werden.

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 

Meine Implementierung unterscheidet sich geringfügig von Ihrer Spezifikation. Sie sagen, es sollte unmöglich sein nach der Größe des Benutzers fragen und dann nach ihrem Gewicht fragen. Ich sage, es sollte möglich sein - das Ergebnis wird nicht unbedingt den gewünschten Typ haben (weil Sie der Umgebung zwei Dinge hinzugefügt haben, nicht einen). Dies kommt hier nützlich, wo askOrCalculateSize nur eine Blackbox ist, die eine Size (und nichts anderes) zu einer Umgebung hinzufügt. Manchmal tut es das, indem man direkt nach der Größe fragt; manchmal berechnet es es, indem es zuerst nach der Höhe und dem Gewicht fragt. Es spielt keine Rolle, was den Typ-Checker angeht.

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

---

Es ist eine Frage noch: Wie kann man wieder eine Berechnung von einem persistenten Zustand? Sie kennen den Typ der Eingabeumgebung nicht statisch (obwohl es sicher ist, dass die Ausgabe immer (Colour, Size) ist), da sie während der Berechnung variiert und Sie erst dann wissen, wenn Sie den permanenten Zustand laden, in dem sie ausgeführt wurde.

Der Trick besteht darin, ein bisschen GADT Beweise zu verwenden, die Sie auf Muster gemustert werden können, was der Typ war. Stage steht für die Stelle, an der Sie während des Vorgangs hätte arbeiten können, und es wird nach dem Typ indiziert, den die Umgebung zu diesem Zeitpunkt haben sollte. Suspended verbindet ein Stage mit den tatsächlichen Daten, die in der Umgebung an dem Punkt war, an dem die Berechnung ausgesetzt wurde.

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 

Jetzt können Sie Aufhängungspunkte der Berechnung hinzufügen:

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

resume funktioniert, aber es ist ziemlich hässlich und eine Menge Code-Duplizierung hat. Das ist so, weil du, sobald du eine Staatsmonade zusammengefügt hast, sie nicht mehr auseinander nehmen kannst, um hineinzusehen. Sie können nicht an einem bestimmten Punkt in der Berechnung einspringen. Dies ist der große Vorteil Ihres ursprünglichen Entwurfs, bei dem Sie die Zustandsmaschine als Datenstruktur dargestellt haben, die abgefragt werden kann, um herauszufinden, wie die Berechnung fortgesetzt werden kann. Dies nennt man eine initiale Codierung, während mein Beispiel (das die Zustandsmaschine als eine Funktion darstellt) eine endgültige Kodierung ist. Endcodierungen sind einfach, aber die anfänglichen Codierungen sind flexibel. Hoffentlich können Sie sehen, wie Sie einen ersten Ansatz für das indizierte Monad-Design anpassen können.