#TT #PLT ... Typescript 渐进类型果然爽炸，Type notation 就可以讨论 value level 的事情，随便创建类型集合，甚至可以是 ("+" | "-")[] 这种...

#PLT #TT

补充一句我现在自己的一点提纲，顺便科普下一些基本的编译原理/程序设计语言理论知识 #Learn #PLT #TT

当然，在完成 ParserKt 以及一些简单过程式语言的实现之前，我是不会涉足类型论的，因为在我看来它就是逻辑/抽象代数，而我逻辑不太好。
不喜勿喷，欢迎帮忙订正。

一般的类型论就是「给程序查错」的一种机制，类型系统制定规则，可以判断程序是否符合。符合=阴性(negative)、不符合=阳性(positive)。
基于停机问题，一个 type checker 不可能同时：
+ sound，不存假阴性
+ complete，不存假阳性
+ terminates，可以在有限时间得出结果（换句话说就是可实现）
取其轻者而废之，所以 completeness — 不会否决(positive) 正常的程序，就废了。（当然，能体现出这种情况的程序也很稀有）

类型是离不开「程序」的，但程序是一个很抽象的东西。
作为引入，我们说说过程式吧。
过程式和函数式最主要的差别是过程式没有闭包，但它依然有子程序(subroutine) 和递归（不一定，但现在已经广泛支持）。（另，递归必须和栈数据结构一起想，希望你学了）
虽说函数式最主要的特征是「以函数的组合编制程序」，仅仅一个闭包其实足矣让过程式和带执行顺序的函数式分道扬镳了，因为函数式可以在闭包的逻辑里混入数据状态，过程式根本没办法（它只能死传参，即便有函数类型也一样）。

闭包是 Lexical scoping 里的概念，而这种作用域又是 λ演算(Lambda calculus, 下简称"λ") 引入的，
这个演算主要是为了建立一个抽象化基本操作（如加法）的形式化方法，或者说一个“迷你编程语言”；实际上它最开始创建的目的就是形式化数学计算。
lambda 演算包含三种项：Abstraction (λformals. body)、Application (f x)、Variable (x)
（另，formal 即是『形式化参数』）

如果你学过 Ruby 元编程，Ruby 的 (variable) Binding 实际上就是 λ 的 "environment"
lambda 演算会有一个全局 environment，被称为 Gamma (Γ)。它可以包含各种“基元操作”（如加减法什么的，不能进一步细分的操作）（另，基于 Peano numbers 也即 N = Zero|N+1，加减法是可以利用分支函数被定义的）
大写的 Lambda (Λ) 则被用于指代全体 Abstraction 集合
两个常见操作：alpha-equivalence (rename) 和 beta-reduction (eval)；第一个代表名字的本质只是对 λformal. 参数的引用，第二个代表可以通过递归“化简”（实际求值）整个树形结构可以获得它代表的值（所以说函数式是不重视求值顺序和副作用、只重视求值结果的）
Lexical scoping 是「嵌套序作用域」，比如有 (λx. λy. x)，那么 x 实际上仅是代表 λx. 这个外层函数(outer function) 的第一个参数。
（另，基于 lexical scoping 和 currying，多参函数也可以变成 λx.λy. 形式的单参高阶函数组合）
（另，参数的求值模式如 call-by-value 是由 caller 计算参数传值、call-by-name 是直接传表达式用到再求值、call-by-need 相较 by-name 的特点是只求值第一次，缓存结果，也就是 lazy）
（另，一般说 (||) (&&) 是「短路操作」，实际上也可认为是「惰性求值」的意思）

在基于过程的『算法』里，程序可以按（求值/控制流）两种计算部分进行划分
编程语言，无论其形式是字面还是二进制，主要的目的是编码程序的语义；最大化表现力非常重要，所以一般的编程语言，语义都可以用递归数据结构—语法树，来表示。

当然，语法树也可以通过翻译器等价变换为线性形式。一般的编程语言设计，最重要的部分就是让它在计算机上跑起来

再来谈谈其他的。下为常见编程范式，按（相对于机器语言的）抽象程度降序排列：
== 非结构编程 (unstructured programming) ==
所谓机器是输入/输出、控制器(control unit)、算术器(ALU, arithmetic logic unit)和一打存储器。
偶尔还包含访问外设/利用中断系统/利用硬件内存管理单元(MMU)/进行权限控制的能力

所谓程序是一串指令序列，它们一个接一个地顺序执行(one after one)
部分指令会读取或修改(read or modify)存储器，也有指令可以令处理器转到程序的另一部分继续执行。
随机跳转(random jumps) 可以实现高级语言需要的分支/循环控制流。（另，图灵完全是要求有等价无限循环的，不过一般说循环都默认包含）

+ 机器语言（存储程序形计算机），一般都是保存在存储器的二进制序列
+ 汇编语言（和目标机器相关，如 Intel 和 AT&T，常见 NASM, YASM 等扩展）
== 表述式 (imperative) ==
所谓表述式指语言面向算法执行过程（抽象程度更高的 顺序、分支、循环，即便图灵完全的非结构化编程里这些理论上就必须实现）建模。
结构化编程可以认为是 程序=数据结构+算法。 一般还认为，数据结构是算法的最终目的或者副产物。

+ 过程式(procedural) aka. 命令式 aka. 结构化编程 (structured programming)
就是 C 的 function，(unsigned) int, array struct enum union 什么的…… 当然 sizeof, alignof 这些都是 C 标准扩展，和 struct 之类的基础数据结构无关
在谈编程范式的时候，指针之类的语言特性，以及 C 对底层机器的操作性都是小问题。
+ 纯面向对象(purely object-oriented)
其实面向对象不能严格算是表述式，但「纯」的面向对象（没有函数式类型的面向对象）可以。
面向对象一般有四大特性——封装、继承、抽象、多态
一般而言『对象』可以被认为是一种强类型的闭包(closure)，常说方法调用是「给对象发消息(message passing)」算是一个比较烂的比喻
如果你学过 Ruby 元编程，你会发现 obj.method(:send) 事实上可以代表一个对象——虽然它只是一个接受 method call 的闭包
方法的
面向对象可以有虚方法
*注：不懂的词往下看，多看几遍就懂了
== 定义式 (declarative) ==
+ 函数式(functional)

Identity type 是『同构类型』，关于同构就是（有类型 a b），（存在 f: a -> b 和 f': b -> a）

https://github.com/thautwarm/EBNFParser #GitHub #zhihu #cs #PLT #TT 啊，原来红姐是这个人啊！

王垠在计算机科学 #cs 方面的确是以程序设计语言理论 #PLT 的传统类型论(打不到 #tt)见长 ，他其它方面我不作评，但此人就这方面的知识水平也不是国内网圈顶尖的，顶多算费心分享(老实说隔壁 ice1000 比他高到不知哪里去了,许多函数式编程社成员也比他了解PLT,但那群人大多没有也“不屑于”有实践能力)；另外『高级语言』是与非结构编程(机器码/其汇编形)、表述式、面向对象、定义式 对应的概念，是编程范式的归类，没有「更高级语言」的说法。

类比嘛你也不能指望人家懂你的领域，同样我们评价一个人也要参考多方事实，不能见得风是得雨。

常用类型理论是为编程实践复用性、安全性(即正确性)所需类型系统—的构造服务的，“大量相关但不相同”描述正确但太抽象（应该举例说 struct/union 的 product/sum type 组合方法，而 enum 仅是 typealise+val define 非新种类型）

而且 C++ 比 C 高级的地方不在于类型系统，类型系统只是约束，闭包、协程等特性实现才是关键，而它们属实践细节(如计算被闭包的量必要的 sizeof)，与真正的类型论都无关。

在计算机科学，实践太冗长、理论太浮华，二者不大统一，甚至有互相鄙视的倾向，所以有领域大佬就觉得，干脆叫计算机工程好了，贴切，咱这些学习「基础」知识的人都应该有这种意识。 #statement

#java #plt #tt #typing #zhihu #旧事重提 https://tttttt.me/dsuse/14417

#endFork #typing #tt #java

#java #cs #DontKnow Integer.valueOf 的缓存机制 (即 (Integer)x==x 的左范围)

#functional 妈的，函数式和 SICP 现在自造词还不一样了，应用序 vs. 传值、正则序 vs. 传表达式(或是传惰性?)...

#JS #CSS #PLT HTTP #backend #blog 大佬的面试经历 我终于知道cs是学啥了🤔 杂学

#rust #PLT #tt https://edward40.com/tagless-final-in-rust 呃... 看来Ray说自己很菜是有道理的，是我见得少了，没想到同道这么多🌝

https://9bie.org/index.php/archives/635/ 超星邀请码... 这又一个 pwn #Security 的

https://cnblogs.com/Dillonh #oi #dalao 是 cnblogs... 上次一个 commajia 大佬也是

#cplusplus #English #PLT #ce #parsing #llvm https://zhuyi.fan/post/write-a-bf-compiler-with-joy.html
🌝🌚 看来是 CS ，爱了爱了

https://raptazure.github.io/posts/purs-react/ #functional #JS #tt #English 草这又是个大佬... 类型论大佬都喜欢英语

#oi #school #life 这位同学亲切一点，好像还在学德语🤔

#kotlin #PLT #tt #functional 🌚
顺便说一句，上面 Lua 指令重编号的如果有 luac 就很简单，因为指令号是「编译器和虚拟机里一致」就透明的东西，想要获得反处理算法所需的 new=>origin 映射表只需要两版 luac 编译相同代码。

之后查一下 prototype 里的 opcodes ， assoc ops[i], opsOld[i] 按序数就能拿到指令号对应关系了，然后 mapBArray 就能翻译过来。 整体命令都不需要十行代码或 indexOf reverse 😒

#typescript #TT 科普 TypeScript Type-Level Programming - lsdsjy的文章 - 知乎
https://zhuanlan.zhihu.com/p/54182787

TS是支持静态类型的JS。有 number,string 等值，也有常量作 literal type: number, .. "div" "body"..
<K extends keyof ElementMap> :R=Map[K] 是入门级子集定义吧！TS里{a:1,b:""} 的类型都是这种表。此外 {[K in keyof T]: } 可作转化
这个表里[num,str] 是 num|str 的意思，因此若有 P={a:num,b:str} 则 P[keyof P] ，就是并集类型。类同{}类型， {[K in KS]: }[KS] 给并集list 作转化

let v: (() => void) extends Function

的类型是true(lit type). 以下 is=extends
type T={a:num,b:str} //v:{a:Num|never} ，never=kotlin.Nothing |的不动(0值)点
let v:{[K in keyof T]: T[K] is number? T[K] : never }[keyof T] //收集并转换

子类型中 Int is Num, Num is Num 。is是 <= (never不大与任何类型)的意思，如何实现(=)呢？

type Equal<T, U> = T is U ? (U is T ? true : false) : false //TS类型上无&& || !
let v: Equal<Func, Function>  // v: true //最后一遍:这是编译期可知

TS只支持 recursive mapped types，“递归函数”只能返回 dict。设想 T={xx: T|Promise<U>} ；把T内所有Promise.resolve 的函数类型是啥？
type Unwrapped<T> = { [K in keyof T]: T is Promise<infer U> ? U : Unwrapped<T> }
type Unwrap<T> = (wrapped: T) => Unwrapped<T>

这里也以infer语法来引入新的 typevar <U> ，算是某种意义上的“模式匹配”。在Haskl 对 ADT 的值作模式匹配；在这儿，我们对有着“代数类型 类型”的TS类型作模式匹配。
ADT 有普通的函数状 data constructor；Type 也有 type constructor，比如 Promise就是 T->Promise<T>的“类型函数”。它是 lit,list,dict 外第三种组合方法
type:
Nat<N> = Zero | Succ<N>
Zero = void; type Succ<N> = { pred: N } //0, +1
_1 = Succ<Zero>
_2 = Succ<_1>

IsNat<T> = T is Nat<infer N> ? true : false
q1 = IsNat<_2> // true
q2 = IsNat<number> // false
IsNatIsNat = IsNat<IsNat> //err: IsNat require param

然后是:
一开始的时候，我把 Coq induction 和数学归纳法搞混了。要用数学归纳法证明一个命题 P，你需要先证明一个基础步骤 P(0)，然后在 P(n) 成立的情况下证明一个递推步骤 P(n+1)。但是在 induction 里面没有“基础步骤”和“递推步骤”之分，甚至 induction 产生的小目标的数量都不一定等于2。之后，我发现你可以把 induction 理解成数学归纳法的一种扩展。数学归纳法是作用在自然数上面的，而自然数是一种递归定义的归纳类型：

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Lemma len_repeat:  --n(s rep k)=k*n(s)
  forall s n,
    String.length (repeat s n) = n * String.length s.

intros s n. induction n
(s rep 0)=0*n(s)—无归纳假设, 下递归定义,有.
(s rep N+1)=(N+1)*n(s)

Lemma len_app_plus: --n(s+s1)=n(s)+n(s1)
  forall s1 s2,
    String.length (s1 ++ s2) = String.length s1 + String.length s2.

要证明 len_repeat，我们就要对 n 进行归纳，因为 repeat 是定义在 n 上的一个递归
证明 len_app_plus，就对 s1 进行归纳，因为 String.length 在每次迭代中会消耗字符串的第一个字符。当你对 s1 进行归纳的时候，第二个情况会是 s1 = String char s，这就对应了 String.length 的定义


作者：陈乐群
链接：https://zhuanlan.zhihu.com/p/54164515 能够看出来写得很好，还带FAQ..可对外道入门逻辑式还不够唉

#rust #PLT 自由程续-阴阳谜题 手动脱call/cc解
Rust 阴阳谜题，及纯基于代码的分析与化简 - 知乎用户FGAvTw的文章 - 知乎
https://zhuanlan.zhihu.com/p/52249705
#Python 5行yield解 https://zhuanlan.zhihu.com/p/43207643

如何制造SCP018 - 圆角骑士魔理沙的文章 - 知乎 — 函数式尾调用优化
https://zhuanlan.zhihu.com/p/43163820
形式验证、依赖类型与动态类型 - 老废物千里冰封的文章 - 知乎 讲了 Nullable,静态长Vec,运行时报错的type兼容
https://zhuanlan.zhihu.com/p/50792280