是否“无类型"也意味着“动态类型"在学术 CS 世界? [英] Does "untyped" also mean "dynamically typed" in the academic CS world?

问题描述

我正在阅读一张幻灯片，上面写着JavaScript 是无类型的".这与我认为的事实相矛盾，所以我开始挖掘以尝试了解更多信息.

I'm reading a slide deck that states "JavaScript is untyped." This contradicted what I thought to be true so I started digging to try and learn more.

JavaScript 是一种无类型语言吗?的每个答案都说 JavaScript 是不是无类型的，并提供了我熟悉和满意的各种形式的静态、动态、强类型和弱类型的示例..所以那不是要走的路.

Every answer to Is JavaScript an untyped language? says that JavaScript is not untyped and offered examples of various forms of static, dynamic, strong, and weak typing that I'm familiar and happy with.. so that wasn't the way to go.

所以我问了 JavaScript 的创造者 Brendan Eich，他说:

So I asked Brendan Eich, the creator of JavaScript, and he said:

学术类型使用无类型"来表示没有静态类型".他们足够聪明，可以看到值具有类型(废话！).上下文很重要.

academic types use "untyped" to mean "no static types". they are smart enough to see that values have types (duh!). context matters.

以学术为中心的计算机科学人员是否使用无类型"作为动态类型"的同义词(这是否有效?)还是有更深层次的东西我遗漏了?我同意 Brendan 的观点，即上下文很重要，但任何对解释的引用都会很棒，因为我目前的必读"书籍并没有在这个主题上打球.

Do academically-focused computer science folks use "untyped" as a synonym of "dynamically typed" (and is this valid?) or is there something deeper to this that I am missing? I agree with Brendan that context is important but any citations of explanations would be great as my current "go to" books are not playing ball on this topic.

我想确定这一点，这样我就可以提高我的理解力，因为即使是维基百科也没有提到这种替代用法(无论如何我都能找到).如果我错了，我不想使用该术语或质疑该术语的使用:-)

I want to nail this down so I can improve my understanding and because even Wikipedia doesn't refer to this alternative usage (that I can find, anyway). I don't want to mess up with either using the term or questioning the use of the term in future if I'm wrong :-)

(我还看到一位顶级 Smalltalker 说 Smalltalk 也是无类型"的，所以这不是一次性的，这让我开始了这个任务！:-))

(I've also seen a top Smalltalker say Smalltalk is "untyped" too, so it's not a one-off which is what set me off on this quest! :-))

推荐答案

是的，这是学术文献中的标准做法.要理解它，了解类型"的概念是在 1930 年代在 lambda 演算的背景下(实际上，甚至更早，在集合论的背景下)被发明的会有所帮助.从那时起，出现了一个被称为类型理论"的计算逻辑的整个分支.编程语言理论就是建立在这些基础之上的.在所有这些数学上下文中，类型"具有特定的、公认的含义.

Yes, this is standard practice in academic literature. To understand it, it helps to know that the notion of "type" was invented in the 1930s, in the context of lambda calculus (in fact, even earlier, in the context of set theory). Since then, a whole branch of computational logic has emerged that is known as "type theory". Programming language theory is based on these foundations. And in all these mathematical contexts, "type" has a particular, well-established meaning.

术语动态类型"是在很久以后才发明的——它与类型"这个词在数学上的常见用法是矛盾的.

The terminology "dynamic typing" was invented much later -- and it is a contradiction in terms in the face of the common mathematical use of the word "type".

例如，这里是 Benjamin Pierce 在他的标准教科书中使用的类型系统"的定义类型和编程语言:

For example, here is the definition of "type system" that Benjamin Pierce uses in his standard text book Types and Programming Languages:

类型系统是一种证明不存在的易于处理的句法方法某些程序行为通过根据短语对短语进行分类他们计算的各种值.

A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.

他还说:

有时会明确添加静态"一词——我们说的是例如，静态类型编程语言"——为了区分我们在这里考虑的各种编译时分析在诸如 Scheme (Sussman和斯蒂尔，1975 年；凯尔西、克林格和里斯，1998 年；Dybvig, 1996),其中运行时类型标签用于区分不同种类的堆中的结构.像动态类型"这样的术语可以说是用词不当，可能应该替换为动态检查"，但用法是标准的.

The word "static" is sometimes added explicitly--we speak of a "statically typed programming language," for example--to distinguish the sorts of compile-time analyses we are considering here from the dynamic or latent typing found in languages such as Scheme (Sussman and Steele, 1975; Kelsey, Clinger, and Rees, 1998; Dybvig, 1996), where run-time type tags are used to distinguish different kinds of structures in the heap. Terms like "dynamically typed" are arguably misnomers and should probably be replaced by "dynamically checked," but the usage is standard.

在该领域工作的大多数人似乎都认同这一观点.

Most people working in the field seem to be sharing this point of view.

请注意，这不意味着无类型"和动态类型"是同义词.相反，后者是前者特定情况的(技术上具有误导性的)名称.

Note that this does not mean that "untyped" and "dynamically typed" are synonyms. Rather, that the latter is a (technically misleading) name for a particular case of the former.

PS:还有 FWIW，我碰巧既是类型系统的学术研究员，又是 JavaScript 的非学术实现者，所以我不得不忍受这种分裂.:)

PS: And FWIW, I happen to be both an academic researcher in type systems, and a non-academic implementer of JavaScript, so I have to live with the schisma. :)

这篇关于是否“无类型"也意味着“动态类型"在学术 CS 世界?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！