静态类型化语言意味着什么?

让a是您应该静态类型化的图灵完整语言,让a'是您在删除类型检查时从a得到的语言(但不是类型注释,因为它们也有其他用途)。a'的接受程序将是a'的接受程序的子集。因此,特别是,a'也将是图灵完备的。

给你的翻译P从B到A(反之亦然)。它应该做什么?它可以做两件事之一:

1. 首先,它可以将b的每个程序y翻译成a的一个程序,在这种情况下,lpy总是返回true,因为a的程序是通过定义正确地输入的。

2. 其次,P可以把B的每个程序Y翻译成A的程序。在这种情况下,如果py恰好是a的程序,lpy将返回true,否则返回false。

因为第一种情况不会产生任何有趣的结果,所以让我们坚持第二种情况,这可能就是您的意思。在b的程序上定义的函数lp是否告诉我们b的程序有什么有趣的地方?我说不,因为它在p的变化下不是不变的。因为a是图灵完备的,即使在第二种情况下,p也可以被选择,这样它的图像恰好位于a中。那么lp就一直是真的。另一方面,可以选择p,以便将某些程序映射到a'中a的补码。在这种情况下,lp会为b的一些(可能全部)程序吐出false。正如您所看到的,您不会得到只依赖y的任何东西。

我也可以用下面的方式更数学地表达它:有一个C类的编程语言,它的对象是编程语言,它的变形是从一种编程语言到另一种编程语言的转换器。特别是,如果有一个同态p:x->y,y至少和x一样有表现力。在每对图灵完备语言之间,两个方向都有同态。对于c的每个对象x(即对于每种编程语言),我们都有一个相关的集合,比如x(我知道的是错误的符号),这些部分定义的函数可以由x的程序计算。然后,每个变形p:x->y都会包含集合的x->y。让我们正式地颠倒所有诱发身份x->y的变形p:x->y。我将把结果分类(用数学术语来说,是C的本地化)称为C’。现在包含a->a'是c中的一种变形。然而,它并不是在a'的自同构下保存的,也就是说,a->a'不是c'中a'的不变量。换句话说:从这个抽象的角度来看,“静态类型”属性是不可定义的,可以任意附加到语言上。

为了更清楚地说明我的观点,你也可以把c'看作是三维空间中几何图形的一类,也可以把欧几里得运动看作是形态。A'和B是两个几何图形,P和Q是欧几里得运动,把B带到A'上,反之亦然。例如,a'和b可以是两个球体。现在让我们在a'上确定一个点,它代表a'的子集。让我们称这一点为“静态类型”。我们想知道B的点是否是静态类型。所以我们取这样一个点y,通过p映射到a'并测试它是否是a上的标记点。正如人们很容易看到的,这取决于所选择的映射p,换句话说:一个球体上的标记点不被该球体的自同构(即欧几里得运动,将球体映射到自身)所保留。

如果 你可以翻译 每一个 B’(用B编写的程序)转换成一个等价的A’(如果B’是正确的,那么语言B和语言A一样享有“类型安全”(当然,从理论上讲是;-)——基本上这意味着B可以做完美的类型推断。但对于动态语言来说,这是非常有限的——例如,考虑:

if userinput() = 'bah':
    thefun(23)
else:
    thefun('gotcha')

在哪里? thefun (假设)对于int参数是类型安全的,而对于str参数则不是。现在——你怎么把这个翻译成语言? A 首先……?

另一种表达同样观点的方法是,你的问题构成了一个矛盾的证据,即:

• A不能映射到B
• 类型安全不是语言的词汇属性

或者两者兼而有之。我的直觉认为后者可能是关键:类型安全是一种元语言属性。

没有什么“可疑”的。;)

一组图灵完备语言,对于任何非平凡的语言都是类型安全的。[ 一 类型系统 T 是一个 严格的 图灵完备语言的子集。因此,在一般情况下,没有翻译人员 磷 ^{- 1} 从 乙 到 一 存在;因此,任何翻译器都不存在- 附有 类型检查器 LP ^{- 1} .

对这种说法的下意识反应可能是: 胡说!两个 一 和 乙 图灵完成了,所以我可以表达 任何 中的可计算函数 任何一个 语言! 事实上,这是正确的——你 可以 用任何一种语言表示任何可计算的函数;但是,通常,您也可以表示 多了一点 . 特别是,您可以构造表示语义定义不明确的表达式,例如那些可能很乐意尝试取字符串“foo”和“bar”的算术和的表达式(这是 丘布斯爸爸 马特利 的答案。这些表达式可能是“在”语言中 乙 但可能无法用语言表达 一 因为外延语义学是不明确的,所以没有合理的方法来翻译它们。

这是静态类型的一大优势:如果类型系统在编译时无法证明上述函数将接收任何参数,但算术加法运算符的结果定义良好的参数除外,则可以将其视为类型错误而拒绝。

请注意,虽然上面给出的示例通常用于解释静态类型系统的优点,但它可能过于温和。一般来说,静态类型系统不需要仅限于强制参数的类型正确性,而且确实可以表示 任何 可在编译时证明的程序所需的属性。例如,可以构造类型系统来强制执行释放文件系统句柄的约束。( 例如 到数据库、文件、网络套接字, 等。 )在收购的同一范围内。显然,在生命支持系统等领域,这是非常有价值的,其中 可证明的 尽可能多的系统参数的正确性是绝对必要的。如果你满足静态类型系统,你可以免费得到这些证明。

[ 一 ]我的意思是,并非所有可能的表达式都是类型良好的。

我的理解是这与编译时和运行时有关。在静态类型语言中,大多数类型检查是在编译时执行的。在动态类型语言中,其大部分类型检查是在运行时执行的。

让我反过来回答:

有两种不同类型的“动态”编程。

一种是“动态类型化”,这意味着您有某种shell,您可以通过在该shell中键入定义来编程,将其想象为Python的空闲shell。

另一种类型的动态编程,是一种更为理论化的编程。一个动态程序,是一个可以改变自己的源代码的程序。它需要一定程度的内射,通常用来改变微控制器上的程序内存。有时,为数字处理生成查找表被称为动态编程。