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

Question

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

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

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

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

Answer 1

所以我想了一下,并取得了一些进展.这是对Martin-Löf Set : Set以组合方式编写令人愉快的简单(但不一致)系统的第一次尝试.这不是一个很好的完成方式,但它是最容易上手的地方.这种类型理论的语法只是带有类型注释,Pi类型和Universe集的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成为唯一的绑定运算符,因此Pi的第二个参数应该是计算返回类型依赖于输入的方式的函数.按照惯例(例如在Agda中,但遗憾的是不在Haskell中),lambda的范围尽可能向右延伸,因此当它们是高阶运算符的最后一个参数时,您通常可以将抽象放在未被括号内:您可以看到我做了用Pi.你的Agda类型(x : S) -> T变成了Pi S \ x:S -> T.

(题外话.类型上拉姆达注解是,如果你希望能够在必要合成抽象的类型.如果切换到输入检查作为你的手法,你仍然需要注释,以检查β-归约样(\ x -> t) s,你有没有办法从整体上猜测部件的类型.我建议现代设计师检查类型并从语法中排除beta-redexes.)

(Digression.这个系统是不一致的,因为Set:Set允许编码各种"骗子悖论".当Martin-Löf提出这个理论时,Girard在他自己不一致的系统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嵌入变量和>>=执行替换的自由monad ),在转换绑定到其组合形式的术语的过程中代表中间阶段会很方便.

这是标准化:

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方式的de Bruijn索引表示(由Bird和Paterson推广).该类型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)

通过这些定义,我提取了相关的开放子项并通过翻译运行它们.

一个de Bruijn编码工具包

这是如何构建pil.首先,我定义了一类Fin用于变量的迭代集.每个这样的集都有一个构造函数保留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

现在我可以通过减弱操作来定义less-or-equals .

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表示所需的移位.为什么养狗和自己吠？

Answer 2

我想"Bracket Abstraction"在某些情况下也适用于依赖类型.在下面的论文的第5部分中,您可以找到一些K和S类型:

令人愤慨但有意义的巧合
相依类型安全的语法和评估
Conor McBride,斯特拉斯克莱德大学,2010

将lambda表达式转换为组合表达式大致对应于将自然演绎证明转换为Hilbert样式证明.