0 简介和一个例子

我们通常把编程语言分为有类型，无类型，强类型和弱类型。

一个编程语言如果实现变量并已跟踪变量的类型并检查这些类型是否与预期匹配，则对其进行类型化，那么可以称这个语言为有类型的语言。

如果它不跟踪类型，则它是非类型化或弱类型化的语言，无类型编程语言是一种不对值施加类似类型的规则的语言。
一个值可以被视为整数、浮点数、字符串、指针等，只需简单地使用它，通常是将其作为参数传递给运算符。

比如现在有一个编程语言，它允许您将 Literal 分配给变量，但不允许您设置变量的数据类型，例如

  A4Bytes   int_var        1234560;
  A2Bytes   short_int_var   12;
  A4Bytes   float_var       9.1;

而这种编程语言还提供了不同的运算符来处理不同的数据类型，例如：

运算符用 + 将 int 添加到短 int 中。

运算符用 #+ 向 int 添加浮点数。
运算符用 = 将 int 分配给 int。
运算符用 #= 将短 int 分配给短 int。

程序员的工作是跟踪每个变量的数据类型并对其使用适当的运算符.
如果用错误的运算符添加两件事，会发生什么。如果它导致编译时错误，则该语言可能是静态类型的。
如果它抛出一个运行时错误，抱怨两者的类型错误，则该语言可能是动态类型的。
如果它没有抛出错误，只是尝试添加这两件事（可能导致乱码），则它可能是无类型未定义的行为。

通常弱类型语言如JavaScript被人视为无类型编程语言。

1 无类型和类型系统

要严格地谈论类型系统及其属性，我们需要开始通过正式处理编程语言的一些更基本的方面。
特别是，我们需要清晰、精确和使用在数学上易于处理的工具，去表达和推理程序的语法和语义。

接下来开发的工具可以处理数字和布尔值,它可以作为几个基本概念的直接工具——抽象句法、归纳定义和运行时错误的溯源、评估和建模。

为以后更强大的语言（无类型语言）详细阐述相同的lambda演算故事，我们还必须处理名称绑定和替换，以展望未来。

2 无类型的λ运算

无类型的定义和一些基本属性或纯粹的 lambda演算，
对于大多数人来说，就是底层的“计算基础”，其余部分是描述的类型系统。

在 1960 年代中期，Peter Landin 观察到，
复杂的编程语言可以通过将其表述为微小的核心的微积分来理解语言的基本机制，

以及一系列方便的派生形式，其行为通过将其翻译成 core核心（Landin 1964、1965、1966；另见 Tennent 1981）。

Landin 使用的核心语言是 lambda 演算，这是一种新发明的形式系统在 1920 年代由 Alonzo Church (1936, 1941)提出，

其中所有计算都是简化为函数定义和应用的基本操作。

跟随兰丁的洞察力，以及约翰麦卡锡(1959, 1981)的开创性工作在，lambda 演算已广泛用于编程语言特性的规范，语言设计和实现，以及类型系统的研究之中。

它的重要性源于事实上，它可以同时被视为一种简单的编程语言，其中计算可以被描述为一个数学对象关于可以证明哪些严格陈述。

λ演算是众多核心演算中的一种，被用于类似以下目的：

	米尔纳、帕罗和沃克的 pi 演算(1992, 1991) 已成为定义语义的流行核心语言，
        基于消息的并发语言，
	Abadi 和 Cardelli 的对象计算（1996）提炼了面向对象语言的核心特征。 

大多数将lambda 演算作为开发的概念和技术可以相当直接地转移到其他语言。

这里的示例是纯无类型 lambda 演算的术语λ，或用布尔值和算术运算扩展的 lambda 演算λNB。 这相关的实现是完全无类型的。

3 运算的多个变化方式

这可以通过多种方式丰富 lambda 演算。

首先，它经常方便为数字、元组等功能添加特殊的具体语法，记录等，其行为已经可以用核心语言模拟。

更有趣的是，我们可以添加更复杂的功能，例如可变引用单元或非本地的异常处理，这些功能可以在核心中建模语言使用，否则只能通过使用相当繁重的转译的方式实现。

这种扩展甚至最终导致了诸如机器学习之类的语言（Gordon、Milner 和 Wadsworth，1979；Mil ner、Tofte 和 Harper，1990；Weis、Aponte、Laville、Mauny 和 Suárez，1989；Milner、Tofte、Harper 和 MacQueen，1997 年）、Haskell（Hudak 等人，1992 年），

或相关的计划（Sussman 和 Steele，1975 年；Kelsey、Clinger 和 Rees，1998 年）。 正如我们在现在中看到，对核心语言的扩展通常也涉及对类型系统的扩展。

3 小结

本文介绍编程语言类型系统的分类。编程语言依据类型系统分为有类型、弱类型和无类型。类型系统的探讨涉及抽象语法、语义和运行时行为。

有类型语言如本文示例，变量关联特定类型并需匹配运算符。
无类型语言不强制类型，如JavaScript。无类型的λ演算是计算基础，Peter Landin和Alonzo Church的工作展示了如何用它理解编程语言。
Lambda演算可扩展以模拟数字、异常处理等复杂功能，影响了Haskell和Scheme等语言的发展。