检查自由monad AST中的绑定结构-Java 学习之路

使用这个简单的基础仿函数和其他机器来获得具有约束条件的免费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))

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

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

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

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

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

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

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

1 回答

1

我无法检查例如结合的结构 . \a -> \b -> \c -> b + a .

回复于 2024-04-20T15:15:44+08:00

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

1 回答

相关问题