顺推 #PL #CS #PLT #Learn StackOverflow 这个问题（Soundness and completeness of systems）的回答

Soundness prevents false negatives（假阴性） and completeness prevents false positives（假阳性）.

In modern languages, type systems are sound (they prevent what they claim to) but not complete (they reject programs they need not reject).

Soundness is important because it lets language users and language implementers rely on X never happening.

Completeness would be nice, but hopefully it is rare in practice that a program is rejected unnecessarily and in those cases, hopefully it is easy for the programmer to modify the program such that it type-checks.

Type systems are not complete because for almost anything you might like to check statically, it is impossible to implement a static checker that given any program in your language
(a) always terminates, (b) is sound, and (c) is complete.

Since we have to give up one, (c) seems like the best option (programmers do not like compilers that may not terminate).

— Robert Harvey

我没彻底理解，感觉总而言之，类型检查系统里，soundness 就是让通过检查的程序不可能是突破了类型约束的（但是有些符合约束的程序会被误判为『positive』有问题的），而 completeness 就是让类型系统尽可能『智能』一点，允许实际上符合约束的程序通过编译

而由于某知名的确定性问题否定答案『停机问题』
不可能太做到完美（逻辑上是不可能的）
(a) 编译器（检查器）能得出结果
(b) 实现是 sound 的
(c) 实现是 complete 的.

只能抛弃一个，所以就抛弃最不需要的 completeness 了
Java 8 里泛型的形变就是一个例子，可能吧（也可能不是，因为这类类型理论往往和 Agda、Idris、F* 之类的完全完全不 Industrial 的语言有关

List<Integer> 其实可以是 List<Number> 的子类型（换句话说，List<Number> 类型的容器可以容纳 List<Integer> 类型的值），可是其实不是，还非得 PECS 原则改成

List<? super Number> ls = new ArrayList<Integer>();

Kotlin:

val ls: List<Number> = ArrayList<Int>();

（因为标准库里处理了泛型型变问题）

才 check，不过这貌似是 generics 的 variance 问题，所以可能和这类无关，要想得到更准确的知识得问大佬

"Don't block, Keep Moving!!!" 🏁

#China #life

首先我们说说那个乘公交车『接钱』的问题

通俗地讲就是说你搭公车，结果带的钱不是不够，正好一张大约 5 块左右的整钱无法找开，因为现在公交没有售票员了，只好自己找钱的意思

for example:

小明一人搭公交车，手上 5 元人民币，票价一张 2 元

小明将五块钱投入收款箱，我们认为现在他手上有 2.5 张票，因为票价一张 2 元，半张就是 1 元

首先来了一个现金付款的吃瓜群众，小明对其说明情况后吃瓜向小明付款 2 元购买到车票（其实不是实物，不过可以认为是）

然后又是一个吃瓜，小明又是如是一通，这名乘客向收款箱里放了 1 元钱后给了小明一元钱（来购买另一半车票）。

所以这个问题里我们讨论的粒度实际上是半张车票，或者说，可以把它视为一张车票，不过那样一人登车需要两张车票
然后这个对象我们可以付钱（给箱子、给别人）买，也可以随便卖给别人，就这事。之前我妈教我的，推荐不要使用。
中国人并没有网上说的那么团结，除非是在围观跳楼起哄的时候，怪团结的。呵呵。真棒。

（一转攻势）想到这里的时候我突然悟出『教学半』（教人是学习的一半，或者说，不教人你就只得到了一半知识）

（我好突然啊）

因为教别人需要你对某种知识有更深刻的理解，这种老师才是好老师

如果不是，就会像某本最近很火的前端开发书一样，把分词和预处理、编译和预编译、解析器和解释器都混为一谈...

普通的程序员也可以教别人啥啥框架怎么使用，但只有看破框架层的东西的人才能写出好教程。

好比老师教人植树，不好的老师只看到表象，授人以鱼（树木长势好坏的外观，好比给人编译好的程序）

而好老师看到本质授人以渔（树木长势好坏从它的根部，暗处来判断（透过表象看到本质，透过因变量看到引起变化的自变量），好比给人程序的源代码允许进一步研究扩充）

即使是在讲比较浅层的知识时易学性也比不好的老师高，因为他们真正了解自己讲的事情，从整个算法流程和结构图广度来看都是

最重要的是好老师一般都是好学生，他们知道如何学习最好，效率最高
哪些方法自己理解的快，哪些表示方法理解慢容易混淆误记，所以他们拿捏得当，教人起来也更为游刃有余一些。

然后我们说说这周的 #task 们：

首先是 Pickle 点名器（因为我注意到了可以加新特性，然后我又多花了点时间重新设计了一下，包括添加 Lua 脚本引擎来扩展和『函数库化』这个程序以增进扩展性），不过现在老师找到新欢了（seewo 那的某个课堂优化大师挺好用的，官方逼死同人啊...），算了等寒假吧

其次是扒谱（昨日青空），这周本来的任务。

讲笔记。讲完了（好吧还有几个）。因为我刻意没有记啥笔记，成天队列溢出太烦人了。

最后还有一件事和技术无关的，我决定在 @dsuset 里说。

其实我在学校里又考虑了一下 H2O2，显然 H2 这次不会和 GeekApk 一样失败了，我现在至少也是有一点工程能力的。

H2O2 带回了之前一些基本的设计，我又考虑了一下 GitHub 什么的... 包括 Telegram 不过之前已经有了，H2Link（GA 里叫过 GFC、GeekURL）、H2Inline（GA 里叫过 EFC、GeekCode）、虚拟依赖系统，还有之前因为我智商不够用（以为只能通过 PRIMARY KEY 过滤数据）导致没有 Tag 系统的问题（当然 Categories 还是会有的），现在都改了。学了一点 PL （程序设计语言）理论以后设计和文档只会更优雅更直观的表述问题的本质，双氧水，寒假见。 <3<3<3

另外就是我打算以后有时间的时候出一本 CS 相关的入门书籍 #book 《与小鸭 Doddle 的神奇 #CS 岛历险》（Magical Adventure with Doddle on the CS Land）

故事里 Doddle 是一只有神奇魔法的鸭，年龄和姿势水平深不可测但是看起来只是一只普通的看不出年龄的鸭子，带着一顶名为 λ-hat 的帽子，背着能自己漂浮的魔法棒

与主角 编程兴趣班学员 Mike 在书店里相遇，Mike 在各种 Android 开发、小程序开发、Web 前端、全栈工程师的疯狂浪潮里突发奇想选择了僻静的 Computer Science 书架，买回家里，打开 PL 理论书本 Mike 发现书面上的鸭蛋图画突然消失，从此 Doddle 走进 Mike 的生活，Mike 选择了不止步于应用层开发，Doddle 带着 Mike 走向 CS 圣地。路途遥远有高峰也有隧道，Mike 究竟会遭遇什么、学到什么呢？

不过肯定是我买了数位板之后的事情了，因为我还要在里面插入漫画，类似 Realm of Racket，这是讲述故事和知识的，非常青春（迫真）（其实最开始我的想法是... 开心？不过我觉得... 其实给现在高中大学类似的看也好，因为智商高一些方便理解）

#Mathematics #PL #Math #learn

+ 数学上的分段函数

还是看 PDF 吧。TeX 命令也可以贴不过我懒得贴了（因为我想找在线的即时预览编辑器，没找到能用的 hhhh

https://cn.overleaf.com/ 慢死了

116 面 e6. Haskell. 等价，虽然我不是特别熟悉 Haskell 所以有余赘

p(h) | (h >= 0) = 7 * h
     | (h <= 40) = 7 * h
     | h > 40 = 10.5 * h - 140

或者我们可以更 less-boilerplate 一些，利用 Haskell 的 range

p h
  | elem h [-1/0..40] = 7 * h
  | h > 40 = 10.5 * h - 140

好吧，这个不会 terminate，因为我用的是 -Infinity... 而 Haskell 不知道我到底想说啥... 因为我也不咋会 Guard pattern

main = print $ p <$> [0..300] 然后至于数据画函数图像嘛可以随便找个软件比如 LibreOffice 什么的，KDE 也有转们的软件，要不然 Kotlin JavaAWT JPanel 也可以。

让我们再看看 Haskell 里的 Guard pattern
是类似的。不过这里 Haskell 的分布函数有个 branch exhaustivness check 的问题，比如 Fib 函数

fib 0 = 0
fib 1 = 1
fib n = fib (n-1) + fib (n-2)

main = print $ fib 1

但这个 Guard pattern 版本

fib :: Int -> Int

fib n | n == 1 = 1
  | n == 2 = 2
  | otherwise = (fib n - 1) + (fib n - 2)

main = print $ fib 0

不 total（完全）（比如，输入 -1 就没有值），不 check。（咦？怎么能过？不 sound？）（之前 GHCi 过不了就是）

那么一定要用就可以上 undefined（

+ 啥是 tailrec #Haskell #functional

首先啥是递归

Y = λf. (λx. f (x x)) (λx. f (x x))
(Y Y)

我们先来进行 β - 归约... 算了看过程

首先我们 f (x x) [ f := Y, x := (λx. f (x x)) ] 看不懂算了，因为数学的东西就是为了形式化，不易读的... 所以不数学算了（

(λx. f (x x)) (λx. f (x x)) where f = y 被替换为 (λx. Y (x x)) (λx. Y (x x))
然后接着展开... 唉头大，总之，类似这样就可以了，学个一半然后自己再学也没什么

(λf. (f f))
  (λself. (self self))

首先 apply

(λself.

... 到

(lambda f.
(λself. (self self))

(λself. (self self))

apply... (self self) where self = (λself. (self self))

((λself. (self self))
(λself. (self self)))

又是它。无限循环。infinity recursion。结束分析....

然后看看这个 ES6 #JavaScript 的 tco 优化器，汲取灵感 <del>所以 ES6 还是很 functional 的</del>

function tco(fun) {
  var value = null, active = false, accumlated = [];
  return function accumlator() {
    accumlated.push(arguments);
    if (!active && (active = true)) { // 是的，我利用 && 非短路语义压行了
      while (accumlated.length != 0) value = fun.apply(this, accumlated.shift());
      active = false; return value;
    }}} // 是的，Sexp 系写多了的结果...

sum = tco((x, y) => (y > 0) ? sum(x + 1, y - 1) : x);

console.log(sum(1, 100)) // 101

然后我们看看这个伪代码例子

type <A : Comparable<in A>> binarySearch : |A[]| |A| |Range| Int

binarySearch xs o <srch = xs.indexRange> = |>
  let index = srch.mid, guess = xs[index] in when
    | srch.len zero -> nil
    | guess is o -> index
    | guess > o  -> tailrec(srch.a..srch.mid.sub1)
    | guess < o  -> tailrec(srch.mid.add1..srch.b)

tco 就是尾调用优化，如果一个函数的最后一步是调用自身或者兄弟函数（这个 case 目前请无视）就可以进行尾调用优化
这样调用栈帧就可以不保存，就不会 ~~上~~ 栈爆 ~~Stack Overflow~~ 了
其实我们发现这种递归可以优化为循环的（试试用循环 + 变量解决它），所以 tco 允许我们用递归的方式写循环

+ 过程和结果。副作用和返回值

有的时候我们更注重过程而不是结果，比如... 比如... （突然害羞）（迫真）生活中例子很多

比如....

puts "Hello, world!" #=> nil

class Foo; end

macro_rules! foo {
  () => { "foo" };
};

`

nil 我们要你何用？
() 我们要你何用？

我们要的是 puts 调用产生的副作用，向 STDOUT 写出一行你好世界
我们要的是 class Foo 的副作用，定义一个 Foo 类赋值到 Foo 常量上
我们要的是 macro_rules! 宏的副作用，它把一个用户定义的宏注册到系统里面去以便使用

副作用在很多语言里都是 invisible 的，只有返回值和异常什么的可以在抽象函数调用之间传递
这也一般无可厚非，因为很多时候我们不要返回值只需要副作用而已，他们两个还是很不一样的

不过 Haskell 这完全 pure 的语言里面有 IO 类型，不过 @ice1000 都说他啥时候还觉得 Haskell 的 IO 不好理解我也不敢随便说话了

纯函数就是没有副作用的函数，一般数学函数都属于此类，纯函数不是什么不用 printf 也不是什么不用局部变量，它是说

+ 函数本身运行稳定可预期
+ 函数的运行不对外部环境产生影响
+ 函数的数据流全是显示的，就是说函数与外界环境交换信息只能使用它的参数（包括 this）和它的返回值

纯函数的好处是
+ 无状态，无需考虑线程安全
+ 纯函数的组合还是纯函数
+ 相同参数永远相同结果，可以缓存计算结果、延迟求值、改变求值顺序、改变求值环境、多次求值也可以随意

当然别处还有更严谨的定义，不过我不纠结这些就是了...

+ 扫描到树状图以及输出（挂起中，因为... 还有事...）

... 因为 UNIX 的 fs 文件系统都是比较方便的吧... 我们拿这个做例子快点讲了好办事

Haskell. 我们先来看看我们的需要的 API 抽象

``import System.Environment
import System.Directory
import System.IO

lsdir :: FilePath -> IO [FilePath]
lsdir = listDirectory
fexists :: FilePath -> IO Bool
fexists = doesFileExist

data FTree = FTree [FTree] | Atom FilePath deriving (Eq, Read)
ftree :: FilePath -> FTree

instance Show FTree where
show FTree fs = show fs
show Atom fp = show fp

ftree = undefined

首先我们需要一个 API 来拿到文件夹子树

listDirectory "." >>= print

然后我们需要一个 API 判断『对象（路径表示的）』是文件还是目录（里面还有文件）

doesFileExist "/proc/cmdline" >>= print

`OK. 那么我们来实现 `ftree`

#life #school #China #dev

没学过 Kotlin

现在一直没有学习新语言的勇气和精力..

多读书，多看报，少吃零食，多睡觉。

GraalVM 现在连 Minecraft Server 貌似都跑不起来？

太真实了

我到现在也没学 EE..

#Java #sysadmin #docker #linux

maven 其实我不太懂，似乎没有版本管理？