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 来说，就更明显了

== Duck/Statically typed, explicitly(implicitly) typed, weakly/strongly typed

隐式转型 即为隐式类型转换，不管采用何种方法（比如，在不同二进制长度的机器数值之间转换可能需要 extension (bit widen) 或 bit narrowing），（可能依照类型系统）在需要的时候自动地将一个类型集合中的对象映射到另一个类型集合中的对象（也即值, value）即为隐式转型

强类型(strong typing)和弱类型(weak typing)

这是一个相对的概念 — 在程序设计语言规范上
强类型在需要进行类型转换的时候要求程序员显式把类型转换操作写出来
弱类型会在需要的时候进行自动类型转换（比如 JavaScript，点名批评）

强弱都是相对而言的，弱类型语言可能在某些地方对类型有严格的要求、强类型语言亦可在一些地方提供隐式的类型转换
动态弱类型因为其延迟类型检查和可执行操作确定类型的特性也被称为 Duck typing — 走起来像🦆、叫起来像🦆，那它就是🦆！

显式类型和隐式类型
这是一个相对的概念 — 在程序设计语言规范上，如果所有要检查类型的地方都被要求标注上类型，即为显式类型(explictly typed)
否则即为隐式类型(implicitly typed)
有时候这个问题没有直接的是否回答，比如，在一些支持类型推导(type infer)的语言里（比如 Haskell 和 Kotlin）类型声明是可选的

动态类型和静态类型
某程序设计语言规范上的概念 — 类型检查（依据类型约束检测程序是否有效 — well behaved, valid）是在『执行时』“动态地”进行或是在专门的时间里进行（比如『编译』时）
一般来讲时序上越早检查越好，但也不是绝对的（参考 completeness）

程序设计语言类型的显式隐式、弱和强都只是相对的概念，不是非是既非的

下面会说一下关于传统解析器架构的事情，然后是一个简单的 LLVM 编译器

#PL #PLT #Learn 啊~ 既然上面已经有了基本的直觉了，那么下面的就是要来讲：
（当然，其中可能涉及到一些使用我利用在校划水时间设计的 Ra 程序设计语言，目前还没有规范，语言主打符合 PLT 直觉以及函数式编程 / 面向对象过程式均可、小体积、优雅运行时实现）

== Types and values (re) #Haskell

不使用 Haskell 是不行的！（好吧，Haskell 只有一点，更多的是 Agda 的说，感谢 @ice1000 的代码, 好吧，我觉得他不会承认“这”是使用了他最近写的代码，因为太辣鸡了）

类型 (type) 是值 (value) 的集合（至少这里我们还可以这么认为）

(agda)

data bool : Set where
  true false : bool

inv : bool -> bool
inv : {a : bool} {A : Set a} A -> bool
inv : ∀ {a : bool} Set a -> (Set a)
-- a in bool => A is Set of a => inv: Given x of type A resulting type bool
-- A = { true, false }, bool = { true, false }

inv true = false
inv false = true

Zero sized types (Rust 里的概念，仅仅因为它还有点代表性)

比如 Kotlin 的 kotlin.Unit、Rust, OCaml, Haskell 的 () 空 Tuple 都属于 Zero sized type
之所以称他们为 Zero sized types 是因为他们只有一种可能的值 — 不需要存储任何状态，只要拿到这个类型的实例 — 肯定就是这一个值
不需要存储状态，所以无须任何空间分配即可『保存』下这种类型

Empty types (aka. Bottom type)

Kotlin 里的 Nothing 类型、Rust 的 std::never 属于此类型
之所以称他们为 Empty types 是因为如果把他们看作值集合的形式，就是空集 emptyset
如果把他们放在子类型的继承树里，他们位于最底端（离树根节点最远）故也名 Bottom type

这种类型只能在类型角度被讨论，因为他们没有可能的值 — 通常这意味着程序不可能访问到有这种类型表达式的值，比如说得到值的时候程序肯定已经终止运行
即使是在“落后”的 C11 里，stdnoreturn.h 也起了一个类似的作用 — 虽然不是类型理论上的

== Type constructor (Parameterized Types, Variance)

Type constructor 就是接受很多类型（也可能利用柯里化，这样只需要接受一个类型返回一个类型架构器就可以做到多接收的效果）返回一个类型的东西

被称为 Kind

A kind is the type of a type constructor or, less commonly, the type of a higher-order type operator.

比如

Maybe :: * -> *
Maybe String :: *
(->) :: TYPE q -> TYPE r -> *

* 代表着一个类型，比如 (String :: *)

Kotlin 里的 nullable type？为什么不认为是一个类型架构器呢？

Parameterized Types (Generics) and Variance
== Arbitrary operation on types

==== Product (*)

(agda)

data bit : Set where
  zero one : bit

等价 Ra（这里使用 Sum type）

type bit = zero + one where
  data zero, one

也等价 Ra（这里使用 Subtyping）

type bit where
  data zero, one is bit

zero 和 one 都是 Zero sized type；is 为他们定义了子类型关系
type ... where 是 Ra 类型定义的交叉引用语法

二进制。一个 bit 集合的长度 (card) 是 2

type Twobit = <bit * bit>
assert card(Twobit) == 2*2

type Threebit = <bit * bit * bit>
assert card(Threebit) == 2*2*2

<> 是 Ra 程序设计语言的 Tuple （元组）类型语法；Tuple 是 Ra 里的 anonymous product type
它的乘法项没有名字（可以用 0, 1 之类的数字引用第 n 项）。
That's it. 你在 instance level （value level）看也是一样，

assert zero is bit and one is bit
assert <zero, one> is Twobit
assert <zero, zero, one> is Threebit

对字符串也是一样，字符串可以理解为字符（一种 Enum）的数组
Ra 里；数组是 Homogenus Product Type

— forall T. sizeof(T * Unit) = sizeof(T)
— forall T. T * Nothing = Nothing

Homogenus Product Type (e.g. arrays)

Homogenus Product Type 也是不记名的，只能以顺序编号之类的方法引用其项目
与其他 Product 不同的是；Homogenus product 的项都是同一类型；而非任意类型相乘

Ra 程序设计语言里可以使用 ** 语法定义这种类型

type Int8 = 8** Bit
type Int8' = <Bit * Bit * Bit * Bit * ... * Bit>

Ra 里，具名的 Product type 可以这样定义和使用

data Person { name :: Str }

data Student is Person
  { grade :: Nat * class :: Class }

data Teacher is Person
  { classes :: Vec of Class }

abstract fun Person.briefDesc(): Str = "a person called $self.name"

==== Sum (+)

type Either of A (out) = Nothing + Just where
  data Nothing
  data Just { value :: A }

fun (of A) getOr(shim: A)(eit: Either of A): A match eit
  Nothing => shim
  Just { val = value } => val   

Ra 里的 Sum 都是有 Tag 的(tagged union)；利用 Tag 可以区分不同 Sum 成员类型的实例
Ra 也支持声明处型变

— forall T. T + Nothing = T

Untagged union

C 和 Rust (新版本) 支持单单并类型的值集合而不加 Tag，就是直接类型理论上的 Union
C 的 Union 是不安全的；因为 A + B 的 Union "T" 支持 A, B 的所有操作，但 T 值只能是 A 和 B 中的一种

Unit (ZSTs) 好比 product 和 sum 类型里的 1；T*1 还得 T、T + 1 和 T + R 没有区别
Empty 好比 0；T*0 得 0、T+0 还是 T

==== Intersection (&)
==== Union (|)
== Subtyping
参考这里

== Traits
参考这里

== Dependent Type
参考 ice1000 的简历

Π Pi 类型：返回类型依赖参数
Σ Sigma 类型：元组成员的类型依赖其他成员的值

#recommended #blog https://codeday.me/

😐 今天暂时就到这里了，如果觉得太少了的话也可以去隔壁的欢乐谷看看《好耶，是形式验证！》

程序设计语言类型扩展起来说多了还是逻辑... 逻辑... 逻辑...

类型是什么？类型就是对程序逻辑本身的高层抽象



; one = λf x. f x
(define one (lambda (f x) (f x)))
; two = λf x. f f x
(define two (lambda (f x) (f (f x))))  

(define inc-abs add1)
(define zero-abs 0)

(define to-number
  (lambda (coded)
    (coded inc-abs zero-abs)))

(define result (+ (to-number one) (to-number two)))

👆 意义不明确，但是可以观察到函数式编程用 abstraction 的时候类型有点被抽提出来的感觉...

对一段程序而言，没有比它本身更好的描述它类型的方式了（这也是为啥 Python 这类语言没有被称为『无类型』 "untyped" 语言，因为它实际上是将类型和程序逻辑本身绑在了一起，只能边执行边检查），而类型系统尝试以更简洁有效的方式对特地用途（类型检查）描述一段程序

类型也是逻辑。

看完上面这些资料（我可花了整整一个假期... 的四分之一来写他们啊！）以后，你最大的感想应该是：

我艹，这些都真 TM 的好好玩啊！

如果不是，请擦亮眼睛再仔细的阅读一遍，直到你觉得他们很 excited 🐸 或者放弃为止

当然，你也可以完全跳过和我这种喜欢一遍一遍辣鸡重复强调的普通人（而不是天才，我觉得冰封很天才，而且除了他我不认识其他同龄同水平的 PLT 爱好者，可见就是所谓的 PLT 高中阶段中国，哦不是中国留学第一了呢，说不定）一起学习的话，也欢迎去隔壁冰封岛和众多知乎真·大牛那看看

如果无视自然发展规律的话（今天在乡下放牛，第二天就站到 MIT 台上讲学尖端量子物理走向人生巅峰，我觉得即便是天才也是不可能的，这被称为“童话”）

#PL https://ice1000.org/languages-cn/#covscript

现在我想起来 CovScript 那个 Parser [include compiler.hpp]... 想想还蛮符合直觉的?
@LEXUGE 在写化学等式解析器的时候也写出了一样的程序算法...

说实在话，我觉得他写的这个... 还真的很复杂，真的，我甚至看了好一会还找不到很多我认为有的东西被放在哪里

https://github.com/covscript/covscript/blob/8c32e7593097c59b3bffc3540209aa6f79c7cbc1/include/covscript/impl/compiler.hpp#L54

这里他还写了个自动机... 虽然我现在还不想从 eval 函数开始找解析过程，但我已经找了好一会还不清楚解析器的是什么样的，说明要不然 CovScript 的解析器架构我不熟悉要不然它太复杂了，不够简洁易理解
即便只是预先处理词条们，自动机（但是无状态）这种方式... 我都没有想出来过，因为我一直在用 Stream 的... 而且 cs 所谓的 compiler 其实基本上还包含了半个 parser 的代码... 而 parser.cpp 里却只是一些辅助 compiler.hpp 工作的方法实现...

我想如果我是第一次写，我也会想出把词条线性表按优先级拆分（在 C 里面就是直接走指针运算）然后子程序下去规约的形式... 🙈

虽然现在我是直接使用递归下降法在词条流上解析二元表达式组。

总之等我同样是自 GC 的 Ra 语言定义好实现了再看吧，现在稍微有点感觉了.... 但还是很累，总感觉可能在词条列表本身上一遍一遍做了很多处理，不是一次完成解析的

#GNU GIMP 好像就有这个功能(XPM) 的说

https://t.me/one_real_world/1809

https://javl.github.io/image2cpp/

看上去有点意思。

#计算机