带有Bound的互相递归语法

Question

这是一个依赖类型的lambda演算的语法.

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中解除了这个.)类型系统是双向的,将术语分为可以从打字上下文推断出类型的术语,以及只能根据目标类型进行检查的术语.这在依赖类型系统中很有用,因为通常lambda术语没有主体类型.

无论如何,我一直试图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实例最后一行的漏洞,我需要一些类型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