使用带有类型注释树的Bound

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

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

为了能够使用abstractinstantiateExp ,我定义了一个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用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)

... 也许?

回答(1)

3 years ago

Disclaimer :我不确定这是理论上的做事方式,但似乎有用 . )

这个问题 Build 在错误的假设上,即统一应该是替代的一部分 . 这在使用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不假设存在类型 .

由于这个属性,重写这四个函数以使用像 TypeLikeAnnotatable 这样的类最终只会执行无关紧要的统一,因为其中一个值总是有一个新类型 . 因此没有必要概括图书馆 .

没必要

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