Kotlin 抽象的威力、扩展方法、operator overloading，typealias、闭包

立刻告一段落，实在是太花时间了 没时间写编译器了

看起来全 TM 没时间写了，不过不要紧，因为过两天高考放假（这里希望各位都能取得好成绩哦~我知道很多同学也都是很努力的，努力就一定有收获呢）
我还会回来的~ 🐱

所以，我要先巩固一下 LLVM Cookbook 的学习结果

写一下 Toy 语言的前端和代码生成器、JIT、FunctionPass

这些是编译器工程师的基本操守，大概从会写 (for LLVM like frameworks) Pass 开始就算是一个 CE 了，加油哦。

这个编译器接受这样的语法，它的 tokenizer 基本是使用 libc 的 API（e.g. isalpha, isalnum, isspace from ctype.h）弄的

然后数值的解析基本都是 atoi, strtod 什么的。

这里，因为我实在是没有时间，所以支持特性的很少

以后我会给它增添浮点类型（就是所谓的 “两种基本类型：Long integer 和 Double Prec floating point，不支持类型组合”）first-class 支持
和支持 hex, binary 字面数值


— 语言部分

这是一门简单的计算器语言：它支持 Int 值，可以进行 +, -, *, / 操作
可以进行 function definition：def <name> ArgList Expr


Tokens

数值：C isdigit+
标识符（名字）： C isalpha isalnum*
空格：C isspace+
注释：支持行注释，以 # 开始直到 "\n", 换句话说，自动支持 CRLF 和 LF, 可怜的 Windows！（默认 CR \r）
好吧，因为原版支持了 \r，我也支持一下算了，于是 Windows 也可以用

data Token
  = Num Int | Iden String
  | Spaces Count | Comment String
  | KwDef | ExpGrouper Bool
  | Operator | EOF

EOF：因为不用 EOFException，什么？Haskell 为什么不用 Maybe 或者 Exception Monad？因为这是要用 C 写的！

关键字在词法上和标识符采取一样的规则：

def

只要不是上面任何一种，即为 Operator，支持：

() 作为表达式组合的标记
, 作为列表分割的记号
infixl + < - < * < /

就有这样的语法 EBNF 规则，首先我们想的是 def 定义函数，entry 规则是一个表达式组，我们可以像 REPL 一样用：

Entry -> Expr

TERMINATOR def, extern
TERMINATOR SYMBOL +, -, *, /, COMMA, (, )

Expr -> Primary . "BinRhs" (binop Primary)*
  where binop -> '+' | '-' | '*' | '/'

Params -> Expr (',' Expr)* -- Recursive
Names -> ident (',' ident)*

Primary ->
  "Derefing" (IdentRef | IdentCall) | NumLit | ParenExpr
  where
    ParenExpr -> '(' Expr ')' -- Recursive
    NumLit -> number
    IdentRef -> ident
    IdentCall -> ident '(' Params? ')'

— Function
FunTypedef -> ident '(' Names? ')'

ExternFun -> extern FunTypedef
DefFun -> def FunTypedef Expr

这样就可以弄出这些示例：

def add2(x) x +2

DefFun {
type { name "add2"; args (!!) ["x"] }
body {
Expr {
me IdentRef(ident("x")); op '+';
rhs NulLit(number(2))
}
}
} (1)

def sub1mul3(x) (x-1)*3
def add(x, y) x + y


def sumWeight(x, wei) (x-1) + wei*10

然后我们又是分开来 handle FunDef 和 Expression 的求值的
REPL 其实就是

forever do {
expr = parse!(gets)
expr.evaluate!
}

其中 Expr.evaluate!

when expr {
is Expr -> puts this.treeEvaluate!
is ExternFun -> module.externFunction(this.type)
is DefFun -> module.createFunction(this.type, this.body.compileAll())
otherwise -> error("Cannot handle expression $this.name")
}

比如上面的例子 (1)，只需后序遍历 AST 就可以面向某种目标生成代码：

walk DefFun {
val signature = type.createSignature()
unless my_module.hasExtern(signature) and my_module.hasDefinition(signature)
my_module.createFunction(signature, body.walk())
else error("Defined function does not match (for $signature)")
}
walk Expr: Value {
return when op {
'+' then Builder.createI32Add(me.walk(), rhs.walk(), "sum")
otherwise error("Unknown operator $op")
}
}
walk IdentRef: Value {
return scope.get(name).mapError { error("Failed to resolve symbol in context $scope.ctx") }
}

walk NumLit: Value {
ConstantInt.get(Types::getInt32Ty(my_ctx), value)
}

LLVM 是基于 SSA 架构的，这个架构假设 LLVM 有无数个机器寄存器，它的指令结构是线性的，但是任何指令的结果都可以被其他指令引用而无须显示指定目标存储器，这样的指令虽然是线性序列，但实际上可以被归纳到树形结构或者从树形结构被创建

比如 data Ast = Lit Int | Add Ast Ast（Haskell）

eval :: Ast -> Int
eval (Lit x) = x
eval (Add lhs rhs) = eval lhs + eval rhs

evalSsa :: Ast -> Value
eval (Lit x) = constInt x
eval (Add lhs rhs) = add (eval lhs) (eval rhs)

上面的 walker 对于 (1) 应该能生成这种代码（LLVM IR）

define i32 @add2 (i32 %x) {
entry:
%sum = add i32 %x, 2
ret i32 %sum
}

这是对 Ast 进行后序遍历（一种括扑排序）的结果，当然有多少个 Add 都一样，结果肯定是正确的

def add2_3(x) 3+(x+2)

define i32 @add2 (i32 %x) {
entry:
%sum = add i32, %x, 2
%sum1 = add i32 %sum, 3
ret i32 %sum1
}

试用！ #CE

source_filename = "add.ll"
!llvm.module.flags = !{!0}
!llvm.ident = !{!1}

!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{!"duangsuse version ??? (Fedora 7.0.1-6.fc29)"}

define i32 @add2_3 (i32 %x) {
entry:
  %sum = add i32 %x, 2
  %sum1 = add i32 %sum, 3
  ret i32 %sum1 
} 

declare i32 @printf(i8*, ...)

@.fmt = private unnamed_addr constant [9 x i8] c"res: %i\0a\00", align 1

define i32 @main (i32, i8**) {
enrty:
  %res = call i32 (i32) @add2_3(i32 3)
  %_r = call i32 (i8*, ...) @printf(i8* getelementptr inbounds ([9 x i8], [9 x i8]* @.fmt, i32$
  ret i32 0  
}
 

—
[DuangSUSE@duangsuse]~/projects% lli add.ll
res: 8

（ #Low #China 🌚

响应国家号召，本频道明天将进行技术升级，停更一天。

#PL #PLT 推荐，当然本频道之前也有讲类似的东西，非常感谢 LEXUGE 一直能关注这种弱鸡频道...（是的，在同为非应用向编程的人前我丝毫不会感觉自己容易被喷、或者对方要秀我一脸什么的，而且也不会莫名“自大” — 这类人显然在我说些可能他们还没学到的东西时候不会有任何不适感，各弄各的） 因为我在 GitHub 更新上看到他 Star 我最近改名的一个 repo，说起来，最近大家（一些可以认为是『学院派』一点的博主）都开始用纯 English 写作了，有点看不懂的样子，看来英文还是得学啊

https://github.com/duangsuse/Essay-C-Calculator 没写完完

https://github.com/DirClean/BackwardParser #life #dev 唉，果然还是没法逃过应用向的追击嘛。只是花了整整一天的时间而已，使用了 Java 的 IO、File、Gson 和 Kotlin 语言设计的 :: reference、clinit block，虽然我不清楚是不是翻译器生成的，不过要生成那玩意怕不是翻译器有点高级（因为需要把一个 nullable 翻译成 lateinit，空判断也要翻译好）（为什么？是因为它很 Kotlin，但是不够 Kotlin，排除 const val 而不是 enum 这类无关紧要的问题外，它居然使用了 System.out.println 而不是 kotlin 的 ForceInline 的 println 函数，虽然）

比如 Java 8 的 Stream（StreamSupport.stream(?, boolean)；Spliterator.spliteratorUnknownSize；Gson 的 JsonElement、JsonObject；函数式编程都常用的 map 操作；Kotlin 里自己明明都... 抑或是 Spring ORM Repositories 里的 findFirst），虽然我对 Stream 的理解还是有的，可是还是莫名觉得威胁....

我果然还是不喜欢应用，看来 Yuuta 开发的速度果然是变快了呢，但是总是觉得自己虽然，工程向的人总是还不够令人满意呢... 不够包容

总是觉得会被喷，现在看来只会越来越严重了呢... 我也必须得赶快想想办法... 虽然对我来说阅读堆砌的逻辑已经不存在任何难点了，有没有办法证明我自己也能来写这些有时候会用所谓不常用抽象和逻辑的代码呢？

可能还是我不够包容吧... 为什么我会变成对那些写了很多东西但都是『不够学术向』的人有被害倾向的说呢？

记得刚才看见 Trumeet/XXXParser 的时候立刻就点进去看了，大概是害怕自己的技能会被轻易复制的那种吧。我果然还是有病。

顺便说一下，Trumeet 的英文语法水平值得练习一下，虽然我的语法也很差，但是 Trumeet 这里似乎的确有点很容易发现的语法错误，我想即便是初中生的话也大概是不能容忍的吧。
说实在话，我觉得为什么很多人的洋文语法都比我还辣鸡... 虽然我是从小训练语感稍微强一点啦

英文歌唱起来稍微有点困难，某些连音就不会连，但是音标上也开始到感受到所谓音位音标和音素音标的区别了呢，看起来语音学这种启蒙的课程也是很有用的...

https://github.com/DirClean/BackwardParser/blob/master/src/main/kotlin/moe/yuuta/ruleconverter/SourceParser.kt#L198

最后一段时间我看了一下这个函数，顿时觉得好魔法，虽然逻辑很易懂但是我弄不清 Name 是什么以及所谓的 RelativePath 是怎么单单通过最后的一个“append”操作加上自己的目录什么的弄出来的

我果真是老了么...
val path = file.absolutePath.substring(baseFolder.absolutePath.length)

啊终于知道了...
val paths = path.split(Pattern.compile(File.separator))

这里 path 是一个 String；file 是一个 kotlin.io.File /* alias for java.io.File in Kotlin JVM */

噢终于知道这是干什么的了，为啥不直接用 File 的 getRelativePath（因为这是 VFS，虚拟文件系统操作，文件夹，或者说树路径的名字是有语义的）

不过函数式编程的话可以这么写（抽象一个 VFS.simplifiedFile (Dir) Name(String): String 出来）：

typealias FilePath = String
private fun relativePath(file: kotlin.File): FilePath {
// 首先我们拿到相对 base dir 的 file path（直接通过路径线性表，噢不是 String 的 subseq）
val relCanonicalPath = file.absolutePath.subsequence((myBaseDir as FilePath).size).split(File.seprator)
// 然后直接 foldl 好了，至于如何解决最后一个文件名字的问题，不是可以先 subseq，反正性能不敏感
// Empty 的情况... 虽然我觉得不太可能，直接在 VFS 里面处理呗、异常直接传递或者捕获，如果捕获目的只能是为了提示这是第一次循环，当然 fold 又是不计数的...
val dirPath = relCanonicalPath.let { it.subsequence(0, it.size -1) }.fold(StringBuilder()) { ac, x -> ac.append(VFS.simplifiedDirName(x)).append(File.seprator) }
dirPath.append(VFS.simplifiedFileName(relCanonicalPath.last.name))
// 然后
return dirPath.toString()
}

至于异常什么的就传递吧，毕竟这个操作把异常吞掉什么的，可能这还不属于应用本身的逻辑，这一层不用处理异常呢

弄了半天我还是觉得自己低端一些，发现我把别人写了二十行的程序不仅少用了不少逻辑减少了不少分支，还少写了不少代码啊....
但我真的不觉得自己低端，只是我的思路就是这样而已... 真的就是这样而已，我没第一个想到要用 for until （我没说这是『特殊』的语法，其实只是扩展方法） 也没有想到要在 val 里用 elvis (?:) 操作决定提前返回 null(实际上这样导致某 val 的值可能为 Nothing，即便实践上后面的代码无法访问到这种情况，因为 Nothing 显然不会出现，它只能在类型的角度被讨论)
但这真的就是我的直觉...

#task 嗯嗯，那么明天又要上学了啊... 看来本来打算完成基本的计划都无法完成了呢，那计划就只有继续讲一些理论向的东西和开发一个应用算了

+ #PLT Zero sized types、Empty type(bottom type) 的 Sum(+) 和 Product(*): 为什么要给他们起这种名字

+ #Qt 5 Widgets 开发一个支持插件的 "Dullboy" 应用，其目的在于利用和 KDE Applet / Systemd 的集成，定时启动强制锁死用户界面一段时间，让我这种“工作狂”（无褒义，仅仅是我对自己的戏称）不能随便糟蹋身体健康 的说。

+ 顺带讲一下关于传统序列解析器架构策略相关的内容（比如命令行参数解析器）

+ 回复在 #Bilibili 《黑子的篮球》 S1 里看到的一个 NOIP 同好，虽然我不是 #OI 方面的说... 也不是不可能，但现在不是

== 这些是明显做不完的

+ #PL C++ 弄一个 REPL 支持的计算器，有所谓的 MidTreeParser 抽象和 ReplLexer 这种支持 Hook 上输入事件的 Lexer
+ LLVM 开发 Toy 语言的编译器，当然是照 LLVM Cookbook 画瓢，不过我是不会抄里面的不良实践的（比如，明明是返回 nullptr 却写成返回 0、到处使用 global linkage 的 static 变量）

+ Android 视图应用：Lime tokenize view
尝试开发一个使用 RecyclerView, Fragments, Services 的 Android 应用

应用向的人不准喷！不准喷！与你们无关！你们熟悉的我只是暂时没有时间去熟悉，也不要拿冰封哥的 CastleGame 数据库访问 show 我，比起 SQLite RDBMS，还是等会关系代数了或者说会图数据库了才能来说话！

+ Android 版本的 AllDreamWall & SDK

SDK 想做成 Maven 管理库的形式，不过不用为 Central 填写元数据，而且也只是自己发布的说
同样不准喷，真的不能喷啊... 这有什么的呢？

+ 默写一点关于 HTML4(5) 和 CSS 相关的东西，写点布局

+ 继续写完 smms.es6 （这个使用的 requests-promise-native）

这个是真心推荐，作者还为我们排版了数学公式，讲的就是 Rust 的 Trait (in its type system) 和集合论之间的联系（子类型和可取操作） #PLT
作者用的是英文，不过推荐依然要阅读，我过会也会阅读的

当然，因为我最近有在设计一门叫做 Radium 的新高级程序设计语言的说（而且它支持 Trait）
所以这个理论比较有用，但是我之前也有考虑过 trait 类型和其他相关类型的干系（基本没有理论基础的情况下，而且 Ra 的类型系统也没有被规范化，仅仅是我想了一些常见的例子中的类型检查和关系而已）

上面的转发评论可能是误解... LEXUGE 应该是有看我的频道，但这个和我之前的 PLT 入门没有很大联系（之前没有讨论到 Traits，只是简单的给了一个直觉，而且还没有贴 Agda 之类的来强化直觉... 真的是我没有时间...）

constructed types
show :: Show a => a -> String
(/) :: Fractional a => a -> a -> a

说到 traits （属性）
忽然发现上面有一个很弱智的错误：

show :: Show a => a -> String
(/) :: Fractional a => a -> a -> a

(Show a) & (Fractional a) constructed types ???

不是不对（因为 Show a 是 一个 Constraint，它在 Haskell 里也是类型，哦不，类型的类型，好吧还是类型... 刚才说那个不是类型的是 typeclass，它不是类型）但是这里角度错了
非常抱歉，我说错了一个非常基础的 Haskell 知识...

这里实际上，他们的类型是（a 是类型变量，String 是一个类型，它的 kind 是 ∗；(->) 是柯里化函数类型架构器；:: 表示 "has type"；() 包裹的 infix operator 是 Haskell 的语法特性，被称为 "sectioning"）

- show :: a -> String
- (/) :: a -> a -> a

不过！

- show 里的这个 a "是" forall a. (universal qunatifier ∀) 不过还有个额外的类型约束：a 必须是 typeclass （Haskell 类型类） Show 的实例 (Show a) :: *, 当然它是一种类型 (Constraint)
因为 Show 是 (* -> Constraint)

ghci> :kind Show
Show :: * -> Constraint
Show String :: Constraint

换句话说，show 就是 show :: forall a satisfies (Show a). a -> String

- (/) 里的这个 a 也是 forall a. 不过也有个额外的类型约束：
∀a.

(Fractional a) => a -> a -> a

有了 a 还不够，还得 "有"（就是 =>）

(Fractional a)

成立才能有 (/) :: a -> a -> a 这个操作符(operator) 存在

这就是 Haskell 里的 typeclass，类型约束这种东西其实 C# 里面都有（where T: class 什么的来让 type checker 保证某种 operation 在这个 type 上有效，比如这里 C# struct 就不能进行强制转换为 C# class 的操作）

当然，PHP5 里的『类型约束』就不是我们这里所讨论的类型约束了（虽然有相似之处，其实更类似 Python 3 里的...），照顾一下人家，毕竟 PHP 是动态弱类型哈？


下面是 Set Theory in Rust's trait system 这篇文章的阅读笔记 #PLT

== 问题：

有 trait 类型 A 和 B
假设有 type T = A & B，你能从中推断出什么？

(讲个笑话，这里我写的正好是有效的 Ra 代码，它定义 T 为 A 和 B 的 intersection type，跑)

where:
- 我们是这么抽象 trait 类型 A, B 的：他们有效操作（method）的 Set（集合）
比如说
Haskell 里的 Show typeclass (一种版本):

class Show t where
  show :: t -> String

这里 Show t 类型就是集合 {(show::t->String)} — Show 是表示类型约束的 Kind（(* ->)... Constraint），Kind 不是类型，它是类型架构器

- TI 是 Type Instance 的缩写(acronym)

== 第一个推论（实际上是从 T 的实际类型倒着推 A 和 B 上的属性...）

T = {method | method is method that implemented by T}

因为，
forall method_a in A
forall method_b in B

都有
method_a in T &&
method_b in T 成立

所以（啊，这是初中数学啊，还不是奥数，这样的简单逻辑快̶没̶有̶写̶出̶来̶的̶必̶要̶了̶...）

T supersetof (A unionset B)

当然这实际上表达了『T: A + B，A 和 B 都是 T .... 的子集 的意思』
在子类型上，我们只能说 T 是 A 和 B 的子类型，A, B 不能是 T 的子类型

== 第二个推论

现在 A, B 是（各自）他们的 type instance 的集合

T = {TI | TI ∈ type T}

定义集合

C = {TI | TI implements A ∧ TI implements B} = A insect B

如果 T 是 A 和 B 实例

T⊂C
T⊂(A∩B)

这里 ⊂ 是 subsetof 的意思
∩ 是 unionset 的意思，(A∩B) 实际上就是 type A, B 所谓的 intersection type

==
我们总结一下，上面这一堆瞎眼但其实是初中数学混高二逻辑和证明的... 集合式子到底是在说什么：
— 对作者：非常抱歉我是这么评价上面这些式子的，但这完全是因为我不习惯数学表达方式导致的，和式子本身以及作者水平之类无关

关于 type T = (A :: Constraint) | (B :: Constraint) （T 就是 Rust 里的 T: A + B）的推论

第一个：
T 是 A, B 的子类型，因为 T 实现了 A 和 B 的所有操作（超集或者同一集合）

T is (A | B)

T 是 A, B 的 Type union，至于为什么作者会把这个定义包含的属性写出来，因为原来我们是在讨论 Rust 的类型约束 T: A+B
我作了点弊，把使用的代码换成了自己设计的 Ra 语言的代码了... Ra 类型语法比较类似 PLT 上的表述，所以看起来就没有区别
作者的本意是告诉大家，
T: A + B => T 是 A, B 的 Type Union （推导过程上面有说，就是讨论有效 operator 集合的问题）

比如 forall t. A = Show t, B = Eq t
T 就是又实现 Eq t 又实现 Show t 的 Constraint

第二个：
在类型类的实例（Trait type instance）角度看：

type C = A | B
pure assert C is A and C is B

— C （trait）要求 Type instance 实现了 A 和 B trait（Trait Type Union）
— Trait Type Intersection 则是没有意义的，因为 trait 只是讨论 operators，不包含 values

— 在值(values)集合意义上讨论
+ A, B 的 Union type T 是两者值的并集；T 的实例可以应用到所有 A, B 『都支持』的 Operator 上
子类型理论里；亲类型和子类型的 union 是亲类型 (ancestor); 这意味着只有亲类型的 operator 可用，而子类型自然包括所有亲类型的值
子类型理论了；伴类型（subtyping 关系中存在相同亲类型的类型）的 union T' 是他们最近的亲类型的子类型
这意味着只有最近亲类型的 operator 可用（至少的），而子类型自然包括所有亲类型的值
但是这个 T' 依然可以包括他们共有的 operator

+ A, B 的 Intersection type T 是两者值的交集；T 的实例可以应用到所有 A 『或者』 B 『支持』的 Operator 上（T 和 A, B 都兼容）
子类型理论里；亲类型和子类型的 intersection 是被派生最多的类型（子类型阶更高的类型）
Num & Int 是 Num
伴类型之间的 intersection 与原类型不存在子类型关系

type T = A | B 的话

C is T


(A | B) is T
(A|B) is (A|B)

这样就好理解多了，如果 A 是 Show Int、B 是 Eq Int

Show Int 可以 show :: Int -> String
Eq Int 可以 (==) :: Int -> Int -> Bool
假设有 ShowEq Int 是 Show Int 或者 Eq Int (Show | Eq)
BothShowEq Int 是 (Show Int) 和 (Eq Int) (Show & Eq)

(Show|Eq) 的操作集合是 show, (==)
(Show&Eq) 的操作集合是 emptyset（空集）

这里 intersection type "我们共有的属性" 是 union type "你或者我有的属性" 的子类型吗？是！

（Haskell 用 Constraint 有点头晕了，我想 Ra 的类型系统应该会直接一点）


从集合角度看

T = A union B

T subsetof (A insect B)

==
供参考：
Ra 的类型系统与上面的集合式子之间的关系大概是：

Intersection type
(A & B) <=> A ∩ B
Union type
(A | B) <=> A ∪ B

Subtyping:
R is T <=> T⊂R
T is R <=> T⊃R

根据我自己刚才的思考以及作者的这个 issue，Rust generic type constraint 里的 + operator 获得的 trait 约束类型采取的是并集运算
Ra 里，并集对应的类型操作符是 | （交集的则为 &）

唉，其实讨论的太抽象了，实际上 Ra 要支持 Traits，还得再多下点功夫才行啊...

果然还是 PLT 说多了... 然后一事无成么...
既然这样待会继续 PLT 吧，不过那个时间管理软件依然必须开发，明天也一样
绝对不能再熬夜了！！！

#fix #typo mangel -> mangle

#PLT 再来说一下 Zero sized types、Bottom type 和 Sum type、Product type 的问题呢，推荐哦！

既然要说的话，势必得顺带提到很多其他的类型理论呢。不过一些我上面已经讲过了，这里讲是强化直觉。
既然要理解的话，直觉就是一切，因为死记书本
似乎是没有用的呢，我们不是文科生，如果没有将理论、作者的直觉和自己的直觉统一，还有不清楚不明白的地方，说明自己不是真正弄懂了这些东西呢。
这就是理论上必须要做好的觉悟。直到完全拥有需要的直觉，不断的重复强调学习！

We say that a language is compiled if the translator analyzes it thoroughly (rather than effecting some "mechanical" transformation), and if the intermediate program does not bear a strong resemblance to the source. These two characteristics—thorough analysis and nontrivial transformation—are the hallmarks of compilation.
如果翻译器对程序进行了彻底的分析而非某种机械的变换，而且生成的中间程序与源程序之间已经没有很强的相似性，我们就认为这个语言是编译的。 彻底的分析和非平凡的变换，是编译方式的标志性特征。

We say that a knowledge point is comprehended if the you analyze it thoroughly (rather than echoing what the books say), and if the concept generated in your brain does not bear a strong resemblance to the text. These two characteristics—thorough analysis and nontrivial transformation—are the hallmarks of comprehension.
如果你对知识进行了彻底的分析而非某种机械的套弄，在你脑中生成的概念与生硬的文字之间已经没有很强的相似性，我们就认为这个概念是被理解的。 彻底的分析和非凡的变换，是获得真知的标志性特征。

— ice1k 的博客...

+ 科学家必须在庞杂的经验事实中抓住某些可用精密公式来表示的普遍特征，由此探求自然界的普遍原理。
+ 爱是比责任感更好的老师。
+ 光用专业知识教育人是不够的，通过专业教育，他可以成为一种有用的机器，但是不能成为一个和谐发展的人。
+ 如果你无法向 6 岁小孩解释它，那代表你自己也不明白。
— Albert Einstein 爱因斯坦

只有做到真正喜欢计算机科学的话，才是真正有效果的学习呦！
有了热爱，才能做到开始的时候不会惧怕那些现在不懂不理解的东西，以及预备好为未来更大的挑战准备好精神基础，不要忘了不管你做什么，你的出发点都是对于计算机们的热爱。 #Statement

虽然有些东西的确很复杂，但是解释，仅仅是解释他们却基本都异常简单，前提是 — 你得足够了解他们！这样你才能画出图、作出比喻和比较、总结出合适的 background，来建设新人的直觉，这些是一个愚蠢的老师根本无法，也可能不想去做到的，因为他们只会想着偷懒。（很不幸，不知道自己在教什么、照本宣科的老师，现在至少在中国不是少数）

+ 背景 0 — 它会告诉你对于类型系统，我这里使用的抽象方式是啥子
+ 背景 1 — 它会和你探讨一些关于 Trait 类型的实际问题，作为一个扩展，不要求一下就懂

因为背景 0 在 Telegram 上已经无法更新，以下内容，基本是 bg0 的续写
==

== Soundness and completeness
这是类型检查器上的一个概念
假设你已经知道什么是程序、什么是类型、什么是程序的类型约束
如果你不知道，参考下面一段程序，这段程序假设你有 "Python 基础" — 熟悉常用数据类型和基础操作 — 比如 print 函数 的理解程度

程序是底层逻辑的组合
编写程序是让你用一些既成的逻辑按一定方法结构组织出一段全新的逻辑，用于解决你的问题

（当然，上面是对函数式编程范式来说，一切皆算法组合，对结构化编程当然也差不多，不过要定义一些数据结构了；当然结构本身也只是程序依赖的描述引用，对面向对象这种披着 OO 外衣的过程式，虽然也搞得蛮学术的，就是一切皆对象）

x = True; y = False; print(x and not y) 这是一段程序，它是由一堆『语句』构成的，语句按出现顺序执行
（编译原理里，它也是程序的特例 — 基本块，这个块里的语句被组合在一起按顺序执行，不会在中途被打断、也只有完全执行和没有执行两种执行情况）
语句里的『表达式』是基本的执行单元；表达式依语法结构不同，执行顺序也不同；执行顺序对程序的结果往往有影响

if input('Y?> ').lower() is 'y':
  print('Accepted')

我们使用『if 结构』和 input 函数, str.lower 方法、is 操作符和 print 函数组织成了一段程序
它判断用户输入是否为 Y 或者 y，如果是，则子程序 print 被执行，向程序输出写入 'Accepted' 字符串

input、str.lower、print 的类型是『函数』，我们可以像 input() 一样在后面加括号『调用』他们
这是你对『类型』的第一印象: 有些东西是 "callable" 类型，所以可以在后面加括号（参数列表）使用他们

assert callable(input) and callable(str.lower) and callable(print)

bool (class) 是 True 的类型：

assert type(True) == bool

type 是 bool 的类型：

assert type(bool) == type

type 的类型是自己，type 是 Python 里的类型。

你现在知道了什么是程序，但还不是很清楚到底什么是类型。在 Python 里，类型可以被理解为集合。
这个集合只有一种操作：is(∈, aka. elementof) 运算符；它没有 add 和 delete 操作；这是这个类型的值(value) 实例的集合

==
上面说的当然是对 Python 这种动态类型的语言来说啦（类型没有类型、只有值有类型，或者说类型检查期是能访问到值本身的）
有的时候也会把它理解为 可用操作（函数） 的集合，比如讨论 trait 类型时，有时候需要判断真子集（比如判断子类型关系时）
不过这里的理论可以作为一个最简单的直觉，只要你还记得集合论的那些操作符（比如集合交并补、真子集超集）即可
实际实践的时候，往往不需要像理论上说的那么检查，有很多的优化适配可以做，理论上所说的有时候往往不能直接拿来当成有效算法
==

assert bool.__instancecheck__(True), "True ∈ bool"
assert not bool.__instancecheck__(1), "1 ∉ bool"

对于 callable 这个类型（它是一种集合，你可以使用一种被称为『是这个类型的对象吗？』的操作），is 操作符被定义为 callable



assert callable(input), "Input function is instance of callable type"

看起来就像你可以问水果店主：
“香蕉”是『水果』吗？ — True.
“萝卜”是『水果』吗？ — False.
香蕉和萝卜是对象 (object), 水果是对象 (object) 的集合，也就是类型

类型就是集合。

我们可以卖给水果店主水果，但是不能卖给他蔬菜甚至锅碗瓢盆！

def sell_fruit(thing: fruit):
  ...

sell_fruit(_) 函数的第一个参数有了一个类型约束：thing 对象必须是一个 fruit
现在你知道了什么是程序、什么是类型，但还差一点：类型约束！

一些『操作』（比如说，『str.lower』只能被提供指定『str 类型』的对象）：

str.lower(2)

TypeError: descriptor 'lower' requires a 'str' object but received a 'int'

str.lower 的『第一个参数』就拥有一个类型约束！它要求一个 'str' 集合中的对象

正类似于你不能卖给水果店老板茄子这种蔬菜，你也不能『将一个数字取字符串小写』
这就是类型约束的意义 — 少出错，它将『必须得执行到那一条语句；str.lower 函数“看到”自己被提供了一个 int 类型的值的时候才能抱怨 — 我不支持这种输入！』时候发生的错误，提前到『类型检查』期间就可以被发现

类型检查的对象往往是一门程序设计语言里的『一等公民』(first-class citizen)
— 函数的参数和返回值 （即便很多编程语言底下都将函数参数作为局部变量实现）
— 值容器，比如全局变量、局部变量、常量

错误被发现并处理的越早，其导致的损失就也就越少！

👆 其实我本来不应该用 Python 这种弱类型语言来讲，你甚至可以写 if 'okay': ... 这种代码... Python 2 就更为混乱了 — True, False = False, True; 看起来 True 和 False 只不过是全局变量而已！

soundness:
考虑一下平时大家使用的『烟雾报警器』 — 还记得吗？那个经常嘟嘟叫的玩意（大雾

void print_string(char *cstr);

这是一个 C99 （C 程序设计语言版本）里有效的函数声明(declaration)，它定义了使用(use)某种函数的基础 — 我们得知道它接受什么、返回什么

因为 C 是一门静态强类型的语言。

设想一下，这段程序正确吗？

char *arg0 = (int) 9;
print_string( arg0 );

这一段呢？

print_string(-1);

他们都不符合类型约束！
第一个程序将 int 类型的实例(instance) 9 赋值给了 (char *) 类型的变量 arg0, 而 C 语言 99 版本没有定义相应的隐式转换规范, 这是不安全的
第二个程序使用 int 类型的实例 9 作为 void (*)(char *) 类型函数的第一个参数，(int) 9 可不是一个 (char *)!

虽然和上面类似的情况在编程实践中可能经常出现，可是很多人都会忽视掉这个事实 — 所谓编译不通过，如果是『类型检查失败』的话，其实类型检查是按照某一种规范来的，而这种规范，是由一门高级程序设计语言的『类型系统』(type system) 定义的

如果一个类型检查器对所有『不符合』类型约束的输入程序，都能给出正确（True）的结果（Positive 和 Negative；表示程序是否符合类型约束），我们称它为『sound』的 type checker

这就是所谓的 soundness

如果一个类型检查器对所有『符合』类型约束的输入程序，都能给出正确（True）的结果，我们称它为『complete』的 type checker

这就是所谓的 completeness

当然对于 True/False 和 Positive（阳性）/Negative（阴性） 的组合，大家肯定也能想到 —
— 第一个 T/F 是程序真正符不符合类型规范
— 第二个 P/N 是类型检查器给出的结果
当然啦，学术界给出的定义正巧相反 — 不是指示程序是否正确，而是指示程序是否有误，这里请大家详情。

sound 的类型检查器不会给出 False Positive — 它断言是无效的程序肯定是无效的；但可能否决掉有效的程序
complete 的类型检查器不会给出 False Negative — 正好相反；它断言有效的程序肯定是有效的，但可能接受无效的程序

随着多态(polymorphic)类型系统的发展和各种高大上类型系统成分（比如 traits）的加入，completeness 越来越成为类型系统检查器实现时需要考虑到的要点

但是根据计算机科学的停机问题（实际上是逻辑问题，Type system 本身也是逻辑问题而已），一个 type checker 不能同时：

+ sound — 命题的可靠性
+ complete — 命题的完备性
+ always terminates — 不论什么输入都一定可以在有限时间内给出结果

为什么 Type checker 却用『命题』来表达，是因为类型约束本身就是一种命题而已：

上面的 Python str.lower 约束，是一种命题，它断言：

str.lower(arg0):
  typecheck arg0 is str

对于 Haskell 的 typeclass 来说，就更明显了