haskell - 具有 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 中删除了这个。)类型系统是 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实例去？

Answer 1

根本不可能做到: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