haskell - 直觉类型理论的组合逻辑等价物是什么？

Question

我最近完成了以 Haskell 和 Agda(一种依赖类型的函数式编程语言)为特色的大学类(class)，并想知道是否可以用组合逻辑替换这些中的 lambda 演算。使用 Haskell，这似乎可以使用 S 和 K 组合器，从而使其无点。我想知道 Agda 的等价物是什么。即，可以在不使用任何变量的情况下制作一种与 Agda 等效的依赖类型函数式编程语言吗？

另外，是否有可能以某种方式用组合器代替量化？我不知道这是否是巧合，但例如通用量化使类型签名看起来像 lambda 表达式。有没有办法从类型签名中删除通用量化而不改变其含义？例如。在:

forall a : Int -> a < 0 -> a + a < a

可以在不使用 forall 的情况下表达相同的东西吗？

Answer 1

所以我想了很多，并取得了一些进展。这是对 Martin-Löf 令人愉快的简单(但不一致)Set : Set 系统以组合风格进行编码的第一次尝试。这不是一个好的结束方式，但它是最容易开始的地方。这种类型理论的语法只是带有类型注释、Pi 类型和宇宙集的 lambda 演算。

目标类型理论

为了完整起见，我将介绍规则。上下文有效性只是说您可以通过连接居住在 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

在与原始版本的一个小变化中，我将 lambda 设为唯一的绑定(bind)运算符，因此 Pi 的第二个参数应该是一个计算返回类型取决于输入的方式的函数。按照惯例(例如在 Agda 中，但遗憾的是在 Haskell 中不是)，lambda 的范围尽可能向右扩展，因此当抽象是高阶运算符的最后一个参数时，您通常可以不加括号:您可以看到我做到了与Pi。您的 Agda 类型 (x : S) -> T 变为 Pi S \ x:S -> T 。

(题外话。如果您希望能够综合抽象的类型，则 lambda 上的类型注释是必要的。如果您切换到类型检查作为您的操作方式，您仍然需要注释来检查像 (\ x -> t) s 这样的 beta-redex，就像您一样无法从整体中猜测部分的类型。我建议现代设计师检查类型并从语法中排除 beta-redexes。)

(题外话。这个系统是不一致的，因为 Set:Set 允许对各种“说谎者悖论”进行编码。当 Martin-Löf 提出这个理论时，吉拉德给他发送了一个在他自己不一致的系统 U 中的编码。随后的悖论由于赫肯斯是我们所知道的最整洁的有毒建筑。)

组合器语法和规范化

无论如何，我们有两个额外的符号，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 嵌入变量和 >>= 执行替换的自由 monad)，它会很方便地表示转换带有绑定(bind)的术语过程中的中间阶段到它们的组合形式。

这是规范化:

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 多一个元素，我们将其用作绑定(bind)器下的自由变量类型，其中 Ze 作为新绑定(bind)变量， 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 的类型，您会发现它准确地说明了类型理论的上下文应用规则，因此它适合反射(reflect)应用程序结构。这就是它的工作!

然后我们只申请封闭的东西

  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 使用的类型注释，从而有效地记录推导。但这是另一 jar 蠕虫......

如果您已经足够渴望开始，这是一个停下来的好地方。其余的是“幕后”的东西。

生成组合器的类型

我使用来自相关类型理论术语的括号抽象翻译生成了这些组合类型。为了展示我是如何做到的，并使这篇文章不是完全没有意义，让我提供我的设备。

我可以编写组合子的类型，完全抽象了它们的参数，如下所示。我使用了我方便的 pil 函数，它结合了 Pi 和 lambda 以避免重复域类型，并且非常有用地允许我使用 Haskell 的函数空间来绑定(bind)变量。也许您几乎可以阅读以下内容!

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)

定义了这些之后，我提取了相关的开放子术语并通过翻译运行它们。

de Bruijn 编码工具包

这是构建 pil 的方法。首先，我定义了一个 Fin ite set 类，用于变量。每个这样的集合都有一个保留构造函数的 emb 加入上面的集合，加上一个新的 top 元素，你可以区分它们: embd 函数告诉你一个值是否在 emb 的图像中.

class Fin x where
  top :: Su x
  emb :: x -> Su x
  embd :: Su x -> Maybe x

我们当然可以为 Fin 和 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 x y where
  wk :: x -> y

wk 函数应该将 x 的元素嵌入为 y 的最大元素，以便 y 中的额外内容更小，因此在 de Bruijn 索引项中，更局部地绑定(bind)。

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 的骗局吧。

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 表示所需的转换。为什么要养一只狗然后自己吠叫？