Взаимно-рекурсивные синтаксисы с привязкой

Question

Вот синтаксис для исчисления лямбды с зависимой типией.

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's 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 

(я более или менее поднял это от Simply Easy.) Система типа bidirectional, расщепляющие термины в тех, чьи типе может быть выведена из контекста набора текста, и те, которые могут быть проверены только против цели тип. Это полезно в системах зависимых типов, поскольку в общем случае лямбда-члены не будут иметь принципиального типа.

Во всяком случае, я застрял, пытаясь определить Monad экземпляр для этого синтаксиса:

instance Monad TermI where 
    return = Var 
    Var x >>= f = f x 
    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 >>= _) 

Чтобы заполнить дыру в последней строке, например TermC «s, мне нужно что-то типа a -> TermI b но f имеет тип a -> TermC b. Я не могу вставить полученный TermC в TermI с помощью конструктора Ann, потому что я не знаю тип TermC.

Является ли этот тип данных несовместимым с моделью bound? Или есть трюк, который я могу использовать, чтобы сделать экземпляр Monad?

Answer 1

Это просто невозможно сделать: TermC не является монадой. Замещение ставит термины вместо переменных. Для того чтобы это имело смысл, термины должны быть в состоянии соответствовать, то есть быть достаточно похожими, чтобы полученный в результате термин по-прежнему обладал хорошими свойствами. Здесь это означает, что его тип должен быть неопровержимым. TermC не делаю.

Вы можете осуществить:

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

и имеют

instance Monad TermI where 
    return = Var 
    bind = substI