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

Question

使用这个简单的基础仿函数和其他机器来获得具有约束条件的免费monad:

{-# 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))

我希望能够做的是以下列方式推理绑定术语:

• 看看PureAST 中的术语
• 注意那里出现的绑定变量
• 注释AST中的相应绑定节点

如果没有进行某种配对,直接通过cofree comonad注释一个免费的monad AST似乎是不可能的,但你可以想象得到类似下面注释的AST(通过,比方说Fix),其中出现的节点绑定变量用Pure注释Just True:

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

那么:有没有办法以这种特殊的方式检查这样的程序中的绑定？即,不引入不同类型变量点菜这个问题,例如.

我怀疑这可能是不可能的.类似的选项data-reify是有吸引力的,但它似乎是非常困难或不可能进行ProgF必要的类型类(的实例Foldable,Traversable,MuRef).

这种直觉是正确的,还是有一些方法可以做到这一点,我没有考虑过？请注意,我很乐意接受任何令人毛骨悚然的不安全或动态手段.

Answer 1

我很满意，这是不可能通过任何“理智”的临时方法来完成的，出于同样的原因，不可能检查例如的绑定结构\a -> \b -> \c -> b + a。