检查自由 monad AST 中的绑定结构

Question

将这个简单的基本仿函数和其他机制用于带有绑定项的免费单子：

{-# LANGUAGE DeriveFunctor #-}

import Control.Monad.Free

data ProgF r =
    FooF (Double -> r)
  | BarF Double (Int -> r)
  | EndF
  deriving Functor

type Program = Free ProgF

foo   = liftF (FooF id)
bar a = liftF (BarF a id)

这是一个简单的程序

prog :: Program Int
prog = do
  a <- foo
  bar a

它有以下（手工制作的）AST：

prog =
  Free (FooF (\p0 ->
    Free (BarF p0 (\p1 ->
      Pure p1))

我希望能够通过以下方式对约束条件进行推理：

查看 AST 中的 Pure 项
注意那里出现的绑定变量
在AST中标注相应的绑定节点

如果不做 some kind of pairing，直接通过 cofree comonad 注释一个免费的 monad AST 似乎是不可能的，但你可以想象得到类似下面注释 AST 的东西（通过，比如说，Fix）其中 Pure 中出现的节点绑定变量用 Just True:

注释

annotatedProg =
  Just False :< FooF (\p0 ->
    Just True :< BarF p0 (\p1 ->
      Nothing  :< EndF))

那么：有没有办法以这种特别的方式检查像这样的程序中的绑定？即，不引入不同的变量类型 à la this question，例如

我怀疑这可能是不可能的。 data-reify 之类的选项很有吸引力，但似乎很难或不可能使 ProgF 成为必需类型类的实例（Foldable、Traversable、MuRef） .

这种直觉是正确的，还是有一些我没有考虑过的方法可以做到这一点？请注意，我很乐意接受任何可怕的不安全或动态方式。

Answer 1

我很满意这不可能通过任何 'sane' 临时方法来完成，原因与无法检查绑定结构的原因大致相同。 \a -> \b -> \c -> b + a.

检查自由 monad AST 中的绑定结构

Examining the binding structure in a free monad AST

haskell

free-monad