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

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