使用带有类型注释树的Bound

loading...


15

我正在使用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回答

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

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

loading...

评论

暂时没有评论!