HOAS的复制机翻译

Question

在关于DSL的无标记最终解释器的这些非常酷的注释的第2.3节中,Oleg Kiselyov展示了如何解决一次解析序列化DSL表达式并多次解释它的问题.

简而言之,他用类型表明了"伪造的一流多态"

newtype Wrapped = Wrapped (? repr. ExpSYM repr ? repr)
fromTree :: String ? Either ErrMsg Wrapped

不令人满意,因为它是不可扩展的:我们必须有不同的Wrapper/ fromTree为每个组上的约束repr.因此,我倾向于使用他的复制器解释器的解决方案.这个问题是关于如何使用HOAS的解释器.

具体来说,请考虑以下语言进行目标语言绑定:

class Lam repr where
  lam :: (repr a -> repr b) -> repr (a -> b)
  app :: repr (a -> b) -> repr a -> repr b

我在为复制器解释器提供类的声音实例时遇到了麻烦Lam.这就是我所拥有的:

data Dup repr1 repr2 a = Dup {unDupA :: repr1 a, unDupB :: repr2 a}

instance (Lam repr1, Lam repr2) => Lam (Dup repr1 repr2) where
  lam f = Dup (lam $ unDupA . f . flip Dup undefined) (lam $ unDupB . f . Dup undefined)
  app (Dup fa fb) (Dup a b) = Dup (app fa a) (app fb b)

是否有某种方法可以为我的类型提供不涉及的类型的递归实例？LambdaDupundefined

我一直在使用的更强大的版本也试图lam从本文中,允许一元与高阶像差口译员,虽然我没有看到它如何帮助我的实例Dup.使用lamHOAS 版本的解决方案非常棒!

---

_{*:Oleg展示了如何使用de Bruijn索引定义声音实例,但我真的对HOAS的解决方案感兴趣.}

    class Lam repr where
      lam :: repr (a,g) b -> repr g (a -> b)
      app :: repr g (a->b) -> repr g a -> repr g b

    data Dup repr1 repr2 g a = Dup{d1:: repr1 g a, d2:: repr2 g a}

    instance (Lam repr1, Lam repr2) => Lam (Dup repr1 repr2) where
      lam (Dup e1 e2) = Dup (lam e1) (lam e2)
      app (Dup f1 f2) (Dup x1 x2) = Dup (app f1 x1) (app f2 x2)

Answer 1

这是不可能的。

为了展示一个例子，我将首先创建一个非常简单的实例Lam：

newtype Id a = Id a

instance Lam Id where
    lam (Id f) = Id (\x -> let Id r = f x in r)
    app (Id f) (Id x) = Id (f x)

现在我将创建一个对 s 进行操作的函数Dup：

f :: Dup Id Id Int -> Dup Id Id Int
f (Dup (Id x) (Id y)) = Dup (Id x*y) (Id y)

从一个例子来看Lam，我能够做到lam f :: Dup Id Id (Int -> Int)。这可能看起来像

Dup (Id (\x -> x*y)) (Id (\y -> y))

这是无法实现的，因为y无法从x-lambda 中获得。（在这里使用sundefined替换，只要它不能很好地工作就会抛出运行时错误。）这种情况并不罕见：只要您在另一个结果中使用其中一个变量，就会发生这种情况。yundefined

我不确定您对更强的Monad通用化要求是什么，但这也发生在其他Monads 上：例如，使用Maybe，您无法将以下内容转换为 a Maybe (Int -> Int)，因为它取决于给定的值：

f :: Maybe Int -> Maybe Int
f m = m >>= \x -> if x > 5 then Just x else Nothing

（您可以使用fromJust它并希望没有人这样做，但这与解决方案相同undefined。）

undefined不过，只有当函数需要查看其他变量时， s 才会抛出错误。如果您绝对确定它永远不会在类似的东西上运行（例如，您将展开/创建限制为经过广泛测试的隐藏模块），那么这种undefined方式就可以工作。

对此还有一个建议：使用更详细的error消息而不是undefined，以防出现问题。