相关疑难解决方法(0)

我正在尝试按照我的建议回答这个stackoverflow问题,uniplate但到目前为止我提出的唯一解决方案非常难看.

这似乎是一个相当普遍的问题,所以我想知道是否有更优雅的解决方案.

基本上,我们有一个GADT可以解析为Expression Int或者Expression Bool(忽略codataIf = If (B True) codataIf codataIf):

data Expression a where
    I :: Int -> Expression Int
    B :: Bool -> Expression Bool
    Add :: Expression Int  -> Expression Int  -> Expression Int
    Mul :: Expression Int  -> Expression Int  -> Expression Int
    Eq  :: Expression Int  -> Expression Int  -> Expression Bool
    And :: Expression Bool -> Expression Bool -> …

{-# LANGUAGE RankNTypes #-}

继续前一系列问题,我有一个带有通用量化函数作为参数的函数,如下所示:

emap :: (forall a. Expression a -> Expression a) -> Expression b -> Expression b

对于不需要额外约束的函数,可以使用哪个,例如:

postmap :: (forall a. Expression a -> Expression a) -> Expression b -> Expression b
postmap f = f . emap (postmap f)

reduce = postmap step

但是,我现在想要将此函数与带有附加约束的函数一起使用,但以下内容不进行类型检查.

substitute :: Pack a => Identifier -> a -> Expression a -> Expression a
substitute i v (Var x) | x == i = pack v
substitute _ _ …