果然还是 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/

看上去有点意思。

#计算机

我一定是闲的无聊了....

默写就不用了，使用了 JQuery 的一些函数基本会用
... 算了还是写一点（

#web #html 之前的盒模型参考这里; 这次花了多久呢... 足足有 20 分钟！太长了呢...

#web #html 使用 JQuery，CDN 是 CDNJS (Cloudflare)

https://duangsuse.github.io/Essay-HTMLs/

1+ 发布