Idris2实现App能否不借助IORef完成打结或规避该操作？

解决方案核心思路 #

你遇到的本质是view和model的循环依赖问题：view需要输入发送器把用户事件传给model，model需要输出更新器来刷新view，之前用IORef或者MonadFix都是为了给这个循环依赖「打结」，但两种方案都有明显缺陷。在Idris2中我们可以通过显式事件队列解耦循环依赖，完全规避可变引用和MonadFix的问题。

方案1：推荐重构App接口（符合Elm架构规范） #

这是最稳妥的方案，直接从定义层面消除循环依赖，架构也更易维护：

record App (m : Type -> Type) (input : Type) (output : Type) where
  constructor MkApp
  -- view接收当前输出状态、输入事件发送器，直接完成渲染，不需要返回刷新函数
  view : output -> (input -> m ()) -> m ()
  -- 纯更新函数，如果需要执行副作用可以扩展为 input -> output -> m (output, List (Cmd m))
  update : input -> output -> output
  -- 初始状态
  initial : output

对应的runApp实现完全不需要IORef或MonadFix，用事件循环处理所有输入：

import Control.Concurrent.STM.TQueue
import Control.Monad.STM

runApp : HasIO m => App m input output -> m ()
runApp app = do
  -- 初始化事件队列，所有输入事件先写入队列再统一处理
  eventQueue <- newTQueue
  let
    -- 渲染逻辑：用当前状态渲染UI，绑定的事件回调直接把输入写入队列
    render currentState = app.view currentState (\evt => atomically $ writeTQueue eventQueue evt)
    -- 事件循环：渲染 -> 取事件 -> 更新状态 -> 下一轮循环
    eventLoop currentState = do
      render currentState
      inputEvt <- atomically $ readTQueue eventQueue
      let newState = app.update inputEvt currentState
      eventLoop newState
  eventLoop app.initial

这个方案的优势：

• 没有任何可变引用，也不需要MonadFix，完全规避运行时崩溃风险
• 无论view是同步还是异步触发输入回调，事件都会先入队列等待当前渲染完成后再处理，不会出现回调未绑定的问题
• 事件流完全显式，方便后续加日志、事件回放、中间件等扩展能力

方案2：兼容原有App接口的实现 #

如果你不想修改已有的App定义，也可以用事件队列代替IORef解耦：

import Control.Concurrent.STM.TQueue
import Control.Concurrent
import Control.Monad.STM

runApp : (HasIO m, MonadConc m) => App m input output -> m ()
runApp app = do
  eventQueue <- newTQueue
  -- 给view的输入回调只负责把事件写入队列，不直接调用model
  refresh <- app.view (\input => atomically $ writeTQueue eventQueue input)
  -- 启动独立协程处理所有输入事件
  fork $ forever $ do
    input <- atomically $ readTQueue eventQueue
    output <- app.model input
    refresh output
  -- 首次渲染
  refresh app.initial

这个实现同样消除了IORef，就算view在返回前同步调用输入回调，事件也会暂存在队列中，等refresh绑定完成、事件处理协程启动后才会执行，不会出现运行时错误。

内容的提问来源于stack exchange，提问作者Cactus