Using Bound with a type-annotated tree

Question

I'm using the Bound library to represent lambda terms:

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

In order to be able to use abstract and instantiate with Exp, I have a monad instance defined:

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

(Where >>>= is defined in Bound.)

Now I'd like to make a type-annotated version of the above. I thought I'd just do

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

data TypedExp a = TypedExp Type (Exp a)

The problem is that the type of abstract is

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

That means that unless I want to simply discard types on substitution, I have to make TypedExp a monad. I can see the intuition for the operations: return creates a variable with an unconstrained type, and bind performs substitution with unification. But to generate fresh variables and perform unification I need some kind of state.

After working at it for a while, I came up with fairly natural definitions for

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

but I can't make the step to an actual monad instance that would do what I want.

Can I twist the types into something that will work with Bound as it is written? Should I go for writing a more general version of abstract, something like...

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)

... perhaps?

Answer 1

(Disclaimer: I am not sure this is the theoretically "correct" way of doing things, but it seems to work.)

This question rests on the incorrect assumption that unification should be part of substitution. This is not beneficial when it comes to using Bound, nor necessary to ensure correct automatic unification.

Not beneficial

Bound provides several functions that require the monad instance. The four key ones are

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

None of these provide extra information that could be useful as type info. They change the way variables are represented and may even change how the tree is represented, but only in ways that make no further assumptions about the types. This makes sense, as Bound doesn't assume the presence of types.

Due to this property, rewriting these four functions to use classes like TypeLike and Annotatable would end up only performing unifications which are trivial anyway, as one of the values would always have a fresh type. There is thus no need to generalise the library.

Not necessary

The problem in the question arises is caused by an incorrect definition of the Lam constructor. We annotate too much. Consider the expression \x. a:

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

Here, the type t is duplicated. We can remove this duplication and solve our problems concerning Lam by changing the way we annotate types:

data Typed a = Typed Type a

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

Now we can write the monad instance by simply always assuming the type is preserved:

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)

This is not always true in general, but it is always true when invoking Bound functions. If more type-safety is desired, these things can be split off into helper functions:

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

This provides sufficient guarantees when building up a tree, as unification is performed in all cases. If we do not export the constructor of Typed, we can provide a function

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

which would perform unification. Note that in this case, x corresponds not to a as above, but rather to Exp a; it is possible to use the value of the whole expression, rather than just the variables, to perform the computation. (Note that this excludes all type-modifying transformations, which might be undesirable.)