描述纯值和（索引的 monadic）不纯值的 AST 的评估器

Question

我有一个 AST，它描述了纯计算和不纯计算，不纯计算在类型级别跟踪状态。我正在使用 HOAS 表示；AST GADT的相关构造函数如下：

data AST a where
  Lam :: (AST a -> AST b) -> AST (a -> b)
  (:$) :: AST (a -> b) -> AST a -> AST b

  Return :: AST (a -> (a := i) i)
  Bind :: AST ( (a := j) i -> ( a -> q j ) -> q i )

  -- then some stateful operations
  -- for instance if the indexed state keeps track of a CD player tray:
  -- OpenCDPlayer :: AST ( ( () := 'Open ) 'Closed )
  -- CloseCDPlayer :: AST ( ( () := 'Closed ) 'Open )

这(a := j) i是 McBride 的AtKey类型，它由带有开始和结束状态（分别为i和j）注释的类型组成。Bind对应于 McBride 的“天使绑定”，归结为提供一个函数

bind :: AST ( (a := j) i ) -> Codensity AST (a := j) i

在哪里 Codensity是通常的共密度变换的索引版本。

我的问题是如何在这种情况下实施评估。通常，一个评估函数的形式如下：

eval :: AST a -> a

然而，在这种情况下，我不知道给评估函数提供什么类型，因为当涉及状态注释类型时，我认为评估应该被表述为具有接近以下类型的类型：

evalM :: Codensity AST (a := j) i -> Codensity ((->) St) (a := j) i

whereSt允许我们在值级别跟踪状态，因此右侧是一个索引状态 monad ( Codensity ((->) s) ~ State s)。
这种类型签名 forevalM看起来相当直观，因为它描述了索引 monad 的自然转换，并且似乎是手头任务的核心。

问题：在这种情况下，我如何制定和实施评估？它应该有什么类型，我将如何实现evalM上面的功能？