使用带有类型注释树的Bound

Question

我正在使用Bound库来表示lambda术语:

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

为了能够使用abstract并instantiate用Exp,我定义了一个单子实例:

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用unification执行替换.但是为了生成新变量并执行统一,我需要某种状态.

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

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

这些都不提供可用作类型信息的额外信息.它们改变了变量的表示方式,甚至可能改变树的表示方式,但只能以不对类型做出进一步假设的方式.这是有道理的,因为Bound不假设存在类型.

由于这个属性,重写这四个函数以使用类似的类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)

这通常并不总是正确的,但在调用Bound函数时总是如此.如果需要更多的类型安全性,这些东西可以分成辅助函数:

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; 可以使用整个表达式的值而不仅仅是变量来执行计算.(请注意,这排除了所有类型修改转换,这可能是不合需要的.)