我最近完成了一门大学课程，其中使用了Haskell和Agda（一种依赖类型的函数式编程语言），我想知道是否能用组合逻辑替换这些语言中的λ演算。对于Haskell而言，使用S和K组合子似乎是可行的，从而使其成为无点风格。我想知道在Agda中的等效方法是什么。也就是说，是否可以构建一个不使用任何变量的依赖型函数式编程语言，相当于Agda?
此外，是否可能通过组合子来替换量词？我不知道这是否巧合，例如，普遍量化使类型签名看起来像λ表达式。有没有一种方法可以从类型签名中删除普遍量化而不改变其含义？例如:
forall a : Int -> a < 0 -> a + a < a
是否可以不使用forall来表达同样的意思？
Set:Set系统在组合样式中进行编码的第一次尝试。这不是一个好的完成方式，但它是最容易入手的地方。这种类型理论的语法只是带有类型注释、Pi类型和一个宇宙集合的λ演算。
Set的新变量来从空白构建上下文。 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
（x：S） -> T变成了Pi S \ x:S -> T。（\ x -> t）s这样的beta-redex，因为您无法从整体的类型中猜测部分的类型。我建议现代设计师检查类型并从语法中排除beta-redexes。）Set:Set允许编码各种“说谎者悖论”。当Martin-Löf提出这个理论时，Girard向他发送了自己不一致的System U中的编码。Hurkens由于随后的悖论是我们所知道的最毒瘤的构造。）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 :.
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)
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 只是集合构造函数，因此，写出未翻译的类型，并允许使用“Agda符号”表示 Pi，我们应该有：
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 的组合表示！S 的 G、A 和 B 参数，同样对于 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的方法。首先，我定义了一类用于变量的Finite集合。每个这样的集合都有一个将其嵌入到上面集合的构造函数保存的embbedding，以及一个新的top元素，并且您可以通过embd功能区分它们：如果某个值在emb的图像中，则embd函数会告诉您。
class Fin x where
top :: Su x
emb :: x -> Su x
embd :: Su x -> Maybe x
当然，我们可以为Ze和Suc实例化Fin
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
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表示的位移。为什么要自己养狗还要亲自去叫呢？
F组合器，这张图片会如何变化？ F的行为取决于其第一个参数：如果A是原子，M和N是术语，PQ是复合，则FAMN-> M和F（PQ）MN-> NPQ。 这不能在SK（I）演算中表示，但可以将K表示为FF。 是否可以使用此扩展您的无点MLTT？ - kram1032(A：Set)→(a：A)→A 的术语 λ(A:Set)→λ(a:A)→a 被翻译为 S(S(KS)(KK))(KK)，它不能在第二个参数的类型取决于第一个参数的类型时使用。 - Anders Kaseorg