首页 文章

什么是类型量词？

提问于
浏览 次
21

许多静态类型语言具有参数多态性 . 例如在C＃中，可以定义：

T Foo<T>(T x){ return x; }

在呼叫站点中，您可以：

int y = Foo<int>(3);

这些类型有时也像这样写：

Foo :: forall T. T -> T

我听过有人说"forall is like lambda-abstraction at the type level" . 所以Foo是一个函数，它接受一个类型（例如int），并产生一个值（例如int - > int类型的函数） . 许多语言推断出类型参数，因此您可以编写 Foo(3) 而不是 Foo<int>(3) .

假设我们有一个 forall T. T -> T 类型的对象 f . 我们可以用这个对象做的是首先通过写 f<Q> 传递一个类型 Q . 然后我们返回一个类型为 Q -> Q 的值 . 但是，某些 f 是无效的 . 例如 f ：

f<int> = (x => x+1)
f<T> = (x => x)

因此，如果我们"call" f<int> 然后我们返回类型为 int -> int 的值，并且通常如果我们"call" f<Q> 然后我们返回类型为 Q -> Q 的值，那么这很好 . 但是，通常会理解这个 f 不是 forall T. T -> T 类型的有效内容，因为它会根据您传递的类型执行不同的操作 . forall的想法是明确不允许这样做 . 此外，如果forall是类型级别的lambda，那么存在什么？ （即存在量化） . 由于这些原因，似乎forall和存在并不是真正的"lambda at the type level" . 但那他们是什么？我意识到这个问题很模糊，但有人可以为我清楚这一点吗？

可能的解释如下：如果我们看一下逻辑，量词和lambda是两回事 . 量化表达式的一个例子是：整数中的forall n：P（n）
因此，forall有两个部分：一组量化（例如整数）和一个谓词（例如P） . Forall可以被视为更高阶函数：整数中的forall：P（n）== forall（整数，P）
使用类型：forall :: Set <T> - >（T - > bool） - > bool
存在具有相同的类型 . Forall就像一个无限连接，其中S [n]是集合S的第n个元素：forall（S，P）= P（S [0]）∧P（S [1]）∧P（S [2]）...
存在就像一个无限的分离：存在（S，P）= P（S [0]）∨P（S [1]）∨P（S [2]）......
如果我们对类型进行类比，我们可以说∧的类型模拟是计算交集类型∩，以及计算联合类型的∨类型 . 然后我们可以定义forall并在类型上存在如下：forall（S，P）= P（S [0]）∩P（S [1]）∩P（S [2]）...
存在（S，P）= P（S [0]）∪P（S [1]）∪P（S [2]）...
因此，forall是一个无限的交集，存在是一个无限的联合 . 它们的类型是：forall，exists :: Set <T> - >（T - > Type） - > Type
例如，多态身份函数的类型 . 这里的类型是所有类型的集合， - >是函数的类型构造函数，而且=>是lambda抽象：forall（Types，t =>（t - > t））
现在是forall T型的东西：Type . T - > T是一个值，而不是从类型到值的函数 . 它是一个值，其类型是所有类型T - > T的交集，其中T范围超过所有类型 . 当我们使用这样的值时，我们不必将它应用于类型 . 相反，我们使用子类型判断：id :: forall T：Type . T - > T.
id =（x => x）

id2 = id :: int - > int
这个向下转换id的类型为int - > int . 这是有效的，因为int - > int也出现在无限交集中 . 我认为这很好用，它清楚地解释了forall是什么以及它与lambda的不同之处，但是这个模型与我在ML，F＃，C＃等语言中看到的不兼容 . 例如在F＃中你做的id <int>在int上获取标识函数，这在此模型中没有意义：id是值的函数，而不是返回值的函数的函数 .

有类型理论知识的人能否解释究竟是什么样的存在？在什么程度上“forall是lambda在类型级别”？

haskell types ocaml existential-type parametric-polymorphism

3 回答

  • 16

    让我分开回答你的问题 .

    • 由于两个原因，调用forall "a lambda at the type level"是不准确的 . 首先，它是lambda的类型，而不是lambda本身 . 其次，lambda存在于术语级别，即使它抽象了类型（类型级别的lambdas也存在，它们提供通常称为泛型类型的东西） .

    • 通用量化并不一定意味着所有实例都具有“相同的行为” . 这是一种称为“参数”的特殊属性，可能存在也可能不存在 . 普通的多态lambda演算是参数化的，因为你根本无法表达任何非参数行为 . 但是如果你添加像typecase（a.k.a . 内涵类型分析）这样的结构或者检查强制转换形式的构造，那么你就会失去参数 . 参数化意味着很好的属性，例如它允许在没有任何类型的运行时表示的情况下实现语言 . 并且它引出了非常强大的推理原则，例如， Wadler的论文“免费定理！” . 但这是一种权衡，有时你想要在类型上派遣 .

    • 存在类型本质上表示对的一对类型（所谓的见证）和一个术语，有时称为包 . 查看这些的一种常见方式是作为抽象数据类型的实现 . 这是一个简单的例子：

    pack（Int，（λx.x，λx.x））：∃T.（Int→T）×（T→Int）

    这是一个简单的ADT，其表示为Int，并且仅提供两个操作（作为嵌套元组），用于转换抽象类型T的内部和外部 . 例如，这是模块类型理论的基础 .

    • 总之，通用量化提供了客户端数据抽象，而存在类型提供了实现者端数据抽象 .

    • 作为补充说明，在所谓的lambda立方体中，forall和箭头被推广到Π型的统一概念（其中T1→T2 =Π（x：T1）.T2和∀AT=Π（A：* ）.T）并且同样存在并且可以将元组推广到Σ-类型（其中T1×T2 =Σ（x：T1）.T2和∃AT=Σ（A：） . T） . 这里，类型是"type of types" .

    回复于
  • 7

    一些评论补充了两个已经很好的答案 .

    首先，我不能说 forall 在类型级别是lambda，因为在类型级别已经存在lambda的概念，并且它与 forall 不同 . 它出现在系统F_omega中，系统F的扩展，具有类型级计算，例如，有助于解释ML模块系统（F-ing modules，作者：Andreas Rossberg，Claudio Russo和Derek Dreyer，2010） .

    在（语法）System F_omega中，您可以编写例如：

    type prod =
  lambda (a : *). lambda (b : *).
    forall (c : *). (a -> b -> c) -> c

    这是"type constructor" prod 的定义，例如 prod a b 是产品类型 (a, b) 的教会编码类型 . 如果在类型级别有计算，那么如果要确保终止类型检查，则需要控制它（否则你可以定义类型 (lambda t. t t) (lambda t. t t) . 这是通过使用"type system at the type level"或类型系统完成的. prod 将是善良 * -> * -> * . 只有类型 * 的类型可以由值居住，更高类型的类型只能在类型级别应用. lambda (c : k) . .... 是类型级抽象，不能是值的类型，并且可能存在于任何形式的 k -> ... ，而 forall (c : k) . .... 分类在某些类型 c : k 中具有多态性的值，并且必须是地面类型 * .

    其次，系统F的 forall 与Martin-Löf型理论的Pi类型之间存在重要差异 . 在系统F中，多态值在所有类型上执行相同的操作 . 作为第一个近似值，您可以说 forall a . a -> a 类型的值将（隐式）将类型 t 作为输入并返回类型 t -> t 的值 . 但这表明在这个过程中可能会发生一些计算，但实际情况并非如此 . 在道德上，当您将类型 forall a. a -> a 的值实例化为类型 t -> t 的值时，该值不会更改 . 有三种（相关）方式可以考虑它：

    • 系统F量化有类型擦除，你可以忘记类型，你仍然会知道程序的动态语义是什么 . 当我们使用ML类型推断将多态抽象和实例化隐含在我们的程序中时，如果您将“program”视为将要运行的动态对象，我们并不会真正让推理引擎“填补我们程序中的漏洞”并计算 .

    • forall a . foo 不是“为每种类型 a 生成 foo 的实例，而是”未知类型 a 中的通用的单一类型 foo “ .

    • 您可以将通用量化解释为无限连接，但是存在一个统一条件，即所有连词具有相同的结构，特别是它们的证明都是相似的 .

    相比之下，Martin-Löf类型理论中的Pi类型实际上更像是功能类型，它们采取某些东西并返回某些东西 . 这就是为什么它们不仅可以轻松地用于依赖类型，而且还依赖于术语（依赖类型）的原因之一 .

    一旦你关注那些正式理论的健全性，这就具有非常重要的意义 . 系统F是不可预测的（包括所有类型的forall量化类型量化，包括其自身），以及为什么它的观点（我们仍然可以推断一般非参数语言中的参数化），它很快破坏了底层静态推理系统的逻辑一致性 . Martin-Löf预测理论更容易证明正确并以正确的方式延伸 .

    有关System F的统一性/通用性方面的高级描述，请参阅Fruchart和Longo的97文章Carnap's remarks on Impredicative Definitions and the Genericity Theorem . 有关存在非参数构造的系统F失效的更多技术研究，请参阅Robert Harper和John Mitchell（1999）的Parametricity and variants of Girard's J operator . 最后，从语言设计的角度来看，关于如何放弃全局参数以引入非参数构造但仍能够在本地讨论参数化的描述，请参阅George Neis，Derek Dreyer和Andreas Rossberg，2011年的Non-Parametric Parametricity .

    这个讨论了“计算抽象”和“统一抽象”之间的差异已经通过表示变量 Binders 的大量工作而得以恢复 . 绑定构造感觉就像一个抽象（并且可以通过HOAS样式中的lambda抽象来建模），但是具有统一的结构，使其更像是数据骨架而不是一系列结果 . 这已经有很多讨论，例如在LF社区，Twelf中的“代表性箭头”，Licata＆Harper的工作中的“正箭头”等 .

    最近有几个人正在研究"irrelevance"的相关概念（lambda-abstractions，其结果是"does not depend"在论证上），但仍然不完全清楚这与参数多态有多密切相关 . 一个例子是Nathan Mishra-Linger和Tim Sheard的工作（例如Erasure and Polymorphism in Pure Type Systems） .

    回复于
  • 8

    如果forall是lambda ...，那么存在什么

    为什么，当然是元组！

    在Martin-Löf type theory中，您有Π类型，对应于函数/通用量化和Σ-类型，对应于元组/存在量化 .

    它们的类型与你提出的非常类似（我在这里使用Agda表示法）：

    Π : (A : Set) -> (A -> Set) -> Set
Σ : (A : Set) -> (A -> Set) -> Set

    实际上，Π是无穷乘积，Σ是无穷和 . 请注意，它们不是“交集”和“联合”，正如您所提议的那样，因为如果不另外定义类型相交的位置，则无法执行此操作 . （一种类型的值对应于另一种类型的值）

    从这两个类型构造函数中，您可以拥有所有正常，多态和依赖函数，正常和依赖元组，以及存在和普遍量化的语句：

    -- Normal function, corresponding to "Integer -> Integer" in Haskell
factorial : Π ℕ (λ _ → ℕ)

-- Polymorphic function corresponding to "forall a . a -> a"
id : Π Set (λ A -> Π A (λ _ → A))

-- A universally-quantified logical statement: all natural numbers n are equal to themselves
refl : Π ℕ (λ n → n ≡ n)


-- (Integer, Integer)
twoNats : Σ ℕ (λ _ → ℕ)

-- exists a. Show a => a
someShowable : Σ Set (λ A → Σ A (λ _ → Showable A))

-- There are prime numbers
aPrime : Σ ℕ IsPrime

    然而，这根本不涉及参数性，AFAIK参数和Martin-Löf型理论是独立的 .

    对于参数化，人们通常会参考Philip Wadler's work .

    回复于

相关问题