6

将这个简单的基本函子和其他机器用于具有约束条件的免费 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似乎非常困难或不可能。ProgFFoldableTraversableMuRef

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

4

1 回答 1

1

我很满意任何“理智”的临时方法都无法做到这一点，原因与无法检查 eg 的绑定结构的原因大致相同\a -> \b -> \c -> b + a。

于 2015-11-16T08:20:12.323 回答