Mutually recursive syntaxes with Bound

Question

Here is the syntax for a notoriously typical lambda calculus.

data TermI a = Var a | App (TermI a) (TermC a) -- when type-checking an application, infer the type of the function and then check that its argument matches the domain | Star -- the type of types | Pi (Type a) (Scope () Type a) -- The range of a pi-type is allowed to refer to the argument value | Ann (TermC a) (Type a) -- embed a checkable term by declaring its type deriving (Functor, Foldable, Traversable) data TermC a = Inf (TermI a) -- embed an inferrable term | Lam (Scope () TermC a) deriving (Functor, Foldable, Traversable) type Type = TermC -- types are values in a dependent type system 

(I more or less removed this from Just easy .) The bidirectional type system , separating the terms into those whose types can be inferred from the input context and those that can only be checked against the target type. This is useful in systems of dependent types, since in general the lambda members will not be of a fundamental type.

Anyway, I'm stuck trying to define a Monad instance for this syntax:

 instance Monad TermI where return = Var Var x >>= f = fx App fun arg >>= f = App (fun >>= f) (arg >>= Inf . f) -- embed the substituted TermI into TermC using Inf Star >>= _ = Star Pi domain range >>= f = Pi (domain >>= Inf . f) (range >>>= Inf . f) Ann term ty >>= f = Ann (term >>= Inf . f) (ty >>= Inf . f) instance Monad TermC where return = Inf . return Lam body >>= f = Lam (body >>>= f) Inf term >>= f = Inf (term >>= _) 

To fill the hole in the last line of the TermC instance, I need something like a -> TermI b , but f is of type a -> TermC b . I cannot insert the resulting TermC into TermI using the Ann constructor, because I do not know the type of TermC .

Is this data type incompatible with the bound model? Or is there a trick I can use to create an instance of Monad ?

Answer 1

This is simply not possible: TermC not a monad. Substitution puts terms in place of variables. In order for this to make sense, the terms must be able to match, that is, be similar enough that the resulting term still has good properties. Here, this means that its type must be irrefutable. TermC will not do.

You can either implement:

  substI :: TermI a -> (a -> TermI b) -> TermI b substC :: TermC a -> (a -> TermI b) -> TermC b 

and

  instance Monad TermI where return = Var bind = substI