Альтернативный способ интерпретации построения вычислений с индексированным типом данных

Question

В книге «Разработка на основе типов с Idris» есть несколько примеров кодирования «программ» с использованием монадического типа данных (что приводит к полезным кодированиям с безопасным типом с индексированными типами данных).Обычно каждый такой тип данных может быть запущен в определенном контексте (для целей обучения это в основном IO).

Я попытался написать другого «бегуна», который не будет выполняться в монадическом контексте, а скореебыла бы функция для выполнения одного step при некотором вводе - если ввод соответствует текущему состоянию программы, мы передадим его значение и продолжим, получив следующее состояние программы.

Это просто ввести, еслитип данных не проиндексирован:

  data Prog : Type -> Type where
    Req : Prog String
    Pure : a -> Prog a
    (>>=) : Prog a -> (a -> Prog b) -> Prog b

  data Event = Resp String

  run : Prog a -> Event -> Prog a
  run Req (Resp s) = Pure s
  run (Pure x) _ = Pure x
  run (x >>= f) ev = let x' = run x ev
                    in case x' of
                          Pure v => f v
                          v => v >>= f

И пример:

  prog : Prog String
  prog = do
    x <- Req
    y <- Req
    Pure (x ++ y)

  test : IO ()
  test = do
    -- this might doesn't look reasonable , but the point is that we could
    -- keep/pass program state around and execute it in whatever manner we wish
    -- in some environment
    let s1 = run prog (Resp "Hello, ")
    let s2 = run s1 (Resp "world")
    case s2 of
      Pure s => putStrLn s
      _ => putStrLn "Something wrong"

Кажется, что все работает нормально, но все усложняется, когда основной тип данных индексируется и отслеживает его состояние.в зависимости от типа (в зависимости от результатов):

data State = StateA | StateB

data Event = Resp String

data Indexed : (ty : Type) -> State -> (ty -> State) -> Type where
  Req : Indexed String StateA (\res => case res of "frob" => StateB; _ => StateA)
  Pure : (res : a) -> Indexed a (state_fn res) state_fn
  (>>=) : Indexed a state1 state2_fn
      -> ((res : a) -> Indexed b (state2_fn res) state3_fn)
      -> Indexed b state1 state3_fn

Внезапно, набрать функцию run не просто:

run : Indexed a s1 s2_fn -> Event -> Indexed a s3 s4_fn

не будетсократить его, потому что вызывающая сторона не диктует результирующее состояние.Это заставило меня попытаться «скрыть» эти параметры с зависимой парой:

run : Indexed a s1 s2_fn -> Event -> (s3 ** s4_fn ** Indexed a s3 s4_fn)

, что означает «запустить эту программу в определенном состоянии для меня, мне все равно, какое результирующее состояние (индексы) будет ".

Но тогда Pure становится проблематичным:

run (Pure x) _ = (?noIdea ** ?noIdeaAsWell ** (Pure x))

, поэтому, возможно, нам также понадобятся входные индексы:

run : (s1 ** s2_fn ** Indexed a s1 s2_fn) -> Event -> (s3 ** s4_fn ** Indexed a s3 s4_fn)

, но ошибки типа вскоре стали слишком большими, и много работы было бы просто «воссоздать» значения для зависимой пары, зная переход (который уже определен переходом в любом случае).Это заставляет меня думать, что я на неправильном пути.Как можно было бы попытаться написать такого переводчика?

Answer 1

Я придерживался того, что изложил во втором комментарии к вопросу.Проверка типов успешно убедила меня, что к этому должен быть иной подход.Если легко написать «пошаговый» интерпретатор для более простого типа данных, а индексированные типы данных усложняют его, то почему бы не определить run с некоторым абстрактным типом данных, который позволил бы нам создать «простую» типизированную структуру, более легкую для интерпретации?

Подведем итоги:

data State = StateA | StateB

data Indexed : (ty : Type) -> State -> (ty -> State) -> Type where
  Req : Indexed String StateA (const StateA)
  Pure : (res : a) -> Indexed a (state_fn res) state_fn
  (>>=) : Indexed a state1 state2_fn
      -> ((res : a) -> Indexed b (state2_fn res) state3_fn)
      -> Indexed b state1 state3_fn

Теперь давайте определим контекст выполнения и функцию run, которая будет работать в этом контексте.run даст нам окончательное значение, но сделает это с помощью некоторого абстрактного EventCtx, потому что все, что нам нужно, это получить значения из внешних событий, и нам все равно, как вычисления будут обрабатывать их:

namespace EventType
  data EventType = Req

data Event = Resp String

-- rename: eventType? what about EventType then :) ?
payloadType : EventType -> Type
payloadType EventType.Req = String

interface Monad m => EventCtx (m : Type -> Type) where
  fromEvent : (et : EventType) -> m (payloadType et)

run : EventCtx m => Indexed a s1 s2_fn -> m a
run Req = fromEvent EventType.Req
run (Pure res) = pure res
run (x >>= f) = do
  x' <- run x
  run (f x')

run теперь просто стандартное дело, ууу:)

Хорошо, но давайте проверим, как мы все еще можем запустить его шаг за шагом, с более простым типом, чтобымы можем где-то хранить промежуточные состояния (ожидая, когда произойдут события):

namespace SteppedRunner

  data Stepped : Type -> Type where
    Await : (et : EventType) -> Stepped (payloadType et)
    Pure : a -> Stepped a
    (>>=) : Stepped a -> (a -> Stepped b) -> Stepped b

  Functor Stepped where
    map f x = x >>= (\v => Pure (f v))

  Applicative Stepped where
    pure = Pure
    (<*>) f a = f >>= (\f' =>
                           a >>= (\a' =>
                                      Pure (f' a')))

  Monad Stepped where
    (>>=) x f = x >>= f

Это опять-таки довольно стандартно, мы получили более простой тип, облегчающий нашу интерпретацию и освобождающий нас от некоторых тяжелых-duty types.

Нам также нужна реализация нашего абстрактного EventCtx, чтобы мы могли использовать run, чтобы превратить наши Indexed значения в Stepped one:

  EventCtx Stepped where
    fromEvent = Await

Теперь наша функция для выполнения шага, заданного текущего состояния и события:

  step : Stepped a -> Event -> Either (Stepped a) a
  step s e = fst (step' s (Just e))
    where
    step' : Stepped a -> Maybe Event -> (Either (Stepped a) a, Maybe Event)
    step' (Await Req) (Just (Resp s)) = (Right s, Nothing) -- event consumed
    step' s@(Await _) _ = (Left s, Nothing) -- unmatched event (consumed)
    step' (Pure x) e = (Right x, e)
    step' (x >>= f) e = let (res, e') = step' x e
                        in case res of
                             Left x' => (Left (x' >>= f), e')
                             Right x => step' (f x) e'

Основная суть в том, что мы можем продолжать только тогда, когда мы связываем (>>=) значение, и мы можем получить значение, когда у нас есть Await и соответствующее событие.Отдых - это просто свертывание структуры, чтобы мы были готовы к другому значению события.

Некоторая программа тестирования:

test : Indexed String StateA (const StateA)
test = do
  x <- Req
  y <- do a <- Req
          b <- Req
          Pure (a ++ b)
  Pure (x++ y)

Вот как мы переходим от исходного, индексированного типа данных к ступенчатому.:

s : Stepped String
s = run test

А теперь просто ради получения результата в тестовой среде:

  steps : Stepped a -> List Event -> Either (Stepped a) a
  steps s evs = foldl go (Left s) evs
    where go (Right x) _ = Right x
          go (Left s) e = step s e

Некоторые повторения:

λΠ> steps s [Resp "hoho", Resp "hehe", Resp "hihihi"]
Right "hohohehehihihi" : Either (Stepped String) String