haskell - 绑定(bind)的相互递归语法

这是依赖类型的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或多或少地将其删除了。)类型系统是bidirectional，将术语分为可以从键入上下文推断出其类型的项和只能根据目标类型进行检查的项。这在从属类型系统中很有用，因为在一般情况下，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实例生效？

最佳答案

这完全是不可能的:TermC不是monad。替代将条件代替变量。为了使之有意义，术语需要能够适合，即足够相似，以使得所得的术语仍具有良好的性质。这意味着它的类型必须是可推断的。 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