使用带类型注解的树的绑定

Question

我使用Bound库来表示lambda术语：

data Exp a = Var a
           | Exp a :@: Exp a
           | Lam (Scope () Exp a)

为了能够在Exp中使用abstract和instantiate，我定义了一个monad实例：

instance Monad Exp where
    return = Var
    Var a >>= f = f a
    (x :@: y) >>= f = f >>= x :@: f >>= y
    Lam e >>= f = Lam $ e >>>= f

(其中>>>=在Bound中定义。)

现在，我想对上面的代码做一个带类型注释的版本。我想我只需要做

data Exp a = Var a
           | TypedExp a :@: TypedExp a
           | Lam (Scope () TypedExp a)

data TypedExp a = TypedExp Type (Exp a)

问题是abstract的类型是

abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a

这意味着，除非我想简单地在替换时丢弃类型，否则我必须使TypedExp成为monad。我可以看到操作的直觉: return创建一个具有无约束类型的变量，而bind执行具有统一的替换。但是要生成新的变量并执行统一，我需要某种状态。

在工作了一段时间之后，我想出了一个相当自然的定义

return' :: a -> MyState (TypedExp a)
bind' :: TypedExp a -> (a -> MyState (TypedExp b)) -> MyState (TypedExp b)

但是我不能进入一个实际的monad实例，它可以做我想做的事情。

我是否可以将类型转换为可以在编写时使用Bound的内容？我是否应该去写一个更通用的abstract版本，比如...

data Typed f ty a = Typed ty (f ty a)

class TypeLike ty where
    data Unification ty :: * -> *
    fresh :: Unification ty ty
    unify :: ty -> ty -> Unification ty ty

class Annotatable f where
    typedReturn :: TypeLike ty => a -> Unification ty (Typed exp ty a)
    typedBind :: TypeLike ty => Typed f ty a -> (a -> Unification ty (Typed f ty b)) -> Unification ty (Typed f ty b)

abstract :: (Annotatable f, TypeLike ty) => (a -> Maybe b) -> Typed f ty a -> Unification (Scope b (Typed f ty) a)

..。也许吧？

Answer 1

(免责声明：我不确定这是理论上“正确”的做法，但它似乎是有效的。)

这个问题基于一个错误的假设，即统一应该是替代的一部分。在使用Bound时，这是没有好处的，也不是确保正确自动统一所必需的。

无益

Bound提供了几个需要monad实例的函数。这四个关键问题是

abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a
instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a
fromScope :: Monad f => Scope b f a -> f (Var b a)
toScope :: Monad f => f (Var b a) -> Scope b f a

所有这些都不能提供作为类型信息有用的额外信息。它们改变了变量的表示方式，甚至可能改变了树的表示方式，但仅以不对类型做进一步假设的方式。这是有意义的，因为绑定并不假定类型的存在。

由于这个属性，重写这四个函数来使用像TypeLike和Annotatable这样的类，最终只会执行无关紧要的统一，因为其中一个值总是具有新的类型。因此，没有必要对该库进行泛化。

不必了

问题中出现的问题是由Lam构造函数的错误定义引起的。我们注释得太多了。考虑表达式\x. a

Lam $ Scope $ (TypedExp t $ Var $ F (TypedExp t $ Var "a"))

在这里，类型t是重复的。我们可以通过改变注释类型的方式来消除这种重复，并解决与Lam相关的问题：

data Typed a = Typed Type a

data Exp a = Var a
           | Typed (Exp a) :@: Typed (Exp a)
           | Lam Type (Typed (Scope () Exp a))

现在我们可以通过简单地总是假设类型被保留来编写monad实例：

instance Monad Exp where
    return = Var
    Var a >>= f = f a
    (Typed tx x :@: Typed ty y) >>= f = Typed tx (f >>= x) :@: Typed ty (f >>= y)
    Lam tp (Typed te e) >>= f = Lam tp $ Typed te (e >>>= f)

这在一般情况下并不总是正确的，但在调用绑定函数时总是正确的。如果需要更多类型安全，可以将这些内容拆分到helper函数中：

UniContext :: * -> * -- some monad we can do unification in
fresh :: UniContext Type
unify :: Type -> Type -> UniContext Type
-- (a -> b) and a to b
applyType :: Type -> Type -> UniContext Type
-- b and a to a -> b
unapplyType :: Type -> Type -> UniContext Type

variable :: a -> Typed (Exp a)
variable x = (\tx -> Typed tx (return x)) <$> fresh

(|@|) :: Typed (Exp a) -> Typed (Exp a) -> UniContext (Typed (Exp a))
x@(Typed tx _) |@| y@(Typed ty _) = do
    txy <- applyType tx ty
    return $ Typed txy (x :@: y)

lambda :: a -> Typed (Exp a) -> UniContext (Typed (Exp a))
lambda p (Typed te e) = do
     tp <- fresh
     tf <- unapply te tp
     let f = abstract1 p e
     return $ Lam tp $ Typed tf f

这在构建树时提供了足够的保证，因为在所有情况下都会执行统一。如果我们不导出Typed的构造函数，我们可以提供一个函数

bindTyped :: Typed x -> (x -> UniContext (Typed y)) -> UniContext (Typed y)

它将执行统一。请注意，在这种情况下，x不是像上面那样对应于a，而是对应于Exp a；可以使用整个表达式的值来执行计算，而不仅仅是变量。(请注意，这将排除所有类型修改转换，这可能是不可取的。)