#Haskell #PLT https://github.com/bgamari/the-thoralf-plugin/blob/master/src/ThoralfPlugin/Convert.hs

#Learn #Haskell https://learnyouahaskell.com/syntax-in-functions

#recommended #IDE #dev https://ice1000.org/2016/12/24/Ligatures/

#Github #Haha https://github.com/nikolas/github-drama

开启看戏模式 😝

#Media #CS #CG https://github.com/xlnx/cuda-raytracer

#recommended #friends #blog #share #CS #Haskell
https://imkiva.com/

这是 @imkiva 的博客，imKiva 曾经使用 C++ 开发过一个自己的 JVM（当然，这个说法不规范，理解万岁）

https://ice1000.org/2018/11/23/MultiDimentionalSyntax/

因为和 InScript 的缩进语法相关就发了这个链接 #PL #Parsing #InScript

#telegram 有一个频道主动临时 mute 的功能『静默广播』，不然订阅者们可以选择自己 mute 掉频道通知。

之前 duangsuse 的朋友们一直都是采用这种方式，不过，现在 duangsuse 决定：

只有偏向工程或者容易理解的广播、分享才以提供通知的形式发布

所以 mute 此频道的部分软件工程师 subscriber 们可以选择 unmute 了，不过普通用户来说可能没有吸引力（

≪last pinned

之前以为 Docker 那个很高大上的… 后来看了 Trumeet 的 AOSP Build Docker 容器脚本才知道也可以很 trivial，看了一遍有啥简单命令都记下来了


WORKER DIR path
-- fix：其实是 WORKDIR
ENV name=val
RUN shell
ENTRY POINT command argv
-- fix：ENTRYPOINT

-- 更多
ADD srcUri dst
FROM parentDockerCoordinator
CMD argVector

世道不古啊，曾经 MSDOS 时代 Geek 们人手一个 debug，汇编反汇编读写磁盘扇区二进制编辑内存转储样样全能，会批处理的、知道计算机结构的数不胜数，现在呢？都在和锤子苹果 NodeJs PHP/Laravel CSS JQuery Vue ReactiveX SAM'Lambda-sugar frontendViewRouting Iterable#map、#filter Symfony trivial'J2EE 混，还基本理论核心思想基本原理规范都一无所知，Kotlin 看两行代码知道和 Java 控制流、定义语法有啥基本区别就立刻上手完全无视掉特性上的天壤之别，各种功能特性到处滥用好像不用就不知道你会一样的，TC39 又弄一大堆混杂新词法语法，不知道那群前端又要搞出什么新花样来了…，Gradle 使用的 Groovy 被当成 markup 纯数据描述的标记语言写，Gradle 到底是哪种工具做什么用的如何构建项目不知道，最害怕学习新语言和新框架，C/C++ 水土不服到处访问悬垂指针空指针内存泄漏工程五年 C++ constexpr 关键字都不知道，位是什么 32 位 64 为为啥不是其他浮点数是怎么表示 unsigned char 是几位长度不知道，啥是 class path 啥是 class loader 不知道，一个看似高大上的『依赖注入』术语其实就是 OO 基本多态 concept 就厉害得不得了而且特别喜欢创造术语以彰显其专业性，成天研究各种开发 bug 汇报统计分析框架各种 hot fix 热修补热更新增量更新 patch 几行 linear 到死的 proguard argVector 混淆加固，泛型协变逆变不知道，Kotlin in out 泛型约束全靠 IDEA 自己推导、连 PECS 是啥都不知道，各种系统资源特点、线程调度，高性能计算、并行计算、线程安全线程同步、锁不知道，文字编码、浮点数、文字栅格化、渲染参数、精调、字体覆盖替补、排版算法，完全一无所知，只靠 IDE 和 Searching Engines 和各种贴代码的博文都可以活… 看得懂就写的出来… 可是能写出真正算法的，看到了藏在高级程序设计语言文法字面后面数据结构和解释算法的，又有百分之几呢？

阅读 -> 编写 -> 理解 -> 创造

很多人终生就是码农的层次了，终生只是个蓝领程序员，可惜啊可惜…

刚刚碰到一个 case，朋友在做一个模拟登录获取信息然后 OAuth2 给其他应用用的项目，结果刚刚做安全检查的时候拿 U123456 P123456 登上去了。检查之后发现是被模拟登录的系统刚好有一个 ID 123456 密码 123456 的用户🌚可以说是非常精彩了

之前某儿童编程平台还把默认密码设为用户手机号前六位呢，which 同时也是用户登录账号的前六位（后端泄漏了用户手机号…

我这种非网络安全系的弱智都能弄到几 k 电话号码，可惜现在各种底层的东西防护做得比较到位了软件健壮性漏洞也不容易出了，应用层真是喜事连连，唉…

#net #recommended #tools https://github.com/jagt/clumsy

这个工具可以用来模拟网络稳定性状态环境，一般无法做到『优化』，但可以让环境变得更差

#unix #tools #recommended https://github.com/sharkdp/bat

果不其然是 #Rust 程序员设计的，他们最会搞这种扩展版本的 UNIX 系统工具了
也只有 Rust 程序员这么有设计和包装觉悟，而且还有能力开发这种有点算法和底层知识要求的项目

https://zh.wikipedia.org/wiki/%E4%BE%9D%E8%B5%96%E7%B1%BB%E5%9E%8B

https://www.idris-lang.org/

https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html#introduction-to-agda

这 Dependent Type 的资料，不过我这次是<del>伸手</del>问了... 虽然没几个知乎大佬有能耐答这类玩意，因为其实我还是很喜欢这些类型数理逻辑理论的，虽然我目前基本函数式也不是太会，由此看来其实 wikipedia 大佬们是蛮厉害了，各种 CS 理论都有翻译，好耶。

USTC 学生弄的那 Type safe printf 被喷是垃圾（或者是我弄的东西被喷是垃圾），不过我也觉得是垃圾就是了...
因为这个例子看起来就是伪代码一样的，也编译不过...

#PLT #CS #learn #Agda duangsuse 来和你们说一下目前学到很简单很简单很基础很基础的逻辑类的知识，下面的都是 Unicode 表示，不是 TeX

= 这些是 Java、Ruby、Kotlin 程序员们能用到的部分 =

是什么呢？就是 Any#equals（相等性判断）要满足的基本属性，现在一些不 trivial 的 JVM 工程书本上都有教。

我们假设下面的代码示例都有 val a = Any() 的环境

+ 自反性（reflexive）

a.equals(a) 只要 a 不是 null（当然，Kotlin 里 Any 容器的取值不可能是 null），就应该返回 true

数学公式 ∀x. x R x （TeX 代码 \forall x . x \mathrel{R} x ）

+ 对称性（symmetric）

假设有一个对象 b.equals(a) == true 那么，a.equals(b) 也应该为 true

数学公式 a R b → b R a

+ 传递性（transitive）

假设有对象 b.equals(a) == true, c.equals(b) == true 那么，a.equals(c) 也应该为 true

数学公式 a R b → b R c → a R c

btw. 面向计算机科学的偏序理论里，集合 X 上的二元关系 ⊑ 同时满足自反性和传递性时被称作一个前序（Preorder）

btw. 偏序理论里，前序只需要再满足反对称即可成为一个偏序（PartialOrder）
反对称（antisymmetric）的公式是 a R b → b R a → a = b
就是说，a R b 对称蕴含 a 就是 b 这种理论，举个例子，数学上的 + 是对称的，数学上的 - 是反对称的（可能吧）

+ 一致性（consistent）

就是说如果参数（包括调用接受者本身，就是说 this）相同，不管调用多少次 equals 都获得相同的结果，就是说它的数据输入输出流全是显式的，是纯函数。

IDEA 现在能给你实现的 equals 函数推荐这个 pure contract 就是这个意思

= 下面的不保证是有用的 =

btw. 我找到了一个中文名字的计算机科学程序设计语言理论的教授，现在国内根本找不到他的资料，你们听说过吗？

https://www.cs.rhul.ac.uk/~zhaohui/ 这个好像是姓罗的 professor

https://zh.wikipedia.org/wiki/Agda#cite_note-3 — 从这里看到的，弄的啥 UTT （Unified Theory of Dependent Types）

他这本 Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science

现在还在收 PhD 学生你们要不要去啊（逃，跟你们开个玩笑，因为我知道本频道没有正好要留学并且对 PL 感兴趣的

《CLR via C#》、《Kotlin 极简教程》这些书上有讲。其实有时候发现这些玩意还是蛮好玩的，只要理解不出问题就可以
而且又能增长见识，如果有时间，看看这些东西，多好。
然后我又单单发了这些偏序理论，函数式的基本理论懒得发了，其实有些东西还是要自己看书，不好理解就多看几遍，没人能替你理解。

所以我最后看了一个上午就会写这一点破烂 Agda 代码，都是 refl(ective) 的相关证明，就是那种即得易见平凡都算不上的那种

我也不知道是背下来的还是学下来的（笑），但我相信即使现在只是背下来以后也真的能学出来（

顺推冰封专门给 Agda 入门写的书 《好耶，是形式验证！》 （可惜他写了你们也没人看，你们非常满足于自己平时所写的那一点写出来立即就能体验到日常使用他们快感的『源于生活去向生活』前端应用和 Web 后端，笑）

btw. 自豪地，我也有能力写书，不过我之前写的那 Ruby 入门的确是 LibreOffice 排版的，有点不像书。其实 TeX 这玩意也蛮好玩的，中文排版也做得，虽然我不会自定义命令但还能用

data _≡_ : {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x

_≡_ refl refl = refl

{- 下面是对称性 a R b → b R a -}
symm : ∀ {a b} {A : Set a} {B : Set b} → (a → b) → (b → a)

{- 下面是传递性 -}
trans : ∀ {A : Set} {a b c : A} → (a → b) → (b → c) → (a → c)

{- 下面是 Functor -}
⋙ : {a b} {A : Set a} {B : Set b} (f : A → B) {m n} → m ≡ n → f m ≡ f n

如果写错了 Agda 不 check 过就算了，反正我也是弱子状态
with 语法、类型构造器语法、类型签名、Coinductive data types GADT、充要条件、dot pattern、rewrite 什么的暂时忘记或者没学会，因为有些概念我得猜... 是猜啊，有时候形式化定义也不好理解的... 反正需要时间，有误解随便喷吧。不说了

顺便借着这类『静态证明程序正确性』的广播再讲个笔记，是关于预测未来是否能实现的 #file #life #science #PL #CS

我也看过一本和『时间操控』有关的小说，和另一部有名的电影：《时间深渊》和《星际穿越》（btw. 就是著名『墨菲定律』的出处，我开始不记得这名字了然后 科幻电影 女儿 木星 常数 时间 几个关键字一查居然知乎专栏找出来了）

顺便推荐 #book 时间废墟，这么随便乱搞时间，其实是暴露人性相关的也很好看，但是成真了以后未必好玩。

他们都有一个经典的观点，就是四位时空里，『时间』也是一种维度，然后那个维度的生物可以随便操纵时间维，反正就可以理解为我们是鱼肉，他们是刀钜，他们是玩玩偶的人我们是木偶就可以了。

咱们今天就来聊聊时间和人类意识相关的东西，虽然我只有高二的水平... 正好么，反正『不识庐山真面目，只原身在此山中』，<del>100% 的正确率谁也不敢保证，10 分钟你看不了吃亏你看不了上当</del>，无法证实的猜想只能是猜想罢了。正如一个权限受到限制的应用程序也不可能知道 Ring0（内核层）的一些事情（诸如当前的 proccess vector）一样，我们这个受到限制的视角也很难做到什么全知全能。大家开心即可。不管说啥唯物主义啥唯心主义，目前保持好好活着的态度即可。政治和道德人伦理性感性都正确。多好。

为什么听我讲...
1. 我觉得我讲得很接地气你们都听得懂
2. 这是程序员给程序员讲的，灰常适合程序员
3. 你们不觉得程序员是个很厉害的职业么？日常工作之中使用各种高大上充分体现人类智慧的理论
4. 你们闲得没事（对于学生党来说就是说你们因为课业繁忙没有时间写代码但还有时间看小说那种），而且这事情有助于开阔眼界增长见识，虽然可能是我臆想编造出来的

无论你有多聪明，无论你的理论有多完美，如果不符合实际，那么它就是错的
— 物理学家 理查德·费曼（Richard Phillips Feynman）

不过有些东西太难以估测，我们这里不说四维时空这种让 Iterable<Frame> 完全变成 RandomAccess<Frame> 的东西，因为如果真的可以随机访问，理论上四维时空真的是可以操纵一切的，并且不会出类似停机问题这种『确定性问题』

首先咱们还是 <del>两句不离老本行</del> 说说啥是维度

在数学里，维度就是... 好吧我不知道，某度百科说是 独立参数的数目
Wikipedia 是最好的学术交流资料

在物理里维度就是 ::

data class Dimension4<R, T>(var x: R, var y: R, var z: R, var t: T)



import java.util.Date

typealias Dimension<R, T> = Dimension4<R, T>

>>> Dimension<Int, Int>(0, 0, 0, 0)
Dimension(x=0, y=0, z=0, t=0)

>>> Dimension<Int, Date>(0, 0, 0, Date())
Dimension(x=0, y=0, z=0, t=Fri Nov 30 16:00:20 CST 2018)

就是说这是个四维元组（就是有四个项目的匿名结构体 struct），三个是（R 类型的）『空间维』，一个是（T 类型的）『时间维』
当然这种简单的泛型使用其实不算什么技能，可以单纯把泛型当成是一种“类型参数”即可，这里不讲泛型，你们可以假设我往 <R, T> 里填 <Int, Date> 的时候某个 data class 里的 T 类型变成了 Date，R 类型变成了 Int
这里不考虑泛型的协变（Covariant）和逆变（Contravariant）的问题，理解万岁

在生活里，维度就是我们对相对位置的简单抽象，拿各种游戏引擎做 2D、3D 视频游戏的同学们肯定非常了解（当然喽）

type XY = (Int, Int) deriving (Eq, Show) -- 二维
type XYZ = (Int, Int, Int) deriving (Eq, Show) -- 三维
type XYZW = (Int, Int, Int, Int) deriving (Eq, Show) -- 四维

这是一个简单的『抽象维度』，当然不要问我为啥不用泛型（当然我也不知道 #Haskell 里这叫不叫泛型 generics），示例而已

然后是数组了，很多语言，哪怕是很早期的 Fortran（真的是很老了，1953-1957）、Lisp（1956 年的版本）、Basic 都有等价于数组（Array）的数据结构（或许 Lisp 的部分不等价，我听说 Lisp 基本都用的是链表...），一般数组实现是使用物理硬件内存上一块连续的空间的（当然由于某些原因也可能不，不过一般都是，我们称这段连续的地址空间叫『buffer，缓冲器』）

数组的维和元组的维差不多，假设我们有个 int fib_first3[3] = {0, 1, 2};，就可以说这个（全局符号） fib_first3 是 3 维的 int 数组，因为一个 Integer 在 64 位机器上是 8 字节（一字节 8 位，4 字节 32 位，8 字节 64 位），这个数组可能需要分配 8 * 3 = 24 字节的 buffer 来容纳它（一些机器还有字节对齐的要求，要不然可能直接崩坏掉 fault 或者造成速度严重降低，为什么降低可能是数据转送要额外步骤或者缓存问题造成的？）（比如你们常用的 x86 架构上的 CDEF 标准，要求对齐到一个字（4 个字节），而这数组就会浪费掉一个字节）
（看不懂是肯定的，因为我写这个不是为了教你们 C 语言和 C 运行时相关的知识）

而一些语言，诸如 C/C++/Basic/C# 还支持交错数组（jagged array）（就是说数组的数组）（搞 OI 的肯定不陌生“多维数组”这个名词，不过我觉得有点混淆的意思就不用了）

int matrix_dim22[2][2] = {
    {0, 1},
    {1, 0}
  };

printf("%i", matrix_dim22[0][1]); //> 1

不过这就是维嘛... 总之就是一个有序的集合。

下面进入正题之一，预测未来的可能性，然后我们再来说说几个问题。

第一个问题是理发师问题，大家想必都听过
第二个问题是停机问题，想必大家都没听过
第三个问题是外祖母问题，这个大概都听过

总结来说：三个都是悖论（好吧，可能有的不是？

我想说的是这个『确定性问题的否定答案』停机问题

我们知道停机问题在图灵机等价的演算模型（比如 lambda 演算 和生命游戏）上都是不可判定的，在逻辑上根本无法在非 infinity 的时间内得出答案或者从实际出发没有答案 — 等算出结果太阳都没了的那种

在简单幼稚的程序设计语言类型里有种类型被称为 buttom type『底类型』
在 subtyping 里，它是所有类型的子类型，因为这种类型根本不可能有实例，这样没有实例的类型当然就可以作为任何类型的子类型喽，检查不出任何问题

在 Kotlin 里面，这种类型叫 Nothing，和 Unit 不一样， Unit 是一个 object，它只有一个实例，而 Noting 则是一个没有实例的类型
在 Rust 里，这种类型叫 never，就是永远都不可能拿到对应值的意思
在 Java 里，这种类型叫 void（不过 JVM 内部的说法是它不是类型，叫 VoidDescriptor，不过，这里当成类型算了...），此外，Java 里有 Boxed 装箱上的 java.lang.Void 类型，它只可能有一个值 — null，因为你拿不到 void 的实例

当然这类理论最好还是推荐冰封的 Agda 博文看看

比方说，在 Rust 里面我们可以定义一个完全不会返回 _Noreturn 的函数 exit_now，因为此函数在求值时会调用 ::std::process::exit，整个进程都退出了，同一个进程里的代码根本拿不到此函数的值：

fn exit_now() -> ! {
  std::process::exit(0);
}

当然你也可以不把返回值 never 写出来

在 Kotlin 里 throw 表达式也是有返回值的，不过类型是 Nothing，因为抛出异常（求值赋值操作右值 throw RuntimeException("Interrupted!")）的时候整个栈帧都 unwind 了，赋值操作根本没有被实际执行，函数异常终止执行，没有返回值。

val a = throw RuntimeException("Interrupted!")
// error: 'Nothing' property type needs to be specified explicitly

val a: Nothing = throw RuntimeException("Interrupted!")
java.lang.RuntimeException: Interrupted!

println(a)
error: unresolved reference: a