话说王垠的那个Yin语言为什么给放弃了?

Tips:点击图片进入下一页

国内拿得出手的就只有aardio了吗


网友评论:
已经删博修仙了

为什么啊
垠神的隐退确实引人深思
德性匹下,毫无姨问。

  -
哈哈哈哈哈,居然有人真的信这个人能完成什么事情
才发现博客都删了

—— 来自 Xiaomi Redmi 3S, Android 6.0.1上的 v1.3.2.1-fix-play




—— 来自 Xiaomi Redmi 3S, Android 6.0.1上的 v1.3.2.1-fix-play
社会学家冒充码农
不是说了你们不配用

yin神目前为止有没有做什么实际的牛逼的事情或者东西?
别的不说、他几篇关于编程语言的总结还是算相当精辟的
充其量就是个摇笔杆子的而已啦
我从来没有想让Yin语言流行起来。我对程序语言的认识,其实超乎所有人的想象。我默默地看着各种新语言扯着各种幌子,不吸取历史教训,继续犯一些古老的错误,或者犯一些我根本不会犯的新错误,或者解决一些根本不需要解决的问题。这些语言缺少的不是功能,而是简单和优雅。要达到简单和优雅,必须要有品位,而品位就像一个艺术家的心,是非常难得到的。没有经过Indiana式教育的人,是几乎不可能达到这种品位的。就算Friedman培养出来的那么多学生,也极少有人可以达到我这种地步。我清楚的知道,其它语言设计者是完全没法达到我的一些精华思想的。我很希望他们设计出那样的东西,这样我就不需要亲自动手了,然而至今没有发现任何人可以做到,甚至根本没有想到。这些想法,早在多年前就已经被我在多个原型中实现过,所以具体做起来不会是问题。在我的心目中,Yin语言就像原子弹的技术。我不想搞核扩散,我并不想让所有人都得到它。我曾经觉得应该把它与全世界分享,后来我发现,你越是愿意分享,别人越是不拿你的东西当回事。我觉得这个世界不配拥有这样的语言,因为人类是那么的愚蠢,而世界对我是如此的不友好。在资本主义这种奖励贪婪人的制度下,Yin语言被所有人掌握,很可能不是在造福世界,而是一种灾难。所以即使我把Yin语言做出来了,它也只会属于少数人,我不想让这样的技术落到贪婪或者愚蠢的人手里。

作者:正义的花生
链接:http://www.jianshu.com/p/f1e4240f527f
來源:简书
著作权归作者所有。商业转载请联系作者获得授权,非商业转载请注明出处。

@刘仲敬
姨神姨鬼

----发送自 App for Android.

PySonar2
好好一个人,疯了

  -
阿西吧
您配吗?
易语言的吴涛才是真的牛吧
国内不错的语言(环境)有好几个
github上的red很不错,aardio上面有人说过了。
易名气比较大

aardio不错,但它的开发者在某些方面上太固步自封了,所以aardio才如此不为人知
这逼就是心里成熟了急着想要把自己中二期黑历史给埋了吧。
aardio才可惜。。
yin神真有自己宣称这么牛逼的话,早就造出超级智能(superintelligence)、取得决定性战略优势(decisive strategic advantage)、实现独占全球统治(singleton)、向可抵达宇宙(cosmic endowment)扩张了。

以上还只是我们凡人对技术神性的想像,yin神应该早就造出更牛逼的才对,或者yin神已经飞升(sublime)到更高维度,以致我们凡人无法观测到其神性了。
你看看他最后说的什么就知道了

一边说要开发一个语言,一边又说要享受生活

别TM扯了好吗,你看哪个做出成果的在成果出来前能享受生活的,不把自己的全部都放在实现自己的目标上,还想做出成果?怕不是小说看多了
yin神反正我不敢根他做同事。。


yin神心理状态不太稳定,自视怀才不遇的感觉,理论水平应该比较高,但是实践以及和他人合作水平就说不好了
不就是IT阿宽么

IT阿宽。。。

我觉得PySonar确实牛逼。

实践水平看起来也不差。
但与人合作的水平看起来是真不行。
目前计算机早就过了那种一个人就能独自撑起一个优秀的软件工程年代了
更何况他与他人的合作能力如此低下
做出来的东西也仅仅是优秀罢了
动态python语言做静态分析,高精度语义索引,我觉得还是有实力的,垠神还觉得这个微不足道。垠神早期的博客给了我不少启发,我也因此学习了scheme和sml。至于yin语言…我觉得要设计出多范式满足工业需求最后一定会像c++或者rust一样非常复杂,语义歧义非常多,过度设计严重。而且我觉得按照垠神的审美,racket就非常接近于理想了。

  -


垠神早就说过了,他钦定的是 typed racket!垠粉失格,仔细研读,请!

说正经的哈,个人还是很喜欢typed racket,erlang,typescript这种类型标记风格的
垠神博客都没了,无法研究了

  -

确实,其实我记得有几篇在任何一个镜像里都没有备份的,好像是讲类型系统的。记不清了。

剩下的好多扯皮。。。无语
垠神有价值的文章,我都看过了。我还拜读了垠神老师的作品,感觉身为程序员而不是pl研究者完全足够了。
垠神博客9成都是牢骚,废话。剩下一成是有价值的

  -
阿宽绝了

  -

是不是他回应知乎彭飞喷他pysonar的那两篇?

http://www.jianshu.com/p/529b21edd418?nomobile=yes

—— 来自 smartisan OD103, Android 7.1.1上的 v1.3.3
哪里有pysonar2的代码呢?想存一份看看


这篇?可惜找不到视频了,真想看看……

唔,找到了 pdf,第二个链接讲的是 Y combinator 的推导过程。
http://download.csdn.net/download/naturemickey/7115833

http://www.slideshare.net/yinwang0/reinventing-the-ycombinator







Hindley-Milner 类型系统的根本性错误

之前的一个时间,我曾经公开过这样一段幻灯片,它是2012年10月的时候,我在 Indiana 大学做的最后一次演讲。由于当时的委婉,我并没有直接说出这些结论的重要性:其实这是一个可以置 ML 和 Haskell 这样的语言于死地的结论。然而现在我发现,委婉其实是一种错误的态度。对待错误的东西,就是应该直截了当,一针见血。否则错误就得以机会蔓延,以至于威胁到正确的想法的生存。

这里问题的关键就在于,ML 和 Haskell 所使用的 Hindley-Milner 类型系统(HM 系统),其实含有一个根本性的,不可救药的错误。这个错误来源于逻辑学家们对于“全称量词”(universal quantifier,通常写作?)的本质的误解。在 HM 系统里面,多态(polymorphic)的函数能够被推导为含有全称量词的类型,比如 \x->x 的类型被推导为 ?a.a->a,但 HM 系统决定这个全称量词的位置的方式,却是完全没有原则的。这就导致了类型变量(type variable)的作用域(scope)的偏差。

我的研究显示,这个错误来源于 HM 系统最初的一项重要的设计,叫做 let-polymorphism。如果右边的函数是一个多态的函数,比如:

let f = \x->x in

...

let-polymorphism 总是会把全称量词的位置确定在 let 的“=”右边。然而这是一个非常错误的做法,它的错误程度近似于早期的 Lisp 所采用的 dynamic scoping。这样做的结果是,全称量词的位置会随着程序的“格式”,而不是程序的“结构”,而变化。至于什么是 dynamic scoping,你可以参考我的这篇博文。

为了弥补这个错误,30多年来,许多的人发表了许多的论文,提出了很多的“改进措施”,比如 value restriction,MLF,等等。但是我的研究却显示,所有这些“改进措施”都是丑陋的 hack。因为他们没有看到问题的根源,所以他们的方案往往只对一些特殊情况起作用。而如果你看到了问题的根源,就会发现这个错误是根本无法弥补的,因为它触及了 HM 系统的根基。为了根治这个问题,let-polymorphism 必须被去除掉。

我为此提出了自己的解决方案:在 lambda 的位置进行“generalization”,也就是说把 ? 放在 lambda 的位置,而不是 let。这样一来 let-polymorphism 就不存在了。但是这样一来,HM 系统就不再是 HM 系统,因为它的“模块化类型推导”的性质,就会名存实亡。由于类型里面含有程序的“控制结构”,这个类型系统表面上看起来是在进行“模块化类型检查”,而本质上是在做一个“跨过程静态检查”(interprocedual static analysis)。也就是说,模块化的类型推导,在 HM 这样的没有“类型标记”的体系下,其实是不可能实现的。

为了达到高效的模块化类型检查,却又允许多态函数的存在,我们终究会需要在函数的参数位置手工写上类型,这样我们就完全的丧失了 HM 系统设计的初衷。

这就是我半个学期的研究所得到的结果。很可惜的是,当我对我的导师以及 Indiana 大学的某些顶尖的逻辑学家们指出这个问题的时候,他们仿佛茫然不知我在说什么,他们甚至匆忙的试图否认这个结论的价值。我惊讶的看见了这些人头脑里的愚昧,官僚和恐惧。我不明白为什么这么明显的事情,他们却可以视而不见。这就是为什么我决定抛弃我的 PhD,因为我决定取消这些人对我的工作做出评价的资格。我也不再在乎任何其他大学的 PhD,管它是 CMU,Berkeley,Stanford 还是 Cambridge。






关于类型推导的幻灯片

今天下午在 IU 做了一个讲座,关于类型推导(type inference)。现在把幻灯片的视频贴在这里。不敢说能让没有一定基础的人看懂,但是我确实放进了很多基本的直觉。这些都是用动画效果演示出来的。我没有想到做一个幻灯片会如此好玩。希望以后多做一些。

视频是用 Keynote 转化而来的 MOV。这里也提供一个 PDF 版本(37MB)。基本的分步显示效果都还在,可是很多动画效果,比如物体的移动,电火花,火焰之类的全都没了。

下面是这个讲座的内容简介:

在这个讲座里,我指出一个简单而统一的思维方式来解释和设计类型推导系统,从最简单的到最复杂的。这些系统包括:

Hindley-Milner 系统(“HM 系统”,ML 和 Haskell 所用)

MLF 和它的竞争者们 (一种比 HM 系统更强大的系统)

Intersection type 系统

Polar type system 和 bidirectional type checking

我试图回答以下这些问题:

设计一个类型系统所需要的主要直觉有哪些?

ML 和 Haskell 所用的 Hindley-Milner 系统所提供的 "let-polymorphism" 有一个重要的问题。如何解决这个问题,而不增加程序员理解的负担?

为什么比 Hindley-Milner 系统更强大的类型系统(MLF,intersection types)很少在实际的语言中用到?

为什么类型系统的“表达力”跟它的“效率”总是成反比的?如何从中找到一个平衡点?


惊闻有人还在念叨根神,深感欣慰.......
不过严肃点说,他写的养猫文章还是不错的,加湿器的评价也不错,因此我回避了雾化器的坑,选了蒸发型。
yinwang怀才不遇太久了,八成已经疯特了。
yin神什么时候何德何能能担起我国pl的门面了,笑

其实这年头造个编程语言是真简单,bat里面要是有老大提供升职机会,不肖半年就能冒出几打对着llvm撸的所谓语言出来。但是,推诚布公的说,在体系结构本身没有大的突破的前提下,已经没有制造大包大揽的通用语言的需求了,这个市场已经饱和了。向rust那样针对安全性入手的语言是个不错的切入点,但是人家同时追求零耗损抽象,这硬骨头都啃了快10年了,都没拿下来。剩下的无非按照需求造一些dsl,都是一些小菜,现成的工具都用不完,根本不用造轮子。

垠神最大的悲剧就是他学了屠龙之际,别人跟他说龙不存在,他满地打滚然后喷人傻逼。

真是看不穿哦
吹了几年pysonar怎么还在吹
博客上有些科普确实算有料, 但你仔细去看, 基本就是对现有技术的不满也没啥解决方案
讲真, 真有料直接发顶会paper了还犯得着在博客唠叨么

http://github.com/yinwang0/pysonar2

笑了,怎么把license改成apache 2.0了?不是说死活不能让开源把自己的钱给赚了么,继续用AGPL啊,2333