我最近完成了一门以 Haskell 和 Agda（一种依赖类型的函数式编程语言）为特色的大学课程，并且想知道是否可以用组合逻辑替换其中的 lambda 演算。使用 Haskell 似乎可以使用 S 和 K 组合器，从而使其无点。我想知道 Agda 的等价物是什么。即，可以在不使用任何变量的情况下制作一种与 Agda 等效的依赖类型函数式编程语言吗？
此外，是否有可能以某种方式用组合器代替量化？我不知道这是否是巧合，但通用量化例如使类型签名看起来像一个 lambda 表达式。有没有办法从类型签名中删除通用量化而不改变其含义？例如在：
forall a : Int -> a < 0 -> a + a < a
不使用 forall 可以表达同样的事情吗？
所以我想了更多，并取得了一些进展。Set : Set这是以组合风格对 Martin-Löf 令人愉快的简单（但不一致）系统进行编码的第一次尝试。这不是一个好的结束方式，但它是最容易开始的地方。这种类型论的语法只是带有类型注释、Pi 类型和全域集的 lambda 演算。
为了完整起见，我将介绍规则。上下文有效性只是说您可以通过毗邻居住Set在 s 中的新变量来从空构建上下文。
G |- valid G |- S : Set
-------------- ----------------------------- x fresh for G
. |- valid G, x:S |- valid
现在我们可以说如何在任何给定的上下文中为术语合成类型，以及如何将某物的类型更改为它包含的术语的计算行为。
G |- valid G |- S : Set G |- T : Pi S \ x:S -> Set
------------------ ---------------------------------------------
G |- Set : Set G |- Pi S T : Set
G |- S : Set G, x:S |- t : T x G |- f : Pi S T G |- s : S
------------------------------------ --------------------------------
G |- \ x:S -> t : Pi S T G |- f s : T s
G |- valid G |- s : S G |- T : Set
-------------- x:S in G ----------------------------- S ={beta} T
G |- x : S G |- s : T
在与原始版本的一个小变化中，我使 lambda 成为唯一的绑定运算符，因此 Pi 的第二个参数应该是一个函数，计算返回类型取决于输入的方式。按照惯例（例如在 Agda 中，但遗憾的是在 Haskell 中没有），lambda 的范围尽可能向右扩展，因此当抽象是高阶运算符的最后一个参数时，您通常可以不加括号：你可以看到我做到了与 Pi。您的 Agda 类型(x : S) -> T变为Pi S \ x:S -> T.
（题外话。如果您希望能够合成抽象的类型，则需要在 lambda 上进行类型注释。如果您切换到类型检查作为您的操作方式，您仍然需要注释来检查 beta-redex 之类的(\ x -> t) s，因为您没有办法从整体中猜测部分的类型。我建议现代设计师检查类型并从语法中排除 beta-redexes。）
（题外话。这个系统是不一致的，因为它Set:Set允许对各种“骗子悖论”进行编码。当 Martin-Löf 提出这个理论时，吉拉德在他自己的不一致系统 U 中向他发送了一个编码。随后由于 Hurkens 的悖论是我们所知道的最整洁的有毒结构。）
无论如何，我们有两个额外的符号，Pi 和 Set，所以我们可能会管理一个包含 S、K 和两个额外符号的组合翻译：我选择 U 代表宇宙，P 代表产品。
现在我们可以定义无类型组合语法（使用自由变量）：
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请注意，我已经包含了在此语法中包含由类型表示的自由变量的方法。除了对我来说是一种反射（每个名副其实的语法都是一个带有return嵌入变量和>>=执行替换的自由单子），它可以方便地表示转换过程中的中间阶段，并绑定到它们的组合形式。
这是标准化：
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
C S :. f :. a $. g = f $. g $. (a :. g) -- S f a g = f g (a g) share environment
C K :. a $. g = a -- K a g = a drop environment
n $. g = n :. norm g -- guarantees output in normal form
infixl 4 $.
（读者的练习是为范式定义一个类型并锐化这些操作的类型。）
我们现在可以为我们的类型理论定义一个语法。
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)
我以 Bellegarde 和 Hook 方式（由 Bird 和 Paterson 推广）使用 de Bruijn 索引表示。该类型Su a比 多一个元素a，我们将其用作绑定器下的自由变量的类型，其中Ze作为新绑定的变量并Su x作为旧自由变量的移位表示x。
完成后，我们获得了基于括号抽象的通常翻译。
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 a b) = C P :. tm a :. tm b
tm Set = C U
bra :: Unty (Su a) -> Unty a -- binds a variable, building a function
bra (V Ze) = C S :. C K :. C K -- the variable itself yields the identity
bra (V (Su x)) = C K :. V x -- free variables become constants
bra (C c) = C K :. C c -- combinators become constant
bra (f :. a) = C S :. bra f :. bra a -- S is exactly lifted application
翻译显示了我们使用组合子的方式，这为我们提供了关于它们的类型应该是什么的相当线索。U并且P只是设置构造函数，因此，编写未翻译的类型并允许 Pi 使用“Agda 表示法”，我们应该有
U : Set
P : (A : Set) -> (B : (a : A) -> Set) -> Set
K组合器用于将某种类型的值提升为某个A其他类型的常量函数G。
G : Set A : Set
-------------------------------
K : (a : A) -> (g : G) -> A
组合器用于将S应用程序提升到一个类型上，所有部分都可能依赖于该类型。
G : Set
A : (g : G) -> Set
B : (g : G) -> (a : A g) -> Set
----------------------------------------------------
S : (f : (g : G) -> (a : A g) -> B g a ) ->
(a : (g : G) -> A g ) ->
(g : G) -> B g (a g)
如果您查看 的类型S，您会发现它准确地说明了类型理论的上下文应用规则，因此这就是它适合反映应用构造的原因。这就是它的工作！
然后我们只申请封闭的东西
f : Pi A B
a : A
--------------
f a : B a
但有一个障碍。我在普通类型理论中编写了组合子的类型，而不是组合类型理论。幸运的是，我有一台可以进行翻译的机器。
---------
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 : A B : U
----------------- A ={norm} B
M : B
所以你有它，在它所有难以理解的荣耀中：一个组合表示Set:Set！
还是有点问题。系统的语法使您无法仅从术语中猜测G和A的B参数S以及类似的 。K相应地，我们可以通过算法验证类型推导，但我们不能像使用原始系统那样只对组合项进行类型检查。可能的工作是要求类型检查器的输入带有关于 S 和 K 使用的类型注释，有效地记录推导。但那是另一罐蠕虫......
如果您有足够的热情开始，这是一个停下来的好地方。其余的都是“幕后”的东西。
我使用相关类型理论术语的括号抽象翻译生成了这些组合类型。为了展示我是如何做到的，并使这篇文章不完全没有意义，让我提供我的设备。
我可以编写组合器的类型，完全抽象它们的参数，如下所示。我使用了我方便的pil函数，它结合了 Pi 和 lambda 以避免重复域类型，并且相当有帮助地允许我使用 Haskell 的函数空间来绑定变量。也许您几乎可以阅读以下内容！
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)
定义完这些后，我提取了相关的开放子术语并通过翻译运行它们。
以下是如何构建pil. 首先，我定义了一个Fin项目集类，用于变量。每个这样emb的集合在上面的集合中都有一个保留构造函数的 edding，加上一个新top元素，您可以将它们区分开来：该embd函数会告诉您一个值是否在emb.
class Fin x where
top :: Su x
emb :: x -> Su x
embd :: Su x -> Maybe x
当然，我们可以实例化FinforZe和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 x y where
wk :: x -> y
该wk函数应将 的元素嵌入x为 的最大元素y，以使 中的额外事物y更小，从而在 de Bruijn 索引项中更局部地绑定。
instance Fin y => Le Ze y where
wk = magic -- nothing to embed
instance Le x y => 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
一旦你解决了这个问题，剩下的就是一点 rank-n skullduggery。
lam :: forall x. Tm x -> ((forall y. Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x
lam s f = 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 s f = Pi s (lam s f)
高阶函数不仅给你一个表示变量的术语，它给你一个重载的东西，它在变量可见的任何范围内成为变量的正确表示。也就是说，我不厌其烦地按类型区分不同范围的事实为 Haskell 类型检查器提供了足够的信息来计算转换为 de Bruijn 表示所需的移位。为什么要养一只狗并自己吠叫？
我猜“括号抽象”在某些情况下也适用于依赖类型。在以下论文的第 5 节中，您会发现一些 K 和 S 类型：
离谱但有意义的巧合
依赖类型安全的语法和评估
Conor McBride，斯特拉斯克莱德大学，2010
将 lambda 表达式转换为组合表达式大致相当于将自然演绎证明转换为 Hilbert 样式证明。