首页 文章

使用带有类型注释树的Bound

提问于
浏览 次
15

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

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

为了能够使用abstract和instantiate与 Exp ，我定义了一个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)

... 也许？

haskell monads

1 回答

  • 5

    （ 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不假设存在类型 .

    由于这个属性，重写这四个函数以使用像 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 ;可以使用整个表达式的值而不仅仅是变量来执行计算 . （请注意，这排除了所有类型修改转换，这可能是不合需要的 . ）

    回复于

相关问题