#PLT #Haskell #CS #PL #Papper https://github.com/wh5a/Algorithm-W-Step-By-Step/raw/master/AlgorithmW.pdf

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

#Learn #Haskell http://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. 我找到了一个中文名字的计算机科学程序设计语言理论的教授，现在国内根本找不到他的资料，你们听说过吗？

http://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 什么的暂时忘记或者没学会，因为有些概念我得猜... 是猜啊，有时候形式化定义也不好理解的... 反正需要时间，有误解随便喷吧。不说了