程序员经验分享-hwhale

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

2024-01-01

我最近完成了一门以 Haskell 和 Agda（一种依赖类型函数编程语言）为特色的大学课程，并且想知道是否有可能用组合逻辑代替其中的 lambda 演算。在 Haskell 中，使用 S 和 K 组合器似乎可以实现这一点，从而使其成为无点的。我想知道 Agda 的等价物是什么。即，是否可以在不使用任何变量的情况下创建一种与 Agda 等效的依赖类型函数编程语言？

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

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

不使用 forall 可以表达同样的事情吗？


于是我多想了一些，也取得了一些进展。这是对 Martin-Löf 的编码的第一次尝试，非常简单（但不一致）Set : Set组合风格的系统。这不是一个很好的结束方式，但却是最简单的开始方式。这种类型理论的语法只是带有类型注释、Pi 类型和 Universe Set 的 lambda 演算。

目标类型理论

为了完整起见，我将介绍规则。上下文有效性只是说你可以通过相邻的新变量来从空构建上下文Sets. 

                     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 上的类型注释是必要的合成抽象的类型。如果您切换到输入checking作为你的操作方式，你仍然需要注释来检查 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 and P只是设置构造函数，因此，编写未翻译的类型并允许 Pi 的“Agda 表示法”，我们应该有

U : Set
P : (A : Set) -> (B : (a : A) -> Set) -> Set

The K组合器用于提升某种类型的值A相对于其他类型的常量函数G.

  G : Set   A : Set
-------------------------------
  K : (a : A) -> (g : G) -> A

The 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 and B参数为S类似地对于K，仅从条款来看。相应地，我们可以验证打字推导从算法上来说，但我们不能像在原始系统中那样仅对组合项进行类型检查。可能有效的方法是要求类型检查器的输入带有关于 S 和 K 的使用的类型注释，从而有效地记录推导。但这是另一堆蠕虫......

如果您足够热衷于开始，那么这是一个停下来的好地方。其余的都是“幕后”的事情。

生成组合器的类型

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

我可以编写组合器的类型，对其参数进行完全抽象，如下所示。我利用我的便利pilfunction，它结合了 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)

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

de Bruijn 编码工具包

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

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

当然，我们可以实例化Fin for Ze and 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

The wk函数应该嵌入以下元素x as the largest要点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)

高阶函数不仅为您提供了代表变量的术语，还为您提供了超载在变量可见的任何范围内成为变量的正确表示的东西。也就是说，事实上我不厌其烦地区分不同的范围by type为 Haskell 类型检查器提供足够的信息来计算翻译为 de Bruijn 表示所需的移位。养狗为什么要自己狂吠呢？

本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)

Haskell

types

functionalprogramming

Logic

agda

直觉类型理论的组合逻辑等价物是什么？ 的相关文章

随机推荐

热门标签