duangsuse::Echo
#PLT #JB 看起来能加结构化编辑，有意思
补充一句我现在自己的一点提纲，顺便科普下一些基本的编译原理/程序设计语言理论知识 #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)；第一个代表名字的本质只是对
Lexical scoping 是「嵌套序作用域」，比如有
（另，基于 lexical scoping 和 currying，多参函数也可以变成
（另，参数的求值模式如 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
在谈编程范式的时候，指针之类的语言特性，以及 C 对底层机器的操作性都是小问题。
+ 纯面向对象(purely object-oriented)
其实面向对象不能严格算是表述式，但「纯」的面向对象（没有函数式类型的面向对象）可以。
面向对象一般有四大特性——封装、继承、抽象、多态
一般而言『对象』可以被认为是一种强类型的闭包(closure)，常说方法调用是「给对象发消息(message passing)」算是一个比较烂的比喻
如果你学过 Ruby 元编程，你会发现
方法的
面向对象可以有虚方法
*注：不懂的词往下看，多看几遍就懂了
== 定义式 (declarative) ==
+ 函数式(functional)
Identity type 是『同构类型』，关于同构就是（有类型 a b），（存在 f: a -> b 和 f': b -> a）
当然，在完成 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）
duangsuse::Echo
补充一句我现在自己的一点提纲，顺便科普下一些基本的编译原理/程序设计语言理论知识 #Learn #PLT #TT 当然，在完成 ParserKt 以及一些简单过程式语言的实现之前，我是不会涉足类型论的，因为在我看来它就是逻辑/抽象代数，而我逻辑不太好。 不喜勿喷，欢迎帮忙订正。 一般的类型论就是「给程序查错」的一种机制，类型系统制定规则，可以判断程序是否符合。符合=阴性(negative)、不符合=阳性(positive)。 基于停机问题，一个 type checker 不可能同时： + sound，不存假阴性…
突然觉得好没意思啊，简单说一下
子类型(subtyping) 我就不说了
刚才说程序是组合来的，通过 递归的树结构（为了保证最大可组合性，所以当然是递归的啊） 可以描述一段代码的抽象结构
也就可以做诸如 preetyPrint、interpret、typeCheck、compile 之类的工作
sum type (一般实现为 tagged union) 和 product type 就不多说了，搜索一下之前也提过
Tuple 是 anonymous 的 product、Array 是 homogenus product、struct 是 named product
product type (f0*f1*f2), field 和 sum type (v0+v1+v2), variant
都是在状态的总数上描述这大类数据类型，比如 k 位二进制总共有 2**k 个可能状态。
注意上面的这两种 type 主要是在 data type 上，而不是类型论上，因为上面那附图知识点好多…… （还好冰封不可能看到这些，不然又要被喷教坏小白以及不学无术）
关于 lambda 演算比较常被人拿出来展示的类型系统框架，Lambda cube，是一个用 3-axis (xyz) 组织出的知识归纳方式，我不太喜欢学术的东西所以应该不会准确。
xyz 轴分别代表 (->) dependent type (^) polymorphism (/) type operator
一般三维座标系会被视为 x-y 再扩展一个深度 z，这里 xyz 分别是 (depend, poly, comb)
Identity type 我不知道，不过说到 identity (itself) 操作，入门者不知道这种函数有啥用。
测试同一性(identity)的，毕竟，没有比一个值本身更好的描述它的相等关系的方式了。
自反性(reflexive)呢？这是一个组合证明最基元的操作，就像那些公理一样，不能再往下细分了
Pi type 就是 dependent type，Sigma type 是 dependent type 的 tuple 元素扩展
row polymorphism 在知乎上有个初中生大佬讲过，不过我不想去找了，感兴趣可以自己搜索
这个 "row" 是代表『列』数据结构，整个系统是貌似是和动态语言相关的
类型类(typeclasses) 就是给一堆操作赋予类型变量，多态
归纳类型(inducative type) 嗯，还记得数学归纳法吗？基线和递推……
逆归纳类型(coinducative type) / Copatterns 嗯，以计算的有限来保证无限类型的有效？
Tactics(格) 是偏序理论里的东西，我不太清楚
Sized types 也是一个讲 =zero 的东西，据说和 dependent type 的 termination check 有关
Path types 据说是线段
HIT 不知道是什么的缩写
Elaboration reflection
Dynamic pattern unification
V type
通通不知道
Holes 据说是可以弄……部分程序？
Conditions
Glue
JMeq
induction recursion
induction**2
Overlap pattern
SSet/SProp
Type-preserving complication
ereasure
hcomp
别说我不懂，难道这还需要强调吗？抱歉我看不懂数学符号和希腊字母…… 谁能不用希腊字母给我解释一遍这些东西，我就跟他学……
我讨厌数学的原因，很大一部分是我觉得代数的表示，各种希腊字母很做作，以及他们过于追求『真理』而丝毫不顾及外面的一层认知“缓冲垫”。说白了，就是他们一开口绝不从零开始、写文章也总是有点没注释完全的地方，哪怕那并不困难。
细化点，我实在是看不到这个“广义”类型论和平时那些“弱类型系统”语言如 Java，甚至 Rust Scala 的“类型”有多大程度上的关系，或许是要求越多、问题越代数，关系越大吧……
子类型(subtyping) 我就不说了
刚才说程序是组合来的，通过 递归的树结构（为了保证最大可组合性，所以当然是递归的啊） 可以描述一段代码的抽象结构
也就可以做诸如 preetyPrint、interpret、typeCheck、compile 之类的工作
sum type (一般实现为 tagged union) 和 product type 就不多说了，搜索一下之前也提过
Tuple 是 anonymous 的 product、Array 是 homogenus product、struct 是 named product
product type (f0*f1*f2), field 和 sum type (v0+v1+v2), variant
都是在状态的总数上描述这大类数据类型，比如 k 位二进制总共有 2**k 个可能状态。
注意上面的这两种 type 主要是在 data type 上，而不是类型论上，因为上面那附图知识点好多…… （还好冰封不可能看到这些，不然又要被喷教坏小白以及不学无术）
关于 lambda 演算比较常被人拿出来展示的类型系统框架，Lambda cube，是一个用 3-axis (xyz) 组织出的知识归纳方式，我不太喜欢学术的东西所以应该不会准确。
xyz 轴分别代表 (->) dependent type (^) polymorphism (/) type operator
一般三维座标系会被视为 x-y 再扩展一个深度 z，这里 xyz 分别是 (depend, poly, comb)
Identity type 我不知道，不过说到 identity (itself) 操作，入门者不知道这种函数有啥用。
测试同一性(identity)的，毕竟，没有比一个值本身更好的描述它的相等关系的方式了。
自反性(reflexive)呢？这是一个组合证明最基元的操作，就像那些公理一样，不能再往下细分了
Pi type 就是 dependent type，Sigma type 是 dependent type 的 tuple 元素扩展
row polymorphism 在知乎上有个初中生大佬讲过，不过我不想去找了，感兴趣可以自己搜索
这个 "row" 是代表『列』数据结构，整个系统是貌似是和动态语言相关的
类型类(typeclasses) 就是给一堆操作赋予类型变量，多态
归纳类型(inducative type) 嗯，还记得数学归纳法吗？基线和递推……
逆归纳类型(coinducative type) / Copatterns 嗯，以计算的有限来保证无限类型的有效？
Tactics(格) 是偏序理论里的东西，我不太清楚
Sized types 也是一个讲 =zero 的东西，据说和 dependent type 的 termination check 有关
Path types 据说是线段
HIT 不知道是什么的缩写
Elaboration reflection
Dynamic pattern unification
V type
通通不知道
Holes 据说是可以弄……部分程序？
Conditions
Glue
JMeq
induction recursion
induction**2
Overlap pattern
SSet/SProp
Type-preserving complication
ereasure
hcomp
别说我不懂，难道这还需要强调吗？抱歉我看不懂数学符号和希腊字母…… 谁能不用希腊字母给我解释一遍这些东西，我就跟他学……
我讨厌数学的原因，很大一部分是我觉得代数的表示，各种希腊字母很做作，以及他们过于追求『真理』而丝毫不顾及外面的一层认知“缓冲垫”。说白了，就是他们一开口绝不从零开始、写文章也总是有点没注释完全的地方，哪怕那并不困难。
细化点，我实在是看不到这个“广义”类型论和平时那些“弱类型系统”语言如 Java，甚至 Rust Scala 的“类型”有多大程度上的关系，或许是要求越多、问题越代数，关系越大吧……
有时候感觉自己还怪分裂的，明明应该敬而远之但仍有好奇
感觉自己就像一个落魄的编辑，跑到一群教授那里像猴子一样
他们都是那样各顾各的，用一些魔法一样简短的话和大量名词、希腊字母，最后说你没天分、不尊重研究者、侮辱理论、咎由自取不懂进步云云……
刚开始想的时候感情丰富波动猛烈，现在没有感情了。
现在想想，或许我还真不适合当“教授”，但只要能做好科普我就知足了
有大佬说我没天分，我当时或许真应该说…… 就是为了让没天分的人，也能做与有天分的人类别相同的事情，才一直坚持这种“民科”的
或许我真的是民科，不需要被人认同，理论又幼稚、到处都是自己幼稚的私货，没有学识、共同体、交流；那么，民科到底是什么呢…… 必须是科班出生，才不侮辱科学吗……
想先弄个 unification 的玩具玩玩…… 反正 ParserKt 也不急着出 v3 🤔
感觉自己就像一个落魄的编辑，跑到一群教授那里像猴子一样
他们都是那样各顾各的，用一些魔法一样简短的话和大量名词、希腊字母，最后说你没天分、不尊重研究者、侮辱理论、咎由自取不懂进步云云……
刚开始想的时候感情丰富波动猛烈，现在没有感情了。
现在想想，或许我还真不适合当“教授”，但只要能做好科普我就知足了
有大佬说我没天分，我当时或许真应该说…… 就是为了让没天分的人，也能做与有天分的人类别相同的事情，才一直坚持这种“民科”的
或许我真的是民科，不需要被人认同，理论又幼稚、到处都是自己幼稚的私货，没有学识、共同体、交流；那么，民科到底是什么呢…… 必须是科班出生，才不侮辱科学吗……
想先弄个 unification 的玩具玩玩…… 反正 ParserKt 也不急着出 v3 🤔
待会枚举下 ParserKt v3 的各种 class 和扩展操作，然后重新设计一下看看 Kotlin 里 unification 算法关系式求解怎么写 🤔
https://stackoverflow.com/questions/58859081/how-to-install-an-older-version-of-gcc-on-fedora
太草了，Fedora 想安装低版本 GCC 都难
太草了，Fedora 想安装低版本 GCC 都难
export CYCLES_CUDA_EXTRA_CFLAGS="-ccbin gcc82"Stack Overflow
How to install an older version of gcc on Fedora
I tried to install CUDA on Fedora 31 but got stuck at the last step because CUDA officially supports Fedora 29 (gcc 8.2) while the version shipped with Fedora 31 is 9.2, I then installed Pytorch with
/usr/local/gcc82/include/c++/8.2.0/type_traits(1049): error: type name is not allowed结果我做了一个很 dirty 的 hack，直接把那个 type_traits:1049 给注释掉了……
/usr/local/gcc82/include/c++/8.2.0/type_traits(1049): error: type name is not allowed
/usr/local/gcc82/include/c++/8.2.0/type_traits(1049): error: identifier "__is_assignable" is undefined
CUDA version 9.2 detected, build may succeed but only CUDA 10.1 is officially supported.
Compiling CUDA kernel ...
"/usr/local/cuda/bin/nvcc" -arch=sm_50 --cubin "/usr/share/blender/2.82/scripts/addons/cycles/source/kernel/kernels/cuda/kernel.cu" -o "/home/DuangSUSE/.cache/cycles/kernels/cycles_kernel_sm50_6255A65CE4C22FC648BF7975BC54FC30.cubin" -m64 --ptxas-options="-v" --use_fast_math -DNVCC -I"/usr/share/blender/2.82/scripts/addons/cycles/source" -ccbin gcc82
不知道会不会爆炸
Forwarded from ❌; Ζέφυρος Λύκος
首先 AEAD 的加密方式已经防止了重放，只有原来的 Legacy 加密方式能被重放
Forwarded from ❌; Ζέφυρος Λύκος
为什么 shadowsocks-libev 占那么多内存就是因为要防重放