使用索引数据类型解释计算构建的替代方法

Question

在一本 'Type-Driven Development with Idris' 书中，有几个使用 monadic 数据类型编码 "programs" 的示例（导致使用索引数据类型进行有用的类型安全编码）。通常，每个这样的数据类型在特定上下文中都可以是运行（出于学习目的，它主要是 IO）。

我试图写另一个 'runner'，它不会在 monadic 上下文中执行，而是有一个函数可以在给定一些输入的情况下执行一个 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

不会削减它，因为调用者不会指示结果状态。这让我尝试 'hiding' 那些具有依赖对的参数：

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

意思是"run this program in particular state for me, I don't care what resulting state (indexes) will be".

但是，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)

但是类型错误很快就变得太多了，而且很多工作只是为了 'recreate' 了解转换（无论如何已经由转换定义）的依赖对的值。这使我认为我走错了路。如何尝试编写这样的解释器？

Answer 1

我已经完成了我在对该问题的第二条评论中概述的内容。类型检查器成功地说服了我应该有一些不同的方法。如果为更简单的数据类型编写 'step' 解释器很容易，而索引数据类型使它变得更难，那么为什么不用一些抽象数据类型定义 run，这将允许我们构建 'simply' 类型结构更容易解释？

让我们回顾一下：

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

这又是相当标准的，我们获得的是一个更简单的类型，使我们的解释更容易，并使我们摆脱一些繁重的类型。

我们还需要一个抽象 EventCtx 的实现，这样我们就可以使用 run 将我们的 Indexed 值转换为 Stepped 值:

  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

使用索引数据类型解释计算构建的替代方法

Alternative way of interpreting computation build with indexed datatype

idris