2022/01/04  阅读:42  主题:红绯


What is Gradual Typing


Posted on March 24, 2014[1] by jsiek[2]发表于2014年3月24日

(For a Japanese translation, go here)


Gradual typing is a type system I developed with Walid Taha in 2006 that allows parts of a program to be dynamically typed and other parts to be statically typed. The programmer controls which parts are which by either leaving out type annotations or by adding them in. This article gives a gentle introduction to gradual typing.

渐进式类型是我和 Walid Taha 在2006年开发的一种类型系统,它允许程序的某些部分被动态类型化,而其他部分则被静态类型化。程序员通过省略类型注释或添加它们来控制哪些部分是哪些部分。本文对渐进式类型作了简要介绍。

The following were our motivations for developing gradual typing:


  • Large software systems are often developed in multiple languages 大型软件系统通常是用多种语言开发的
    partly because dynamically typed languages are better for some tasks and statically typed languages are better for others. With a gradual type system, the programmer can choose between static and dynamic typing without having to switch to a different language and without having to deal with the pain of language interoperability. Hopefully this will increase programmer productivity. 部分原因是动态类型语言更适合某些任务,而静态类型语言更适合其他任务。在渐进式类型系统中,程序员可以在静态类型和动态类型之间进行选择,而不必切换到不同的语言,也不必处理语言互操作性带来的痛苦。希望这将提高程序员的工作效率
  • Several languages already have optional type annotations, but 一些语言已经有了可选的类型注释,但是
    surprisingly, there had been little formal work on what a type checker should do with the optional type annotations and what kind of guarantees the type system should provide. Languages with optional type annotations include Common LISP, Dylan, Cecil, Visual Basic.NET, Bigloo Scheme, Strongtalk. Gradual typing is meant to provide a foundation for what these languages do with their optional type annotations. There are several new languages in development that will also include optional type annotations such as Python 3k, the next version of Javascript (ECMAScript 4), and Perl 6. Hopefully our work on gradual typing will influence these languages. 令人惊讶的是,在类型检查器应该如何处理可选的类型注释以及类型系统应该提供什么样的保证方面,几乎没有正式的工作。具有可选类型注释的语言包括 Common LISP,Dylan,Cecil,Visual Basic.NET,Bigloo Scheme,Strongtalk。渐进式类型是为这些语言如何处理可选的类型注释提供基础。目前正在开发的一些新语言也将包括可选的类型注释,比如 Python 3k、下一个版本的 Javascript (ECMAScript 4)和 Perl 6。希望我们在逐步类型化方面的工作能够影响这些语言

Before describing gradual typing, let’s review dynamic and static type checking.


Dynamic type checking


A number of popular languages, especially scripting languages, are dynamically typed. Examples include Perl, Python, Javascript, Ruby, and PHP. In general, a type is something that describes a set of values that have a bunch of operations in common. For example, the type int describes the set of (usually 32 bit) numbers that support operations like addition, subtraction, etc. A type error is the application of an operation to a value of the wrong type. For example, applying concatenation to an integer would be a type error in a language where concatenation is an operation only on strings. Another example of a type error is invoking a method on an object that doesn’t implement the method, such as car.fly(). (Isn’t it a shame that flying cars have not yet hit the mainstream, and it’s well past the year 2000!) The precise definition of type error is programming language dependent. For example, one language might choose to allow concatenation of integers and another language not. In a dynamically typed language, type checking is performed during program execution, immediately before the application of each operation, to make sure that the operand type is suitable for the operation.

许多流行的语言,特别是脚本语言,都是动态类型的。例如 Perl,Python,Javascript,Ruby 和 PHP。一般来说,类型是描述一组具有一系列共同操作的值的东西。例如,int 类型描述了一组支持加减等操作的数字(通常是32位)。类型错误是将操作应用于错误类型的值。例如,在只对字符串进行串联操作的语言中,对整数应用串联将是一个类型错误。类型错误的另一个例子是对不实现该方法的对象调用方法,例如 car.fly ()。(飞行汽车还没有成为主流,而且已经过了2000年,这不是很遗憾吗?)类型错误的精确定义依赖于编程语言。例如,一种语言可以选择允许整数串联,而另一种语言不允许。在动态类型语言中,类型检查是在程序执行期间执行的,紧接在每个操作的应用程序之前,以确保操作数类型适合于该操作。

The following is an example Python program that results in a type error.

下面是一个导致类型错误的 Python 程序示例。

  def add1(x):
      return x + 1

  class A(object):

  a = A()

The output from running the above program on the standard Python
interpreter is

在标准 Python 解释器上运行上述程序的输出是

TypeError: unsupported operand type(s) for +: 'A' and ‘int'

Static type checking


There are also a number of popular statically checked languages, such as Java, C#, C and C++. In a statically checked language, some or even all type errors are caught by a type checker prior to running the program. The type checker is usually part of the compiler and is automatically run during compilation.

还有一些流行的静态检查语言,如 Java,c # ,c 和 c + + 。在静态检查语言中,在运行程序之前,类型检查器会捕获一些甚至所有类型错误。类型检查器通常是编译器的一部分,在编译期间自动运行。

Here’s the above example adapted to Java.

下面是适用于 Java 的上面的例子。

  class A {
      int add1(int x) {
	  return x + 1;
      public static void main(String args[]) {
	  A a = new A();

When you compile this class, the Java compiler prints out
the following message.

当您编译这个类时,Java 编译器将输出以下消息。

  A.java:9: add1(int) in A cannot be applied to (A)
  1 error

You may wonder, how can a type checker predict that a type error will occur when a particular program is run? The answer is that it can’t. It is impossible to build a type checker that can predict in general which programs will result in type errors and which will not. (This is equivalent to the well-known halting problem.) Instead, all type checkers make a conservative approximation of what will happen during execution and give error messages for anything that might cause a type error. For example, the Java compiler rejects the following program even though it would not actually result in a type error.

您可能想知道,类型检查器如何预测在运行特定程序时会发生类型错误?答案是不可能。一般来说,不可能构建一个能够预测哪些程序会导致类型错误,哪些不会导致类型错误的类型检查器。(这相当于众所周知的停机问题)相反,所有类型检查器对执行过程中将发生的事情做出保守的近似,并为任何可能导致类型错误的事情提供错误消息。例如,Java 编译器拒绝以下程序,即使它实际上不会导致类型错误。

  class A {
      int add1(int x) {
	  return x + 1;
      public static void main(String args[]) {
	  A a = new A();
          if (false)
              System.out.println("Hello World!");

The Java type checker does not try to figure out which branch of an if statement will be taken at runtime. Instead it conservatively assumes that either branch could be taken and therefore checks both branches.

Java 类型检查器不会尝试指出 if 语句的哪个分支将在运行时执行。相反,它保守地假设可以接受任何一个分支,因此检查这两个分支。

Comparing dynamic and static type checking


There is a religious war between people who think dynamic checking is better and people who think static type checking is better. I believe that one of the reasons why this war has gone on for so long is that both groups have good points. (They also have some not-so-good points.) Unfortunately the two groups typically don’t acknowledge the good points made by the other group as being good points. My evaluation of the points, given below, will probably annoy both the static typing fans and the dynamic typing fans. There are of course arguments to be made for or against each of the points, and the evaluation below shows where I land after considering the arguments.


  • Static type checking catches bugs earlier, thereby removing the greater cost of fixing bugs later in the development cycle or the even greater cost of a bug that occurs in the field. Good point! Fans of dynamic typing will argue that you catch even more bugs by creating a thorough test suite for your programs. Nevertheless, I believe static type checking provides a convenient and low-cost way to catch type errors.
  • 静态类型检查可以更早地捕获 bug,从而消除开发周期后期修复 bug 的更大成本,或者消除该字段中出现的 bug 的更大成本。说得好!喜欢动态类型的人会认为,通过为程序创建一个完整的测试套件,可以捕获更多的 bug。尽管如此,我相信静态类型检查提供了一种方便且低成本的方法来捕获类型错误。
  • Dynamic type checking doesn’t get in your way: you can immediately run your program without first having to change your program into a form that the type checker will accept. 动态类型检查不会妨碍您: 您可以立即运行程序,而无需首先将程序更改为类型检查器将接受的形式
    Good point! 说得好 Fans of static typing will argue that either 1) you don’t really need to change your program very much, or 2) by changing your program to fit the type checker, your program will become better structured. The reason why 1) feels true to some programmers is that the language you use changes how you think about programming and implicitly steers you towards writing programs that will type check in whatever language you are using. Also, you get so use to working around the minor annoyances of the type system that you forget that they are annoyances and instead become proud of your ability to workaround the type system. As for 2), there are situations in which the type system gets in the way of expressing code in its most clear and reusable form. The well-known 静态类型的爱好者会争辩说,要么1)你不需要太多的改变你的程序,要么2)通过改变你的程序来适应类型检查器,你的程序将变得更好的结构。对于一些程序员来说,1)感觉真实的原因是你所使用的语言改变了你对编程的看法,并且暗中引导你去编写那些无论你使用什么语言都可以输入 check 的程序。而且,你已经习惯于处理类型系统中的一些小麻烦,以至于你忘记了这些小麻烦,反而为自己在类型系统中的工作能力感到骄傲。至于2) ,在某些情况下,类型系统会妨碍以最清晰和可重用的形式表达代码。众所周知
    Expression Problem 表达问题 is a good example of this. The reason why research on type systems continues to flourish is that it is difficult to design and implement a type system that is expressive enough to enable the straightforward expression of all programs that we would like to write. 就是一个很好的例子。类型系统的研究之所以继续蓬勃发展,是因为很难设计和实现一个类型系统,这个类型系统的表达能力足以使我们想要编写的所有程序都能够直接表达
  • Static type checking enables faster execution because type checking need not be performed at runtime and because values can be stored in more efficient representations. Good point!
  • 静态类型检查支持更快的执行,因为类型检查不需要在运行时执行,而且值可以存储在更有效的表示中。说得好!
  • Dynamic type checking makes it easy to deal with situations where the type of a value depends on runtime information. Good point!
  • 动态类型检查使得处理值的类型依赖于运行时信息的情况变得容易。说得好!
  • Static typing improves modularity. 静态类型提高了模块性Good point! 说得好 For example, in a dynamic language, you can call a library subroutine incorrectly but then get a type error deep inside that routine. Static checking catches the type errors up-front, at the point where you called 例如,在动态语言中,可以不正确地调用库子例程,但是在该例程的深处会出现类型错误。静态检查可以在调用时预先捕获类型错误
    the subroutine. 子程序
  • Static type checking makes you think more seriously about your program which helps to further reduce bugs. Bad point. Type checkers only check fairly simple properties of your program. Most of the work in making sure that your program is correct, whether written in a statically or dynamically checked language, goes into developing comprehensive tests.
  • 静态类型检查使您更认真地考虑您的程序,这有助于进一步减少 bug。说得不对。类型检查器只检查程序的相当简单的属性。确保程序正确性的大部分工作,无论是用静态或动态检查语言编写的,都需要开发全面的测试。
  • With dynamic type checking, you don’t have to spend time writing type annotations. Bad point. The time it takes to write down a type annotation is rather trivial and there are programs called type inferencers that can do type checking without requiring type annotations.
  • 使用动态类型检查,您不必花时间编写类型注释。说得不对。写下一个类型注释所需的时间相当简单,而且有一些名为类型推理程序的程序可以进行类型检查,而不需要类型注释。

Because neither static or dynamic type checking is universally better than the other, it makes sense to provide the programmer a choice, without forcing them to switch programming languages. This brings us to gradual typing.


Gradual type checking


A gradual type checker is a type checker that checks, at compile-time, for type errors in some parts of a program, but not others, as directed by which parts of the program have been annotated with types. For example, our prototype gradual type checker for Python does not give an error for the above program, reproduced again below.

渐进式类型检查器是一种类型检查器,它在编译时检查程序的某些部分的类型错误,但不检查其他部分的类型错误。例如,我们用于 Python 的原型渐进类型检查器不会为上面的程序提供错误,下面再次重现。

  def add1(x):
      return x + 1

  class A:

  a = A()

However, if the programmer adds a type annotation for the parameter x,
as follows, then the type checker signals an error because the type
of variable a is A, which is inconsistent with
the type of parameter x of the add1 function,
which is int.

但是,如果程序员为参数 x 添加类型注释,如下所示,那么类型检查器将发出错误信号,因为变量 a 的类型是 a,这与 add1函数的参数 x 的类型不一致。

  def add1(x : int):
      return x + 1

  class A:

  a = A()

(Our rules for assigning static types to local variables such as a
are somewhat complicated because Python does not have local variable declarations but in most cases we give the variable the same type as the expression on the right-hand side of the assignment.)

(我们为 a 等局部变量分配静态类型的规则有些复杂,因为 Python 没有局部变量声明,但在大多数情况下,我们给变量赋予的类型与赋值右侧的表达式相同。)

The gradual type checker deals with unannotated variables by giving
them the unknown type (also called the dynamic type in the
literature), which we abbreviate as “?” and by allowing implicit conversions from any type to ? and also from ? to any other type. For simplicity, suppose the + operator expects its arguments to be integers. The following version of add1 is accepted by the gradual type checker because we allow an implicit conversion from ? (the type of x) to int (the type expected by +).

渐进类型检查器通过给未注释的变量赋予未知类型(在文献中也称为动态类型)来处理未注释的变量,我们缩写为“ ?”和允许隐式转换从任何类型?也是从哪里来的?任何其他类型。为简单起见,假设 + 运算符期望其参数为整数。下面的 add1版本被渐进类型检查器接受,因为我们允许从?(x 的类型)到 int (+ 的类型)。

  def add1(x):
      return x + 1

Allowing the implicit converson from ? to int is unsafe, and is what gives gradual typing the flavor of dynamic typing. Just as with dynamic typing, the argument bound to x will be checked at run-time to make sure it is an integer before the addition is performed.

允许隐含的对话从?是不安全的,这就是为什么逐渐类型化动态类型的原因。与动态类型一样,在运行时将检查绑定到 x 的参数,以确保它是一个整数,然后再执行添加操作。

As mentioned above, the gradual type checker also allows implicit conversions from any type to type ?. For example, the gradual type checker accepts the following call to add1 because it allows the implicit conversion from int (the type of 3) to ? (the implied type annotation for parameter x).

如上所述,渐变类型检查器还允许从任何类型到类型的隐式转换?.例如,渐进类型检查器接受对 add1的以下调用,因为它允许从 int (类型为3)隐式转换为?(参数 x 的隐含类型注释)。


The gradual type checker also allows implicit conversions between more complicated types. For example, in the following program we have a conversion between different tuple types, from ? * int to int * int.

渐变类型检查器还允许在更复杂的类型之间进行隐式转换。例如,在下面的程序中,我们有一个不同元组类型之间的转换,从?* int to int * int.

  def g(p : int * int):
    return p[0]

  def f(x, y : int):
    p = (x,y)

In general, the gradual type checker allows an implicit conversion between two types if they are consistent with each other. We use the shorthand S ~ T to express that type S is consistent with type T. Here are some of the rules that define when two types are consistent:

通常,渐进类型检查器允许两个类型之间的隐式转换,如果它们彼此一致的话。我们用简写 s ~ t 来表示 s 型与 t 型是一致的。以下是定义两种类型一致性的一些规则:

  1. For any type T, we have both ? ~ T and T ~ ?.
  2. 对于任何类型的 t,我们都有? ~ t 和 t ~ ? 。
  3. For any basic type B, such as int, we have B ~ B.
  4. 对于任何基本类型 b,例如 int,我们有 b ~ b。
  5. A tuple type 元组类型T1 * T2 is consistent with another tuple type 与另一个元组类型一致S1 * S2 中一 * 中二
    if 如果T1 ~ S1 and T2 ~ S2 2 ~ S2. This rule generalizes in a straightforward 。这条规则概括在一个简单的
    way to tuples of arbitrary size. 任意大小的元组
  6. A function type fun(T1,...,Tn,R) (the T1Tn are the parameter types and R is the return type) is consistent with another function type fun(S1,...,Sn,U) if T1 ~ S1Tn ~ Sn and R ~ U.
  7. 函数类型 fun (T1,... ,Tn,r)(T1... Tn 为参数类型,r 为返回类型)与另一个函数类型 fun (S1,... ,Sn,u)一致,如果 T1 ~ S1... Tn ~ Sn 和 r ~ u。

We write S !~ T when S is not consistent with T.

当 s 与 t 不一致时,我们写 s! ~ t。

So, for example


  • int ~ int 不,不,不,不
  • int !~ bool Int! ~ bool
  • ? ~ int
  • bool ~ ? 布尔 ~ ?
  • int * int ~ ? 你在说什么?
  • fun(?,?) ~ fun(int,int) Fun (? ,?) ~ fun (int,int)
  • ? ~ fun(int,int) Fun (int,int)
  • int * int !~ ? * bool Int! !

Why subtyping alone does not work


Gradual typing allows an implicit cast from any type to ?, similar to object-oriented type systems where Object is the top of the subtype lattice. However, gradual typing differs in that it also allows implicit casts from ? to any other type. This is the distinguishing feature of gradual typing and is what gives it the flavor of dynamic typing. Previous attempts at mixing static and dynamic typing, such as Thatte’s Quasi-static Typing, tried to use subtyping but had to deal with the following problem. If the dynamic type is treated as both the top and the bottom of the subtype lattice (allowing both implicit up-casts and down-casts), then the lattice collapses to one point because subtyping is transitive. In other words, every type is a subtype of every other type and the type system no longer rejects any program, even ones with obvious type errors.

渐进类型允许从任何类型到?类似于面向对象类型系统,其中 Object 位于子类型格的顶部。但是,渐进类型的不同之处在于,它还允许从?任何其他类型。这是渐进类型的显著特征,也是它具有动态类型特征的原因。以前混合静态类型和动态类型的尝试,如 Thatte 的准静态类型,尝试使用子类型,但必须处理以下问题。如果同时将动态类型视为子类型格的顶部和底部(允许隐式向上强制转换和向下强制转换) ,那么由于子类型是可传递的,因此该格可以折叠为一点。换句话说,每个类型都是其他类型的子类型,而且类型系统不再拒绝任何程序,即使是有明显类型错误的程序。

Consider the following program.


  def add1(x : int) -> int:
     return x + 1

Using true as an argument to the function add1 is an obvious type error but we have bool <: ? and ? <: int, so bool <: int. Thus the subtype-based type system would accept this program. Thatte partially addressed this problem by adding a post-pass, called plausibility checking, after the type checker but this still did not result in a system that catches all type errors within fully annotated code, as pointed out by Oliart. I won’t go into the details of Thatte’s plausibility checking, as it is rather complicated, but I will discuss an example. The following program has an obvious static type error which is not detected by plausibility checking.

使用 true 作为函数 add1的参数是一个明显的类型错误,但是我们有 bool < : ?然后呢?Int,so bool < : int.因此,基于子类型的类型系统将接受这个程序。Oliart 指出,在类型检查器之后添加一个 post-pass,称为似真性检查,部分解决了这个问题,但这仍然不能导致一个系统捕获全注释代码中的所有类型错误。我不会详细讨论 Thatte 的合理性检查,因为它相当复杂,但我将讨论一个例子。下面的程序有一个明显的静态类型错误,不能通过合理性检查发现。

def inc(x: number):
   return x + 1


In the application of inc to True, both inc and True can be implicitly up-cast to the dynamic type ?. Then inc is implicitly down-cast to ? -> ?. The plausibility checker looks for a greatest lower bound of number -> number and ? -> ?, which is ? -> number, so it lets this program pass without warning.

在应用 inc to True 时,inc 和 True 都可以隐式转换为动态类型? ?.那么 inc 就含蓄地向下转换为?-> ?.似真性检查器寻找数 > 数和? 的最大下界?-> ?是什么?- > 号码,所以它让这个程序通过没有警告。



10:28 am: https://wphomes.soic.indiana.edu/jsiek/what-is-gradual-typing/


View all posts by jsiek: https://wphomes.soic.indiana.edu/jsiek/author/jsiek/


2022/01/04  阅读:42  主题:红绯