前段时间在 FFW 问到有没有机器人往 Telegram 发消息的 cli 工具，似乎没有，于是自己写了一个。最终想实现的是这样一个需求：

some_really_long_task && gu --sender telegram "finished"

https://github.com/outloudvi/gu

Redis 官网连不上 Redis🌝

#Math #recommended @LEXUGE 大佬还是很厉害

#PLT #TT

#PLT #JB 看起来能加结构化编辑，有意思

https://www.jetbrains.com/mps/

好, 我被 jetbrain 忽悠的非常激动(

补充一句我现在自己的一点提纲，顺便科普下一些基本的编译原理/程序设计语言理论知识 #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）

#sysadmin #linux

突然觉得好没意思啊，简单说一下

子类型(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 🤔

待会枚举下 ParserKt v3 的各种 class 和扩展操作，然后重新设计一下看看 Kotlin 里 unification 算法关系式求解怎么写 🤔

https://stackoverflow.com/questions/58859081/how-to-install-an-older-version-of-gcc-on-fedora
太草了，Fedora 想安装低版本 GCC 都难
export CYCLES_CUDA_EXTRA_CFLAGS="-ccbin gcc82"

https://gcc.gnu.org/mirrors.html
编译更不可能，何况手动编译太麻烦

/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: type name is not allowed
/usr/local/gcc82/include/c++/8.2.0/type_traits(1049): error: identifier "__is_assignable" is undefined

结果我做了一个很 dirty 的 hack，直接把那个 type_traits:1049 给注释掉了……

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

不知道会不会爆炸

没炸，成功了 🍥

不过，貌似每次都要调用 nvcc，所以必须得一直 export CYCLES_CUDA_EXTRA_CFLAGS="-ccbin gcc82"