绑定的相互递归语法

这是一个依赖型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

（I更多或更少从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。我不能使用Ann构造函数将生成的TermC嵌入到TermI中，因为我不知道TermC的类型。

该数据类型是否与bound的模型不兼容？或者是否有一个技巧可以让Monad实例去？

来源

2016-08-20 Benjamin Hodgson

如果运行（滥用符号）'（VAR 0（VAR 1））[\ X - > X]'，你会得到'（\ x - > x）（var 1）'，它在你的类型系统中没有语法表示。请注意，本文中的两个'subst'都接收可推论的术语，并且没有'subst：TermC - > TermC - > TermC'。为了定义一个双向类型检查器，不一定要有双向类型系统，所以你可以将这些相互递归的数据类型合并成一个“Term”。 – user3237465

'bound'不支持共享数据，但（如上所述），您可以使用单个数据定义来完成类型检查。 “绑定”的索引版本可以执行相互数据（[例如]（http://lpaste.net/79582）），但它不作为发布的库存在。 –

将所有东西都放到一个数据类型中并不是没有缺点：它可以让你在没有注释的情况下编写一个'Lam'，它不应该在语法上有效。我想我可以在'Lam'构造函数（'Lam（Scope（）Term a）Type'）中需要一个类型，但是对于嵌套lambda表达式您会得到多余的注释，并且您必须支持用于注释其他项的额外构造。 –

这完全不可能：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

来源

2016-08-22 10:12:01 gallais

这种有点作品 - 你得到了“Monad”实例 - 但它最终变得丑陋。你不能使用大部分'bound'的组合器（包括'>>> =' - 你必须通过'Scope'下的'fmap'ping来实现'subst'），因为它们需要一个'Monad'实例用于'范围的第二个参数。所以你最终重新实现了大部分“绑定”。 –

绑定的相互递归语法

回答

相关问题