直觉型理论的组合逻辑等价物是什么？
我最近完成了一门以Haskell和Agda（一种依赖types的函数式编程语言）为特色的大学课程，并且想知道是否可以用组合逻辑来替代这些中的lambda演算。 对于Haskell来说，使用S和K组合器似乎是可能的，从而使其不存在任何问题。 我想知道Agda的等价物是什么。 也就是说，能不能使用任何variables就可以生成一个与Agda相当的函数式编程语言？
另外，是否有可能以某种方式取代组合器的量化？ 我不知道这是否是巧合，但是例如通用量化使得types签名看起来像一个lambdaexpression式。 有没有办法从types签名中去除通用量化而不改变其含义？ 例如：
forall a : Int -> a < 0 -> a + a < a 同样的事情可以不使用forall来expression吗？
所以我想了一下，取得了一些进展。 这是Martin-Löf以一种组合风格编码的令人愉快的简单（但不一致）的Set : Set系统的第一次尝试。 这不是一个好的方法来完成，但这是最容易入门的地方。 这种types理论的语法只是带有types注释的lambda-calculus，Pitypes和一个Universe Set。
目标types理论
为了完整起见，我会提出规则。 上下文有效性只是说你可以通过邻接Set的新variables来创build空的上下文。
G |- valid G |- S : Set -------------- ----------------------------- x fresh for G . |- valid G, x:S |- valid
现在我们可以说如何在任何给定的上下文中综合术语的types，以及如何改变某些东西的types直到它所包含的术语的计算行为。
G |- valid G |- S : Set G |- T : Pi S \ x:S -> Set ------------------ --------------------------------------------- G |- Set : Set G |- Pi ST : Set G |- S : Set G, x:S |- t : T x G |- f : Pi STG |- s : S ------------------------------------ -------------------------------- G |- \ x:S -> t : Pi STG |- fs : T s G |- valid G |- s : SG |- T : Set -------------- x:S in G ----------------------------- S ={beta} T G |- x : SG |- s : T
从原来的一个小的变化，我做了lambda唯一的绑定运算符，所以Pi的第二个参数应该是一个函数计算返回types依赖于input的方式。 按照惯例（例如，在Agda中，可惜不在Haskell中），lambda的范围尽可能地向右延伸，所以当它们是高阶运算符的最后一个参数时，通常可以将其抽象为无括号：您可以看到我做了与丕。 你的Agdatypes(x : S) -> T变成Pi S \ x:S -> T
（ Digression 。如果你希望能够综合抽象types，那么在lambda上input注释是必须的，如果你改用types检查作为你的工作方式，你仍然需要注释来检查一个beta-redex，例如(\ x -> t) s ，因为你无法从整体上猜测零件的types，所以我build议现代devise者检查types，并从句法中排除beta-redex。
（ Digression 。这个系统是不一致的，因为Set:Set允许编码各种各样的“说谎者悖论”。当Martin-Löf提出这个理论时，Girard给他发了一个在他自己的不一致的System U中的编码。 Hurkens是我们知道的最有毒的build筑。）
组合器语法和规范化
无论如何，我们有两个额外的符号，Pi和Set，所以我们也许可以用S，K和两个额外的符号来pipe理一个组合的翻译：我selectU代表宇宙，P代表产品。
现在我们可以定义无types的组合语法（带有自由variables）：
data SKUP = S | K | U | P deriving (Show, Eq) data Unty a = C SKUP | Unty a :. Unty a | V a deriving (Functor, Eq) infixl 4 :.
请注意，我已经包含a在这种语法中包含由typesa表示的自由variables的方法。 除了作为我的一个reflection（每一个值得名称的语法都是一个带有returnembeddedvariables的自由monad和>>= perfoming的替代），在转换与其绑定的术语的过程中代表中间阶段是很方便的组合forms。
这是标准化：
norm :: Unty a -> Unty a norm (f :. a) = norm f $. a norm c = c ($.) :: Unty a -> Unty a -> Unty a -- requires first arg in normal form CS :. f :. a $. g = f $. g $. (a :. g) -- S fag = fg (ag) share environment CK :. a $. g = a -- K ag = a drop environment n $. g = n :. norm g -- guarantees output in normal form infixl 4 $.
（读者的练习是为正常forms定义一个types，并强化这些操作的types。）
代表types理论
现在我们可以为我们的types理论定义一个语法。
data Tm a = Var a | Lam (Tm a) (Tm (Su a)) -- Lam is the only place where binding happens | Tm a :$ Tm a | Pi (Tm a) (Tm a) -- the second arg of Pi is a function computing a Set | Set deriving (Show, Functor) infixl 4 :$ data Ze magic :: Ze -> a magic x = x `seq` error "Tragic!" data Su a = Ze | Su a deriving (Show, Functor, Eq)
我使用贝尔加德和胡克的方式（如鸟和帕特森普及）的德Bruijn指数表示。 Suatypes比Su a有更多的元素，我们用它作为绑定下的自由variablestypes， Ze是新绑定的variables， Su x是旧自由variablesx的移位表示。
将术语翻译成组合器
而这样做，我们获取通常的翻译，基于括号抽象 。
tm :: Tm a -> Unty a tm (Var a) = V a tm (Lam _ b) = bra (tm b) tm (f :$ a) = tm f :. tm a tm (Pi ab) = CP :. tm a :. tm b tm Set = CU bra :: Unty (Su a) -> Unty a -- binds a variable, building a function bra (V Ze) = CS :. CK :. CK -- the variable itself yields the identity bra (V (Su x)) = CK :. V x -- free variables become constants bra (C c) = CK :. C c -- combinators become constant bra (f :. a) = CS :. bra f :. bra a -- S is exactly lifted application
键入组合器
翻译显示了我们使用组合器的方式，这给我们提供了关于它们的types应该是什么的一个线索。 U和P只是设置构造函数，所以，写入未翻译的types，并允许Pi的“Agda符号”，我们应该
U : Set P : (A : Set) -> (B : (a : A) -> Set) -> Set
K组合器用于将某个typesA的值提升到某个其他typesG的常数函数。
G : Set A : Set ------------------------------- K : (a : A) -> (g : G) -> A
S组合器用于将应用程序提升到所有零件可能依赖的types上。
G : Set A : (g : G) -> Set B : (g : G) -> (a : A g) -> Set ---------------------------------------------------- S : (f : (g : G) -> (a : A g) -> B ga ) -> (a : (g : G) -> A g ) -> (g : G) -> B g (ag)
如果你看看S的types，你会发现它正确地说明了types理论的情境化应用规则，所以这就是反映应用结构的合适之处。 这是它的工作！
然后，我们只适用于封闭的东西
f : Pi AB a : A -------------- fa : B a
但是有一个障碍。 我在普通types理论中写了组合型的types，而不是组合型理论。 幸运的是，我有一台机器可以进行翻译。
组合式系统
--------- U : U --------------------------------------------------------- P : PU(S(S(KP)(S(S(KP)(SKK))(S(KK)(KU))))(S(KK)(KU))) G : U A : U ----------------------------------------- K : P[A](S(S(KP)(K[G]))(S(KK)(K[A]))) G : U A : P[G](KU) B : P[G](S(S(KP)(S(K[A])(SKK)))(S(KK)(KU))) -------------------------------------------------------------------------------------- S : P(P[G](S(S(KP)(S(K[A])(SKK)))(S(S(KS)(S(S(KS)(S(KK)(K[B])))(S(KK)(SKK)))) (S(S(KS)(KK))(KK)))))(S(S(KP)(S(S(KP)(K[G]))(S(S(KS)(S(KK)(K[A]))) (S(S(KS)(KK))(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KP)))(S(KK)(K[G])))) (S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS))) (S(S(KS)(S(KK)(KK)))(S(KK)(K[B])))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK)))) (S(KK)(KK))))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK))) (S(S(KS)(KK))(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK))))(S(KK)(KK))))))) M : AB : U ----------------- A ={norm} B M : B
所以你有它，在它所有的不可读的荣耀：一套组合的介绍Set:Set ！
还有一点问题。 系统的语法不能为S猜测G ， A和B参数，对于K也是如此。 相应地，我们可以通过algorithmvalidation打字派生 ，但是我们不能像原始系统那样仅仅检验组合项。 可能的工作是要求types检查者的input对S和K的使用进行types注释，有效地logging派生。 但那是另一种蠕虫
如果你足够敏锐，那么这是一个停下来的好地方。 其余的是“幕后”的东西。
生成组合器的types
我使用相关types理论术语中的括号抽象翻译生成了这些组合types。 为了说明我是如何做到的，并且使这个post不完全没有意义，让我提供我的设备。
我可以编写组合器的types，完全抽象其参数，如下所示。 我使用了便捷的pil函数，它结合了Pi和lambda来避免重复域types，而且有助于我使用Haskell的函数空间来绑定variables。 也许你几乎可以阅读以下内容！
pTy :: Tm a pTy = fmap magic $ pil Set $ \ _A -> pil (pil _A $ \ _ -> Set) $ \ _B -> Set kTy :: Tm a kTy = fmap magic $ pil Set $ \ _G -> pil Set $ \ _A -> pil _A $ \ a -> pil _G $ \ g -> _A sTy :: Tm a sTy = fmap magic $ pil Set $ \ _G -> pil (pil _G $ \ g -> Set) $ \ _A -> pil (pil _G $ \ g -> pil (_A :$ g) $ \ _ -> Set) $ \ _B -> pil (pil _G $ \ g -> pil (_A :$ g) $ \ a -> _B :$ g :$ a) $ \ f -> pil (pil _G $ \ g -> _A :$ g) $ \ a -> pil _G $ \ g -> _B :$ g :$ (a :$ g)
有了这些定义，我提取了相关的开放子项，并通过翻译运行。
德Bruijn编码工具包
以下是如何build立pil 。 首先，我定义了一类Fin ite集，用于variables。 每个这样的集合都有一个构造函数保存到上面的集合中，再加上一个新的top元素，你可以把它们区分开来： embd函数告诉你一个值是否在emb的图像中。
class Fin x where top :: Su x emb :: x -> Su x embd :: Su x -> Maybe x
当然，我们可以将Fin for Ze和Suc实例化
instance Fin Ze where top = Ze -- Ze is the only, so the highest emb = magic embd _ = Nothing -- there was nothing to embed instance Fin x => Fin (Su x) where top = Su top -- the highest is one higher emb Ze = Ze -- emb preserves Ze emb (Su x) = Su (emb x) -- and Su embd Ze = Just Ze -- Ze is definitely embedded embd (Su x) = fmap Su (embd x) -- otherwise, wait and see
现在我可以定义一个“ 弱”的操作。
class (Fin x, Fin y) => Le xy where wk :: x -> y
wk函数应该把x的元素作为y的最大元素embedded，这样y中的额外的东西就更小了，因此在de Bruijn指数术语中，更局部的绑定了。
instance Fin y => Le Ze y where wk = magic -- nothing to embed instance Le xy => Le (Su x) (Su y) where wk x = case embd x of Nothing -> top -- top maps to top Just y -> emb (wk y) -- embedded gets weakened and embedded
一旦你把这些东西整理出来，剩下的就是一个n级的skullduggery。
lam :: forall x. Tm x -> ((forall y. Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x lam sf = Lam s (f (Var (wk (Ze :: Su x)))) pil :: forall x. Tm x -> ((forall y . Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x pil sf = Pi s (lam sf)
高阶函数并不只是给你一个表示variables的术语，而是给你一个重载的东西，在variables可见的任何范围内变成variables的正确表示。 也就是说，我按照types区分不同范围的麻烦，给了Haskell types检查器足够的信息来计算de Bruijn表示的翻译所需的移位。 为什么养一只狗，吠叫自己？
我想在某些情况下，“支架抽象”也适用于依赖types。 在下面的文章的第5部分中，您会发现一些K和Stypes：
离奇但意义重大的巧合
依赖types安全的语法和评估
Conro McBride，斯特拉斯克莱德大学，2010年
将lambdaexpression式转换为组合expression式大致对应于将自然演绎certificate转换为希尔伯特样式certificate。
