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

【问题标题】：Alternative way of interpreting computation build with indexed datatype使用索引数据类型解释计算构建的替代方法
【发布时间】：2018-10-13 20:21:42
【问题描述】：

在“使用 Idris 进行类型驱动开发”一书中，有几个使用 monadic 数据类型对“程序”进行编码的示例（导致使用索引数据类型进行有用的类型安全编码）。通常，每个这样的数据类型都可以在特定的上下文中运行（出于学习目的，它主要是IO）。

我试图编写另一个'runner'，它不会在单子上下文中执行，而是有一个函数来执行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)

但是类型错误很快就变得太多了，很多工作只是为知道转换的依赖对“重新创建”值（无论如何，转换已经定义了）。这导致我认为我走错了路。如何尝试编写这样的解释器？

【问题讨论】：

找到了一种更好的方式来表达一种存在类型，它真正意味着“我不在乎”（与依赖对不同）：gist.github.com/adituv/dcea611d75722560a3af64f5ae651804。只需要找出如何将其应用于“隐藏”多个类型变量。
我只是想知道这种解释计算的“步骤”方式是否有意义，也许更容易实现在某个 monad 的上下文中工作的传统“完整运行”函数将允许我实现并满足它将在其中运行的任何需求系统（从哪里获取输入，如何管理异步等等）。即使这意味着那里的解释器必须允许存储中间状态等，它也可以在更简单的非依赖类型上工作......

标签： idris

【解决方案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

这又是相当标准的，我们获得的是一种更简单的类型，使我们的解释更容易，并使我们从一些繁重的类型中解放出来。

我们还需要实现我们的抽象 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

【讨论】：