타입 안전 흐름 (상태 머신)

Question

하스켈에서 유형 안전 질문 - 답변 흐름을 만들려고합니다. QnA를 FSM과 비슷한 유향 그래프로 모델링했습니다.

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

sa가 질문에 대한 응답이며 s' 출력 상태, 입력 상태이다

그래프의 각 노드는 문제를 나타낸다. 노드는 입력 상태 s에 의존합니다. 즉, 응답을 처리하기 위해 이전에 특정 상태에 있어야합니다.

Question a은 a 유형의 답을 생성하는 간단한 질문/답변을 나타냅니다. si 처음 s1을 생성하는 노드를 통해 s1 다음 Node2로 끝나는 모든 경로를 통과해야에 의존하는 경우 내 말은 형태 보증으로

, 예를 들어, 노드 Node2 :: si -> a -> s2을 부여. s1 == si 인 경우 Node2의 모든 선행 작업은 s1을 생성해야합니다.

예제

문의 글이 : 온라인 쇼핑 웹 사이트에서, 우리는 사용자의 신체 크기와 좋아하는 색상을 요청해야합니다.

1. e1 : 사용자에게 크기를 알고 있는지 묻습니다. 그렇다면 e2으로 이동하십시오. 그렇지 않은 경우 e3
2. e2으로 이동하십시오 : 사용자의 크기를 묻고 으로 가서 색상을 문의하십시오.
3. e3 : (사용자는 크기를 알지 못함) 사용자의 무게를 묻고 e4으로 가십시오.
4. e4 : (e3 후) 사용자의 높이를 요청하고 자신의 크기를 계산하고 ef.
5. 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 여기 즉, 문의 글의 최종 결과입니다 (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 후 어떻게 getEdge :: EdgeId -> Edge s sf 함수를 만들 수있는 입력 형 변수 (s)가 있어야 유지에 대한 나의 기준을 감안할 때?

는

• 내가 현재 상태 s와 현재의 가장자리 Edge s sf 주어진 respond 함수를 만들 수있는 방법, 최종 상태 (현재의 가장자리 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까지 계산할 수 있습니다."

우리는 또한 색인 모나드로 고전 모나드에서 계산을 올려해야합니다 : IStateT의 코드 그냥 일반 상태 모나드의 코드와 동일한 지

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

주 - 그냥 유형의 그 더 똑똑해졌습니다.

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을 쌍으로합니다.

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

resume 일을하지만, 그것은 꽤 추한 및 코드 중복을 많이 가지고 :

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 

이제 계산에 정지 점을 추가 할 수 있습니다. 왜냐하면 일단 모나드를 합치면 내부를 들여다 볼 수 없기 때문입니다. 계산의 주어진 지점에서 점프 할 수 없습니다. 이것은 원래 디자인의 큰 장점입니다. 여기서 상태 시스템을 계산을 다시 시작하는 방법을 파악하기 위해 쿼리 할 수있는 데이터 구조로 표현했습니다. 이것은 초기 인코딩이라고하는 반면, (상태 머신을 기능으로 나타내는) 예는 최종 인코딩입니다. 최종 인코딩은 간단하지만 초기 인코딩은 유연합니다. 인덱스 된 모나드 디자인에 초기 접근법을 적용하는 방법을 알기를 바랍니다.