罗素悖论 类型系统与编程语言

12-03-29 banq
编程语言的基础核心来自于逻辑,来自PROGRAMMING LANGUAGES & TYPE SYSTEMS文章从罗素悖论角度解释,为什么我们引入类型系统,然后才有了今天的编程语言,这对深入理解编程语言来源,破除语言误区有很大帮助。

著名的罗素悖论是:一个集合到底包含不包含它自己?

举个例子,如下集合a包含a本身:

a = { a, b }

但是,我们常识中对树形结构的了解,一个节点(枝)是由其他节点组成的(左 右或子),但肯定不是由它自己组成的,因此我们又认为集合a不应该包含a本身:

a={任何除了a的元素}

或a={b}

我们总结下面:

1.集合包含他们自己

2.集合不包含他们自己

如果有很多集合,这些很多集合也可以表现为一个大集合,那么我们得到如下描述:

1.所有集合的集合应该包含他们自己。

2.所有集合的集合不应该包含他们自己。

从前面推论我们已经知道,我们倾向于第二条为真,但是注意第二句就发生了逻辑矛盾,如果我们需要统计不包含自己的所有集合,必须首先统计其主集合,因为主集合实际上是包含了所有集合的,但是主集合也是一种集合,而集合是不应该包含他们自己的,结果这里发生矛盾,这就是著名的罗素悖论。

解决罗素悖论是引入类型理论(http://en.wikipedia.org/wiki/Type_theory),引入不同类型的层次,每个层次结构中的层只是由同一类型中先前层次组成的。这就诞生了我们今天现代语言Java, C#, Ruby, Haskell 等等,都是采取类型理论,实现特定的属性和层次。

知道这种来历,对于理解编程语言中动态类型(Ruby)和静态类型(Java Scala)等区别很有帮助,还有一种强类型和弱类型,比如Java如下:

// Given a method:

public void increment(int i);

// This call is illegal

increment(24.0);

增加这个方法是非法的,因为24.0是一种double类型,而方法函数参数类型要求是int,Java并不知道如何将24.0转换成int类型,但是也不鼓励由Java自动实现,因为Double在Java中是64位,而int是32位,进行自动转换会丢失信息。

但是Java允许 3+24.0这种算法,这是一种类型扩展type-widening表达用法,算式的结果类型是double的,整数int能够被保护,这种转换将被允许,但是int x = 3+24.0又不允许。

在动态类型语言Python中"1"+2 结果是错误的:

TypeError: cannot concatenate 'str' and 'int' objects

告诉我们范了一个类型错误,Python并不知道如何转换这些类型,同样Ruby会报类似错误,这其实是一种强类型影响的表现,它存在在静态类型语言Java C#,也存在动态类型语言Ruby Python Scheme中。

为了纠正这种错误,我们必须显式地进行转换,如Python必须如下:

"1" + str(2) # returns '12'

或者:

int("1") + 2 # returns 3

很显然Python并不确定"+"(加号)这个操作符应当将字符转为整数型,它留给程序员解决,这是强类型系统中一个最佳实践。

在java中下面是允许的:

"1" + 2 // returns "12"

这里"+"加号操作符被认为是调用对象的.toString(),这是值得商榷的选择,但是它增强了灵活性。

在Python中,一个函数能够接受任何类型的对象:

def fun(arg):

...

这比报类型错误要更加安全,相反Java支持强制性类型:

void fun(String arg) { .. }

这是一种更加安全的方式,只接受特定类型参数。

大部分动态类型语言都假设任何对象能够被转换成String,这是一种为了方便而实现的妥协。

下面谈谈弱类型,javascript是一种弱类型语言:

"100" > 10 // returns true

和上面谈到的强类型不同的是,弱类型语言定义了一些基本约束,防止程序员射中自己的脚,这些类型的自动转换是语言的特别之处,但是每个语言也有自己在遭遇矛盾类型情况下的解决方式:

100 + "1" + 0

结果将是"10010",而在VB,将是数字101,这种转换虽然带来方便,但是也有一定随意性,这时强类型语言显示出其特有的可预测的逻辑一致性了。

结论:

强类型Ruby和java对于团队开发更加安全,而弱类型则可提供快速基于浏览器内部的开发 。

16
banq
2012-03-29 11:24
个人结论:原来所谓动态类型和静态类型其实都是强类型,动态和静态的区别只是方便出发;而javascript代表的弱类型,则类似罗素悖论中集合一样,由于模糊了类型,造成了悖论,带来了随意性,也带来不确定性,怪不得JS难以调试是其本质问题。

参考文章:dynamic-programming-languages-are-slow

增加动态类型语言的特点到静态类型语言中,增强语言编译器特性:性能评价 分析和权衡Adding Dynamically-Typed Language Support to a Statically-Typed Language Compiler: Performance Evaluation, Analysis, and Tradeoffs

[该贴被banq于2012-03-29 11:28修改过]

banq
2012-03-31 09:45
下面谈一下自己感想,可能会出错,主要是思考目前OO面向对象和面向函数语言的争论。

从类型理论角度出发创造的编程语言有两个特点:需要编译器,必须有系统设计,在系统设计确定好类型即可:Design the type system correctly, and the language will design itself.只要你正确设计系统,语言将会设计自己。

这也是大部分编程语言总是从“类”开始,任何一个对象或值都都属于一个特定的类型,这样才能回避罗素悖论。

类型理论明确规定任何实体必须有类型,这是面向对象OO基础。

面向函数语言则是从另外一个角度来思考问题:函数,函数学派典型代表是lambda calculi,导致了Lisp, ML, 和 Haskell 等语言,正如面向对象学派呼唤每个都是对象,他们认为everything is a function;每个都是函数。

这里插一段我本人对世界本质一些胡思乱想,我在早期研究EJB时,发现其分类是从有态和无态两个方面,所以,使用EJB必须搞清这两个区别,而这两个不是我们日常思维所习惯的,这也是Spring当初回避这个问题得到大部分初学者认同原因,为什么EJB要分这两点呢?要从其分布式架构原理去了解,无态侧重计算过程,也就是函数,通过失败恢复failove来保证可靠性;而有态侧重的是计算结果,是一种Value值,属于一种可变状态,其可靠性通过session复制来实现(这两种处理方式在如今流行的云计算中也是不可回避的)。从这里我隐约感觉到计算机世界中好像就像人类世界,只存在两种人男和女一样大道至简。

侧重过程或侧重结果是计算机世界中两种不同的思维角度,就像有的人侧重过程,而有的人看重结果一样,这两样是无法取舍的,都是必须的,阴阳一体而已。

回到这个类型(Type)系统和函数系统lambda calculi,很显然,这两种视角也是一种侧重过程和侧重结果的思维,如果你看着结果数值,那么一定要给它类型;如果你看中计算过程函数,那么也一定要给他套上类型,否则全部都违反罗素悖论。

lambda calculi套上类型系统称为:Church's Type Theory

有了以上宏观中立出发点,当我去理解Lambda Calculi时,就比较好理解,比如God Math/Bad Math这篇文章谈到,everything is a function; there are no values at all except for functions,一切都是函数,除了函数以外什么都没有,没有值(我前面提到侧重结果),在侧重函数的世界里,是排他的,否则它不能成为一个阴(或阳)。

对函数学派有兴趣可以去了解一下豆瓣上这篇文章读书笔记

下面提出的问题思考是:Scala这样试图集中函数和对象(阴与阳)于一体的语言是否行得通?打个不确切的比喻,将男女混合一体是否可行?为什么将之矛盾化,主要来自于CAP理论,业界折腾了那么长时间,包括EJB集群 数据库集群,后来才明白三者不可兼得,有了CAP理论,才有云计算的一个新平台。

[该贴被banq于2012-03-31 09:54修改过]

oojdon
2012-03-31 14:52
在SICP这本书中,作者也写到过类似的观点,在第三章的末尾

We began this chapter with the goal of building computational models whose structure matches our

perception of the real world we are trying to model. We can model the world as a collection of separate,

time-bound, interacting objects with state, or we can model the world as a single, timeless, stateless unity.

Each view has powerful advantages, but neither view alone is completely satisfactory. A grand unification

has yet to emerge.

译文:注意加粗部分

本章开始时提出了一个目标,构造出一些计算模型,使其结构能够符合我们对于试图去模拟的真实世界的看法,我们可以将这个世界模拟为相互分离,受时间约束具有状态的相互交流的对象,或者模拟成单一的,无时间无状态的统一体,每种观点都有强有力的优势,但是就其自身而言,又没有一种方式能够完全令人满意,我们还在等待一个大一统计算理论的诞生

oojdon
2012-03-31 14:54
不好意思,豆瓣上这篇文章读书笔记点进去就是这本书,没注意

猜你喜欢
2Go 1 2 下一页