雾雨魔法店

上一篇 LdBeth：NuPRL 中的证明{x:N|2<x<3}–virtual evidence Constructive proof assistant 有个需求， 千里冰封 你懂吗：dependent type 下的类型推导 (meta variables) 比如 Agda 中 id' : forall (x : Prop) -> x -> x id' _ x = x 的第一个参数是不参与计算的，就可以写成 implicit argument id : forall {x : Prop} -> x -> x id x = x 在用了 implicit argument 以后，id 就是个 polymorphic function。 NuPRL 是如何实现这样的功能的呢。众所周知 universal qualification 是用 dependent function type (Pi type) 实现的。 $\forall x:\mathbb{P}. P(x) == \prod_{x:\mathbb{P}}{P(x)}$...

上一篇 LdBeth：NuPRL 中的证明 (二) – 我从来不写递归的 这篇的主要內容是 Virtual Evidence: A Constructive Semantics for Classical Logics 和 Constructive Reading of Classical Logic 的导读。 也算是第一次展示了下 NuRPL 中的证明，順帯引入 squash type 的概念。 MLTT Agda 中要获得 LEM 得 posutulate （防止你们说 CubicalTT）。众所周知这样 p 出来的 LEM 虽然和 MLTT 相容，但还是沒有 computational meaning 的，这样的 classical logic 是沒有灵魂的。 那 NuPRL 是怎么解決这个的呢？ Recall, refinment type OR subtyping in NuPRL $\{x:A\ |\ P(x) \}$ it is easy to get non dependent form...

图文无关。 上一篇文章 LdBeth：NuPRL 中的证明–从一到CTT 上一篇讲了 CTT 中的一些类型。dependent function, dependent product, dependent record, universe 这些因为和 ITT 的沒什么区別，就默认读者已经会了。CTT 特色的 dependent intersection 和 dependent union 因为应用范围超出了基础，就先不讲了。 General Recursion considered K Also, in some other type systems, general recursion is not expressible, and such structural recursion operations must be built in. 在 Agda 中，众所周知是用写程序來证明的，tc 过了相当于证明过了。然而 NuPRL 因为 undecidable type checking 的性质，除了程序以外，证明还包括了 tc。 比如吧，在 Agda 里要证 $x\leq x!$ ，就要先写 ! (factorial) 的定义，写完了以后，在使用 factorial 的定义之前，还要做两件事: 给它一个能过 tc 的类型声明，并且证明 termination。...

本文假设读者已经装了 NuPRL5 的 VM/要到了帳號并照著 http://nuprl.org/html/02cucs-NuprlManual-02overview.pdf 做基操。 这是向略懂 dependent type 的人的 NuPRL 教程，介紹这一最神/传奇的定理证明器。你不需要会 Haskell，但是至少要能理解 untyped lambda calculus，最好会点 OCaml/SML，最理想是 LCF ML，因为这是 NuPRL 的 Tactic 语言，而且它沒正式的 language report。Lisp 麻，会用 Emacs 程度就可以了，在 NuPRL 里几本用不上。 这文章只能向有 Agda/Coq/HOL/PVS/Metamath 经验的介绍下 NuPRL 了，因为完全 normie 的话像我一样出见 NuPRL 怕是不太可能有过了。 Equality in CTT 我们先来看 equivalence。不好意思让你们失望了，NuPRL 里沒有 ADT。所以 NuPRL 的 $a = b \in T$ 是个 primitive，如果 a 和 b 不等就是个空集，相等则有唯一成员 $*$ ，相当于 unit type。 值得一提的是，在 Agda 用的 ITT 中，一个 value 只能和自己相等，但在 CTT，因为有 quotient type 的概念，你还可以定义一个类型使两个不同的 value 相等。...

⍝ CA 的原理很簡單，用 APL 的 primitive ⌺ (Stencil) 就可以表示 cell←{⍵⍪(⍺⍺⌺3),¯1↑⍵} ⍝ two-color ca 的映射 rule ← {⎕IO←0 ⋄ (2⊥⍵)⌷⌽(8⍴2)⊤⍺⍺} ⍝ three-color ca code ← {⎕IO←0 ⋄ (+/⍵)⌷⌽(7⍴3)⊤⍺⍺} ⍝from APL matrics to Netpbm format pgm ← {'P2'(⍕⌽⍴⍵)(⍕M),⍕¨↓⍵-⍨M←⌈/,⍵} 題图(code2040 size:1001×1001)生成方式 (⊂pgm ((2040 code)cell⍣1000) initi 500)⎕NPUT'a.pgm' ⍝ from shell $ pnmtopng a.pgm > z.png mobile automaton 就相当于两个 two-color ca。 不过我们可以先把 accumulator 给 abstract 出來。 acc ← {⍺←1 ⋄ ((⊢⍪(⍺⍺∘,¯1↑⊢))⍣⍺)⍵} ⍝ 这样之前的可以写成 (⊂pgm 1000 (2040 cell code acc) initi 500)⎕NPUT'a....

∇R←DECODE N R←2⊥N ∇ ∇R←X ENCODE N R←(X⍴2)⊤N ∇ ∇R←ENCODE32 N R←(32⍴2)⊤N ∇ ∇R←ENCODE64 N R←(64⍴2)⊤N ∇ ⍝ example ⎕←A←ENCODE64 865940890845960854 0 0 0 0 1 1 0 0 0 0 0 0 0 1 0 0 0 1 1 1 0 0 0 0 1 0 1 0 0 1 1 0 1 1 1 1 1 0 1 1 0 1 0 1 1 0 1 1 1 1 0 1 1 0 1 0 1 0 0 0 0 0 0 0 DECODE A 8....

看到一篇反映了一些多数人对 APL 的误解的 art，决定写点文章让更多人了解真正的 APL。 bhuztez：函数式-21天入门教程 在原始APL里，求平均数，通常的写法是 $avg\leftarrow \{(+\omega)\div\not\equiv \omega\}$ 我不知道原始的 APL 指的是啥，不过 direct definition (用 {} 定义匿名函数， $\alpha\ \omega$ 指代参数) 是 Dyalog 搞的，叫 D-function，后來改叫 dfns，然後其它如 GNU APL 仿了 Dyalog 的这个feature，而且这个实现的历史可沒那么早 你看，2010 年的 APLX1 都压根不支持 dfns。(APLX 是比較接近 APL2 的，不过 IBM 的 APL22 当然是最标准的，可惜我沒有 mainframe 可以用) 可以查到的是 These ideas were first presented in the Dyadic Vendor Forum at APL96 where they appeared to meet with general approval. Dfns were introduced with APL/W version 8....

最近观察到一些人跟事，有感而发。 假设你听说编程很厉害，有很多用，想学编程，但是编程有这么多不同的分支，有手机APP开发，有算法，有深度学习，有区块链，有编程语言。。。你该学什么好呢？ 很明显，因为你基本上不懂编程，所以你无法做技术上的分析，那你只能从表面上分析：越热门火爆，越缺人的东西，越适合 - 供需关系，基础经济学嘛，人才越缺，我越好找工作，工资越高，热门的方向，发paper更多人cite，做出项目也有更多star，更多人用，谁不想被更多人需要呢？ 如果这方向还比较简单，这就更好了：同等条件下，为什么要选更辛苦的工作，而不是轻轻松松攒钱？ 但是如果你真这样选，那就把自己坑了。 在说原因之前，我们先来考虑一些问题。 众所周知，技术会过时，30年前学的visual foxpro到现在价值为零，而你不希望你学的东西毫无用处，那你应该去学更不会过时的技术（半衰期更长）。而什么技术半衰期更长？ 更新迭代比较慢的技术。大版本号每上升一次/新框架推出一次，你就要重新学习一次新的API（比如啥tensorflow啥react），然后还要把旧的代码升级上去。 已经活了很久的技术。如果大公司推出了一个新平台，很可能过几年就打入冷宫，重新选个新欢（Objective C）。或者更惨的，这个方向直接凉凉（VR），你学的东西全部变废物，好不好玩？ 很不巧的是，热门的方向正好这两点都不具备。 热门的方向，自然有各大公司卖力的去推平台推框架竞争，飙版本号，生怕落后一点点就丧失掉大蛋糕。这样迭代周期一两年一单位，你要不停翻新你会的知识，君不见tensorflow2.0一出，一推叫着我不行了，不能再学的？（如何评价 TensorFlow 2.0 版本，是否是 Google 再一次力挽狂澜？） 如果一个方向活了很久，那为什么最近才变得热门？就算我们去考虑特例，比如大环境变了，突然这个方向变得可行（GPU跟大量数据导致深度学习效果很好），那以前学的东西也变得没用了 - 因为玩法变了。90年代那些链接主义NN在现代还有什么用吗？ 如果你选了个更简单的工作，那你处境更危险：本来低半衰期就导致你难以积累技术，现在再加上积累了的技术也不会带来太多竞争力，那过个五年，你不能再经常996，工资也变高了，然后跟新员工技术上拉不出差距，然后当方向慢慢变冷，竞争变激烈的时候，老板不炒你，难不成留着你过年？注意，有的工作准入门槛低，但这不等于简单 - 因为提升能力的最有效方法就是让你做刚好在能力范围外的事情。 你可能会反问‘难不成我看啥方向冷门，然后一头扎进去饿死？’ 也不是。你应该做的是去学习基本功。比如啥操作系统，算法，编程语言，体系结构这些。 这些东西都出来半世纪多了，能发掘的都发掘得差不多了，所以你能随便打开任意优质大学的公开课，然后毫无违和感的假装自己活在1990。 半世纪多的东西也不会一天突然凉凉，被打入冷宫需要重新学习。这些东西也不是一个公司能左右的 - 谁家产品这么长命？ 同时，做这些基础方向，也不代表你不能做有实际impact的工作，只能去grind 1% gain，或者直接呆象牙塔，无实际应用（不一定是坏事）- 你完全可以打好基础，然后去用这些基础做各种热门应用，这样大家都需要你，但是你的半衰期则是几十年，等你的应用方向凉凉，人老珠黄了你拔吊无情，去接着做其他的应用方向，岂不美哉？ 比如我表面上看上去是在做深度学习框架（TVM），其实天天都在写SML Compiler，一边在看Abstracting Abstract Machine打算实现下，另一边写的代码却被deploy到亚马逊，爽歪歪。 再举个反面例子：在这么多深度学习框架/算法中，有很多（我数出了五个，其中还有citation就快上万的教授的paper，不想点名，因为这是体制的问题，就lantern没问题）都自称对自动求导做出了创新，但是其实90年代的啥ADIFOR ADIC就已经覆盖了所有的所谓创新（其中还有这些新work由于缺乏自动求导常识做的负优化）。如果这些人肯耐着性子去看几十年前的自动求导书，从头翻到尾，也不至于闹这种笑话。 PS：我本来觉得这些道理本科生也都懂的，但是认识了好几个不好好打基础去学新潮东西的高中生，写上来希望对这种人有帮助。

几天前，有个人来找我，问我：‘我这语言语法设计得怎么样？’ 我连语法都没看，就问：‘你这语言的设计目的是什么？’ ‘我希望设计一个语言，融合FP跟OOP，这样我可以既有FP的表达力，也有OOP的易用性’ 我忍着吐槽的欲望，问：‘那你有继承吧？’ ‘有’ ‘那Subtyping呢？’ ‘当然也有’ ‘那你打算怎么做类型推导？’ ‘Algorithm W’ ‘你该知道，Algorithm W是靠unification做推导的，你如果有subtyping，跟Algorithm W不相容，你想好这么解了吗？’ ‘啊。。没有’ 其实如果答出来，还有很多相近的设计问题： OOP提倡extensibility，但是FP的ADT是封闭的，无法扩展新类型 - 而Class/Object无法在类型安全且不更改以前代码的前提下扩展新的method，这个语言该怎么提高扩展性？ Invariant/Covariant/Contravariant/Recursive Type/Existential Universal Quantification/Module的Subtyping怎么做？ Ad Hoc Polymorphism呢？如果靠Typeclass，这套东西怎么跟OOP的Class System整合？如果靠implicit Coherent问题怎么解决？ 这些问题不是不能解，毕竟融合FP跟OOP的语言一大推，OCaml跟Scala不说，往早说，Luca的一推paper全是这个套路，但是问题是，当你要设计语言的时候，这些东西要先考虑清楚，而不是先去考虑语法。比如说Subtyping可以看F<:跟MLSub，Extensibility可以看MLPolyR/Data a la carte/Object Algebra。 另一个我想吐槽的事情，就是‘超市买菜’模型。很多人在设计语言的时候，都会有如下的思路：‘X是好的，Y是好的，Z是好的，我也刚好都需要，所以我这个语言要有X, Y, Z。’,比如上面那个人，就认为‘FP是好的，OOP是好的，我都需要，于是我去设计语法去了’ 这样做的问题是完全没考虑到各种feature之间的互相影响-而这才是设计语言最麻烦的地方。 比如说，某个语言是Dynamically Typed的，但是有个叫Type Stability的概念：如果我能静态用Dataflow Analysis分析出类型，我就会用Type Directed Compilation做传统静态类型的优化。同时，我提供Type Annotation，所以如果分析不出来还可以手动加类型。 那好，这语言有Reference（指针），这再加上Higher Order Function，跟Dataflow Analysis很合不来，随便写点高阶的东西推不出，性能突然暴死怎么办？而Type Annotation则因为这个语言有Subtyping，同时Type Annotation选择会runtime check/convert的原因，导致没有Arrow Type，所以无法给高阶函数加Annotation，而这又恰巧是最需要的时候。。（Gradual Typing性能坑，而且他们还有Union Type，这下不止性能有问题，连做都不好做，见The root cause of blame: contracts for intersection and union types） IMO，如果设计语言，应该正好反过来：很多人都是先设计语法，然后再写实现，最后interaction管都不管听天由命的。如果是这个顺序： 先去考虑我这个语言的目的是什么（提示：如果你不是GRAIL，Scratch，APL，那答案不会是‘语法’）（提示：答案九成是‘我在设计这个领域的DSL’。） 然后去找可以实现目的的最小feature set-不可以被desugar的feature set越大，设计如上所说，越多坑，静态分析/类型推导/Partial Evaluation等操作也越难实现（要处理的case更多是一码事，不好处理的特性也是一码事（比如高阶语言不适合静态分析，指针不适合Partial Eval，Lambda Cube越往上爬越不好推类型，Subtyping更不好推等等）） 想想看自己要实现的Pass，脑袋里面建个大概的蓝图，想想要采用啥算法，看看有没有坑（要用Dataflow analysis做分析？跟高阶函数说再见吧。HM？Subtyping不相容。想在Effectful Language里面做Dead Code Elimination？你还是高阶的？好好想想Effect Analysis怎么设计吧） 如果上一步发现冲突，移除一定的Feature/Pass，看看能不能被啥弥补，或者直接不要，然后接着找冲突 好了，开始实现各种Pass吧 到了最后，才到实现Surface Language/Concrete Syntax/Parser/Pretty Printing/IDE Support这些外观上的东西的地步。 那才可以在第零时间发现这些特性/Pass interact的坑，也可以有个明确的目的，而不是看到啥好的特性，就往语言里面乱塞，最后做出一个跟C++一样复杂坑多又不好扩展的语言。

注：这跟genetic programming毫无关系。 最近，我有一个任务：我要写一个Partial Evaluator。 更具体的，这是个Simply Typed Lambda Calculus加上Reference/ADT的Partial Evaluator（PE）。Lambda Calculus上的PE很多人都做过，但是加上Reference就不好办了。我找了很多Scheme/ML的PE的paper，但是在里面，很多都对Effect闭口不提。就算提Effect，也是‘遇到Effect不做PE，跳过就好’。 没办法，我只好自己设计。凭借着我对Partial Evaluation跟Staging的理解，我弄了一个这样的设计： 0：我们先写一个Definitional Interpreter。 1：我们reify the Store。 2：我们利用MetaOCaml式的LetList写一个ANF converter。 3：我们把Definitional Interpreter的Value lift上Partially Static Domain，然后跟ANF converter‘合并’- 这样，Partially Evaluated Code会生成ANF代码，于是就没有code duplication跟capture avoidance substitution的问题。 别急，我们来一步步来看这是啥意思。 0：我们先写一个Definitional Interpreter。 type ('a, 'b) sum = Left of 'a | Right of 'b type var = Var of int type term = | Let of (var * term * term) | FromVar of var | Abs of (var * term) | App of (term * term) | Unit | Int of int | Add of (term * term) | Mult of (term * term) | IfZero of (term * term * term) | MkProd of (term * term) | Zro of term | Fst of term | MkRef of term | SetRef of (term * term) | GetRef of term | TLeft of term | TRight of term | Match of term * term * term type 'a env = int -> 'a let emptyStore _ = raise Not_found let extend e v x = function i when i == v -> x | i -> e i let genCounter () = let cnt = ref 0 in let gen () = let ret = !...