Tripod-语言参考规范（草案）

FrankHB

2019-06-10 01:48:10 +08:00

@svenFeng LZ 的煋闻早就贴了。（看了大概就不会要啥 spec 了……不过题外话，我倒是强烈支持你这话拎过去跟 Rust 党说去。）
PL 的东西成熟和 LZ 的不成熟倒是没什么直接关系。LZ 这方面出的问题首先是他没找对什么“遗留问题”，而不是解决上出了问题。（但是我寻思你也同样没指出这些问题……）
另一方面，当代主流 PL 业界扯乎的幼稚设计整个也没好哪去，比如言必称 type，连 type 满足什么需求八成都没搞清楚。
在这个前提之下，sum type 算什么“自然的结构”？多糊上个 natrual transformation 是不是更自然了？
啥叫 forall 语义？跟 SFINAE 有啥关系？

@WispZhan 哪壶不开提哪壶…… C++17 以后的大多数东西，都是需求方面有大量的表面共识但设计起来各说各话，做出来的特性怕是快人人喊打了。

@trait 2young。你一开始的截图里是如果按现有的语言习用的术语理解，是有很明显的有低级错误的：LZ 看起来连声明和定义的区别都没搞清楚。但撇开这种设计的实例（至少有 C 和 C++）本身的流行程度，“定义”其实是非常 specific 的设计，和一般的 PL 理论并没什么关系。（ C++要定义很大程度上是为了 ODR，你能把 ODR 糊到哪家 PL 理论上去？）如果能在 spec 中另外给出“定义”之类术语的定义，也是可以说得通的，这同样和一般的 PL 并没什么关系。
可能你会觉得违反“ PL 常识”是岂有此理，但是现有工业语言还就是这样做的。例如，ISO/IEC 14882 事实上钦定 polymorphic 的外延就是指某些特定的 inclusion polymorphism，全然不顾 parameteric polymorphism 云云。还有，大坨的语言 spec 根本就没分清楚 variable 和 mutable object，但非得这样说在 spec 本身的 scope 里也说得通。
所以你引用的文献就比较匪夷所思了。更麻烦的是，还有相当严重的质量问题。跑题先不论（第一篇和啥叫 scope 有关么……），至少这坨 ppt 里的东西并不比 LZ 给的内容更严谨。
作为例子，这里首先根本就没说清楚什么叫 variable。即便是笼统地概括，也跟正式的(normative)东西差的老远。按实际影响比较广的定义（参考 ISO/IEC 2382 ），variable 是一个一大箩筐东西的四元组，其中并没有什么 type。另外，lifetime 套在 variable 上是说不大通的。为了讲 type （ checker ？）而夹带不够全面的私货，这在教学的意义上也是可耻的。（就不说氵到啥叫 typing 都没敢说了。）

trait

2019-06-10 09:38:45 +08:00

@FrankHB 我截图是作用域你跟我扯一堆什么定义声明 var lifetime，来，你跟我说说，楼主作用域给的定义什么叫做“可见”，谁可见？？？

svenFeng

2019-06-10 09:53:09 +08:00

@FrankHB forall 就是全程量词∀，forall 语义就是全程量词的语义啊，C++ template 本质是类型宏，要刷出类型再类型检查，根本不能保证 forall 语义，比如λx. (+ x x)在 rust、haskell 之类的是编译不过的，而 C++则没问题。

Sum type 很自然啊，sum/product 这两种组合数据的代数结构本来就是自然而然的啊，用 product 虽然可以表达 sum type 的逻辑，但是用起来十分费劲（比如你看看 golang ），你说的是 natural transformation 吧？ damn，不学猫论跟你们吹逼就是吃亏。

C++的遗留问题太多了，非得一个个列么。。。我回 LZ 写着写着就不想写了，浪费时间。

svenFeng

2019-06-10 09:55:54 +08:00

@FrankHB 补充一下λx. (+ x x)是将类型写为 forall a. a -> a -> a 的情况编译不过

FrankHB

2019-06-10 12:24:23 +08:00

@trait 怎么话都说不利索……

1. 你看清你截的图了？

a)“什么定义声明”就是截图里提到的内容。

b) 第一句就指出“标识符在程序文本中可见”，哪来的“谁可见”的问题？

c) 可见性(visibility) 和所谓定义之类的术语在 ALGOL-like 的工业界 spec 里还是挺流行的。这跟“什么定义声明”说白了是一个档次的常识。你如果不是习惯性看漏和装着不知道，那说明你欠缺这方面的知识基础。

2.你看清我的回复了？

什么 var lifetime 婊的是你引用文献的质量明摆着不合格。

是不是要我更明白地指出你引用文献的水准更不合格呢？

FrankHB

2019-06-10 12:25:13 +08:00

@svenFeng 你觉得拿 natural transformation 开刷我会不清楚全称量词是啥么……

（真的，我当时已经输入了“就现在这种 PL 还有资格管一个设计里有没有 universal quantification 么”，想了下嘲讽性质太强就删了。）

你的关于 forall 的说法，按我现在的理解重新表述一下：

要 implicit typing/structrual type inference，要 first-class higher-order type，要 sound 能 typecheck。

然而我的意思是：

1.不，真的不都需要 nominal typing，即使是为了 typecheck。

2.就算非要这样……都这样了，为啥不直接更具体点，比如上 System F 呢。
（ Undecidable xxxxx ……嘛，只要没洁癖非得干掉 type annotation，这实际上真的不是啥大事儿。）

“ sum/product 这两种组合数据的代数结构本来就是自然而然”这个……还行吧。
但是之前讨论的默认上下文显然是指塞到语言的内建特性里。把这两者混为一谈就很不地道了。

要我说的话，继续上面的思路：
……
哦，还得解决 metaprogramming 破事多的问题是吧。
……
（跳得有点远……）
……
嗯？我为啥需要内置 type system 呢？

当然，这跟 LZ 的设计无关。

C++ 的遗留问题罄竹难书算是普遍共识了，这个也没啥问题。像 C++ 把 class template 排除出 type 这点我深恶痛绝，不过这不是 template 本质是什么的问题。后者的问题(phasing) 比类型系统的问题更严重。

svenFeng

2019-06-10 14:09:56 +08:00

@FrankHB 🌎你说的我都赞成，但是我感觉我们在跨服聊天😣

FrankHB

2019-06-10 14:31:21 +08:00

@svenFeng LZ 也在和你们跨服聊天啊。。。。（虽然这楼里我压根还没理过。）
不开玩笑，LZ 虽然眼界不咋地口味奇特，但是已经上手的部分比这里大多数人清楚多了。虽然没自己做过的会有这种印象也不奇怪。
另一方面，眼界问题也被这个拉平了一部分。比如 LZ 经过提醒起码知道要有像模像样的 spec 了，而你张口就来要有 semantic specification，好像 LZ 提供的东西压根就不包括这些内容一样……于是，看起来是指 formal spec 了？那么，你真的清楚现实有多少语言的这部分 spec 是 formal 的么？

svenFeng

2019-06-10 15:43:54 +08:00

@FrankHB 先不管现实语言，你觉得造一个语言之前给一个 formal spec （最好用形式化证明过）不重要？比如 type system 的 type rules 以及证明需不需要？

FrankHB

2019-06-10 18:27:39 +08:00

@svenFeng 不说不重要，但是确定这点重要性本身是重要的吗？有 formal spec 的 spec 能保证在 spec 的意义上就一定质量更高呢，一定更容易实现呢，一定更不容易被误解呢，一定更直接解决当前问题呢，还是一定更容易扩展呢？
退一步讲，就算已知有必要，你用什么方式来确保 spec 内对元语言的正确使用？
这些问题实际上就是 formal spec 为什么通常不是 normative spec 的原因。

svenFeng

2019-06-10 19:39:19 +08:00

@FrankHB 从我举的 type rules 的来回答，formal spec 可以用 coq/Isabelle 来 formal proof，能保证 sound，不然靠猜想和直觉吗？写 type checker 直接按着 rules 写就好了，就是更容易实现，不会写着写着才发现幺蛾子，每一次扩展都重新加到证明了，更简单肯定说不上，起码更有底气，formal spec 起码比自然语言描述起来准确，最好给个 coq 代码就更完美了，有疑问看 proof 就行了。

Qiaogui

2019-06-11 16:59:08 +08:00

@FrankHB 大大，感谢您一直以来的支持。
我发现靠别人进行实质性的帮忙还是靠不住，我还是决定自己先动手写个编译器，有以下几个问题想咨询一下大大：
1. 对于各种形式的递归，如果编译器要将它们实现成为可以无限递归的形式（不受栈的限制），该怎么做？
2. 对于 Pascal 那种形式，可以进行内部定义以及重重嵌套定义该如何实现？
3. 该使用 LLVM、JVM CLASS、或者其它低级语言作为底层实现？
4. 如果使用 LLVM，哪些点应该重点学习？哪些可以一笔带过？因为 LLVM 的资料太大，很繁琐，而且向后兼容性也不好，FreePascal 都不推荐使用 LLVM 的编译器。
5. 可不可以翻译成其他的高级语言，类似于 C/C++，直接的 JAVA 源代码等？。

FrankHB

2019-06-11 18:07:22 +08:00

@svenFeng 我想我基本明白你的意思。不过，LZ 的名义目的一直是“通用”编程语言——所以这里有些微妙的差异——特别是考虑工程可行性的时候。
1.考虑整体工作量上的复杂度，无法指望“容易实现”。
我说的实现，当然，首先是语言自身的实现。所以你说的写（正确的） type checker 更容易这样的局部的着眼点是合理的。
但这和不使用 formal spec 的传统做法相比，这其实也只是在 QA 提升了一小部分（即便相比传统方法的提升是决定性的）；而作为代价，还明显地多出来了一部分：写验证代码。
据我所知，Coq/Isabelle 作为语言虽然有越来越往通用的方向上走的姿势，仍然还是 proof assistant 为中心，不适合直接实现 QA 以外的部分。
（题外话，其实就是 ML 系的语言都有很浓的 DSL 的味道—— pure functional 在某种意义上是注定无法“通用”到哪去的——就像汇编一样。）
所以，维护这样的语言及实现，得至少找到会同时使用非验证语言（实现语言）和验证语言的部分。
除了 IC 验证等极少数领域，这在工程上整体工作量很可能更多，几乎没有换来周知的正面效果。
2.Formal spec 的一个显著作用和预期目的是使 spec 的精确性更容易保持，尽量减小实现的偏差，而提升整个实现环境的质量。
但很遗憾，这个目的除了极端封闭的个别关键嵌入式产品（……比如月球车）外，因为依赖外部系统的关系，基本没法系统性地实现。
因为 formal spec 使用的 formal semantic methods 到目前为止能做到的最符合这个目的的做法，说白了也只是从一个 abstract model 翻译到另一个而已。
假设 formal spec 作为 source model 的描述是无 bug 的，也不能保证实现无 bug。
所以如果 target model 的实现本身不靠谱，翻译之前的 model 再保证没 bug 也挽救不了整个系统的实现质量（只能排 bug 时更容易踢皮球而已）。
举个例子，你如果用 C++当实现语言，整个系统的实现就别指望严格地靠谱了，因为 C++的 normative spec 不是 formal 的，更没有 C++实现宣称 formally verified。
使用公开的资源，你可能只能选择 C99 的一个子集然后使用 CompCert 来实现才能基本达到这种保守的目的——如果有 bug，bug 基本就是宿主环境和处理器厂商的。
然而考虑到 C 对 strict conforming program 的限制，这对实现整个的语言这种任务来讲，基本没啥意义。
3.上面还是理想情况。更直接的实际困难是，你没法指望保证写对 formal spec ……使之符合 informal 的 endorse 用的吹给用户听的设计的意图（至少对设计一个通用语言讲这是必要的，因为你没法指望它的用户具有足够 formal 脑细胞能自动领会你的设计多提供了传统设计没保证的啥）。
因为得分析确认需求，在你造得出替你思考的强 AI 前，这只能是手动的。我不觉得有谁有能力在“造一个通用语言”的目标上满足这里的人员资源。
此外，“有疑问看 proof ”也只是少数维护者才能做得到的事情。在教用户理解如何使用时，还多出来一遍切换 normative formal 和 informal spec 的工作量，这也是人肉的，也可能出错。
如果这个 formal spec 要 publish，我好像也没看到有谁能直接印 Coq 代码上去就算数了……
其实我觉得如果能印 Coq 代码上去大概还是进步的。我不清楚确切理由（也许是灌水的惯性问题），但是现状是，这方面业界人士似乎都喜欢在明显不适合的地方继续滥用 subsequent calculus 之类的东西。
当然，informal spec 这里也不省心。但是讽刺的是，因为后者不要求那么 formal 到必须通过 verfication，反而是更能“容错”的——不少 spec 的 bug 甚至可以延后解决，而不影响实现的进度。
4.非工程的意义上，如果你想写得整体上让人能看得懂，这样做还有摆脱不了 meta language 不够 formal 的问题——以至于不得不妥协，很难整个 formal 到底。
具体来讲，上面的依赖外部系统换成 spec 本身——项目会有外部 spec 依赖。
比如你能拿 Coq 代码当 formal spec，那么你如何判断 Coq 代码作为工具来说是保证能正确表达你的意思的？是不是还要引用 Coq 的 reference ？或者更极端点，直接把用到的部分包含进来？
然而上面说了，Coq 本身仍然相当地 DSL。在通用语言的 spec 里包含 DSL 的 spec，即便这部分只作为 meta language，我觉得仍然是十足的迷惑行为。
（虽然 Robin Milner 等看起来不那么想，实际上还把 ML 剁成一坨坨分开讲，似乎还很能彰显 ML=metalanguage 的样子——但是他们自己在 spec 用的 denotational 的东西和英语显然很不够 ML ……）
5.暂时忘掉上面所有的麻烦，还有个扩展的问题：spec 如何被用户复用以得到一个派生的语言？
如果 spec 的形式是 proof 堆出来的，那么要么这个派生的语言是 spec 规定的严格的保守扩展，要么就得几乎一个个重新（人肉）检视所有 proof 是否仍然能够符合新的需要。
一类具体的实例是本体论扩展问题。通常意义的 formal spec 中，基本只能使用 closed world assumption （除非你开洞允许用户覆盖 type system 相关的 rule，但都这样了，写死在 spec 里还有啥意义……），而真正意义上的通用语言要求 open world assumption。
你如何设计你的 type 以允许扩展加入新的 disjointed type universe 且确保原有的 typing/typechecking rule 仍能 consistent 且有意义？
当然，可以限制被扩展的语言只能作为 meta language 来彻底回避这个问题，但这又让通用打折扣了。