另外 #fix 再说一个问题，就是我这里提的这一条其实是我的误解 #Android

至于这一条呢，是我在《Kotlin 极简教程》上注意到的，并不适合这种情况，是我误记了

它是说 Kotlin 的 Any（因为 Kotlin 开始就没有只考虑 JVM，后来还有 KJS、KN 呢，所以 Kotlin 自己语言层面的一些东西不单单在跟着 Java，如现在的一些 Kotlin JVM Developer 们的日常，Kotlin JVM 要 Kotlin 反射还得加依赖还是什么的）没有 Java （就是 Kotlin 的 Any? 和 Any 映射到 java.lang.Object）的 Object#wait Object#notify 这种锁同步工具 Kotlin 里就不推荐了（因为 Any 类型里面没标这些方法虽然 JVM 运行时里是有的，Object 对象当然能响应这些调用），推荐使用专门的并发编程工具比如 java.util 里面那些

后面那句说的就是可以加 (o as Object) 强制转换到 java.lang.Object （原来的类型是 kotlin.Any）来使用这几个方法

而 Trumeet（Yuuta）写的

     private val lock = Any()

实际上他后来是要 synchronized (lock) { ... } 的（而不是 lock.wait(5.seconds()) 这种对 java.lang.Object#wait(long) 的调用），这当然没有问题，要不然 kotlinc 也不给过了。

CRUD 语句比较简单，都学过了（那么我就再花点时间顺便学一下，感谢 dalao 的分享 #SQL #Postgres

现在也比较合适，因为我在学校的时候学着分析了一下实际的应用，理工两开花，结果非常成功。而且我发现 Kotlin + SpringBoot 开发起来非常模式化、MVC 模式非常简单（就是几个 Entity、后面那些东西都是自动生成的，写个 interface 和几个 Spring EL 一 瞬 解 决模型层查询问题，Controller 层都非常 trivial，@ResponseBody 可以直接组织起 JSON 来，不需要脑子），决定赶快做一个练手（别怪我写的东西太 trival... 或许还不如 OI 生一天的，当然现在 OI 生可能也有些不是多复杂的东西（甚至 dfs 深度优先搜索不会做都不是不可能），当然我觉得都差不多，没啥有意思的算法，就是拿那几个接口绑定一下完了，Xposed 插件什么的都一样，我觉得写这种东西应该比编写效率和建模分析能力，当然也可以当我智障好了。这就轻松多了）
所以还是比较适合学这类东西的（属于 JPA 层（当然实际上 Web 后端和前端都还有很多知识可以学，不过其实能借助文档比较不用脑子的学会了，不需要多少思考，代价就是不会有太大提升

顺推博文 SQL查询语句及关系代数复习题

这是代码 #code 据说实现的是一个 sorted set 的 table？？？

INSERT INTO array_test(id, items) VALUES (1, ARRAY[1])

比较简单不讲

ON CONFLICT (id) DO

下面的语句是插入 id 冲突的时候执行的

UPDATE SET items = ARRAY(SELECT DISTINCT item FROM unnest(array_test.items || excluded.items) item ORDER BY item)
WHERE NOT array_test.items && excluded.items

RETURNING items;

unnest(): This function is used to expand an array to a set of rows.
子句们（不是所有 #PL 爱好者都必须把 AST 之类的东西搞出来或者指出那个语句什么组成情况...）
UPDATE SET: UPDATE changes the values of the specified columns in all rows that satisfy the condition. Only the columns to be modified need be mentioned in the SET clause
SELECT DISTINCT: The SELECT DISTINCT statement is used to return only distinct (different) values.
RETURNING(of UPDATE): The optional RETURNING clause causes UPDATE to compute and return value(s) based on each row actually updated

简单到幼儿园级别的 SQL 子句就不说了（比如 ORDER BY）

当然我只是顺手找了点文档而已... 具体实现逻辑自己分析吧（我看了个大概）（因为我准备发书单来着...）

深入的话就是 data type 和相关的 operator 和 function，以及 pg 对 CRUD 扩展的专有写法

我目前还是想拿 Pg 做点实际的应用（

实在是没有那个力气开几个理论向学习，因为定理证明、PL 理论那些已经够累了... 代数程序逻辑依然在学，反正理论向都是均衡发展但都很薄弱就是了

现在具体来讲就是 The Little Schemer 终于熟悉了一点这个列表处理语言... 不过我觉得还是 Haskell 好，因为 Haskell 更符合直觉（看很多用 Haskell 讲程序分析的论文就知道），Scheme 一类的一大堆 car cdr 让不让人活了

具体就是（拿 foldr 和 foldl 举个例子）

Haskell 里（比较简单比较符合那些面向程序分析变换的方式，没有 Foldable、Functor 什么的 class，也是因为我没好好学过 Haskell，羞愧）

foldr :: (a -> r -> r) -> r -> ([a] -> r)
foldl :: (a -> r -> r) -> r -> ([a] -> r)

foldr f v [] = v
foldr f v (x : xs) = f x (foldr f v xs)

foldl f v [] = v
foldl f v (x : xs) = foldl f (f v x) xs

reverse :: [a] -> [a]
reverse = foldl (\xs x -> x : xs) []

map :: (a -> b) -> ([a] -> [b])
map f = foldr (\x xs -> f x : xs) []

length :: [a] -> Int
length = foldr (\_ n -> n + 1) 0

当然，上面的都是 point-free 风格（两边约掉一个参数）（现在你们知道啥叫程序变换了吧？），which 曾经被淫王喷的，因为不直观（实际上他也喷 fold 这种递归模板的，实在是不够直观），不过我是为了讲这个专门举的例子求不喷。

而我们用 Scheme 翻译一下原来简单直观的代码瞬间变成了乱码（这里就没加类型，因为我没试过有静态类型系统的 Scheme 实现）：

(define fold-right
  (lambda (f v l)
    (cond
      ((null? l) v)
      (else (f (car l) (foldr (cdr l)))))))

(define fold-left
  (lambda (f v l)
    (cond
      ((null? l) v)
      (else (foldl f (f v (car l)) (cdr l))))))

(define foldr
  (lambda (f v)
    (lambda (l) (fold-right f v l))))

(define foldl
  (lambda (f v)
    (lambda (l) (fold-left f v l))))

(define reverse
  (foldl
    (lambda (xs x) (cons x xs)) '()))

(define map
  (foldr (lambda (x xs)
    (cons (f x) xs)) '()))

(define length
  (foldr (lambda (_ n)
    (add1 n)) 0))

一　瞬　混　乱
不要停下啊（指乱码）

而且像这种（universality property of fold operator）拿 Scheme 表示就彻底... 彻底（暴论
请善用模式识别。高中生数学科目必须要会的技能

g [] = v
g (x : xs) = f x (g xs)

⇔

g = fold f v

e.g. reverse 函数

reverse [] = [] （其实 reverse [_] 来匹配只有一项的列表也可以，我觉得是这样）
reverse (x : xs) = reverse xs ++ [x]
⇔
reverse = fold f v
where f = (\x xs -> xs ++ [x])
v = []

步骤（推算出 f）大概就是 (g xs) 换成 xs...

g (x : xs) = 

f x (g xs)
reverse (x : xs) = reverse xs ++ [x]
reverse xs ++ [x] = ((++) (reverse xs) [x])
参数顺序不对，再加层 lambda 表示法就可以了（

定理证明现在勉强理解了一下 rev (rev v) = v 这种，所谓的『更小规模』的证明 forall a v. rev (v ::r a) = a :: rev v 也能勉强理解了，看了证明思路也有，但是还不会写，rewrite 归纳证明比较符合直觉（拿 xs 递归解决什么的...）然后 Agda 总算是看得懂了（我不知道写了多少遍那几个例子才,,,）

那些还没到理论上，都还是实际应用用到的

（说错了（羞愧

#Haskell #FP #PL #Agda #Book 成天讲这种小学生水平的实在羞愧... 马上发书单，随便说点感想后弄点实际上的应用（

顺便说一下，王垠（其实我知道我不应该老是提他，而且相信大家有很多人都只知道王垠，因为很多人在吹他，然后这里面有些人就连轮子哥、Rednaxelafx 大、三锋都不知道）（其实知道又怎么样，你们不会看他博客的...）喷一些人是 fold 都不知道是什么就在那瞎用

其实嘛，我想了一下发现我自己就有点这个意思，不过我是搞得懂 foldr 然后暂时搞不懂 foldl

当然，对一些比较崇拜淫王的人来说（其实我现在因为选择了放松一点自己这方面发展就没有那么神经质了（之前我总是觉得会有 #Android 开发的前端来喷我，现在不会有这种臆想了
我对王垠真的是没有什么看法，和大家一样，都只是相对客观的就事不就人评价而已
不过我绝对不会把他当成偶像什么的去膜拜，在我看来他是大佬，但就如他的博客名当然我在扯淡一样，我不知道他到底哪些东西会不会是在扯淡，在跟你们开玩笑
当然我就他所展示的经历而言非常羡慕出国留学的经历。就这样。That's all

#dev 能做应用层的人也就是永远只会去做应用层吧... 因为你们对这些不感兴趣，也没什么，扯不到什么优秀不优秀上面去，各有所好而已（其实也不然，我发现很多老一点的程序员后来都会从脚本小子步入理论或者更底层的工程，看你们的性格了）

不过是我游戏都懒得玩成天弄这些东西，然后你们放松就是玩 Ingress、然后其他游戏什么的... 玩 Android 的也有，我也非常喜欢玩 Android #CoolApk #GeekApk （当然别喷这个了，都过气了）（再者，士别三日即更刮目相看，我已经不是 18 年的我了）

当然也有人喜欢用自己应用、看自己应用得奖、发展，卖到钱时候的成就感，喜欢和自己的用户插科打诨，有人只是单纯喜欢写应用，或者喜欢练习写应用，反正都没什么的，各有所好。

这个 foldl 就是 foldLeft，Kotlin 里当然也有（说明 Kotlin 其实也蛮函数式的，删除）（因为是废话啊）（Kotlin 显然比 Java 8 什么的更函数式，当然 Java 9 比 8 其实变化不大，主要还是方法本地变量支持类型推导不用明写了）（所以冰封哥会说垃圾 Jawa）
（当然我还赶不上去年他的水平，我都不知道他到底上不上学... 怎么就有这么多时间拿来玩这些东西，真 TM 是好知者不如乐知者）（看看这篇 Agda 教程博文，还是他讲『简单』东西的，然后 2017 的他写的 9012 年的我都看不太懂）（成都的学校都这么优秀么，这还有没有天理了...）（好吧，就是比你优秀，不服拉黑...）

（我可没有这么智障，不服拉黑什么的）（那可真是智障）（接下文）

（看了那个博文那个章节后突然发现说得好啊，而且可见王淫还是蛮有水平的（废话）

其实我刚才说的弄不懂是我在吃饭的时候考虑了一下拿 foldl 定义的 reverse 函数

Haskell（Scheme 的太长不复制了）

foldl :: (a -> r -> r) -> r -> ([a] -> r)

foldl f v [] = v
foldl f v (x : xs) = foldl f (f x v) xs

reverse = foldl (\x xs -> x : xs) []

能用（F**king 的 GHCi 里莫名其妙报 Branch exhaustivness 错误弄得我一直很麻烦）。（如果是 Prelude 里的 foldl 的话 reverse foldl 的第一个 lambda expression 参数的两个参数 x xs 调成 xs x 就可以了）

这里用 foldl 而不是 foldr 来定义是为了方便大家了解 fold operator
而且，FoldLeft 可以尾递归优化成循环的形式（can be easily modified to run in constant space），FoldRight 出于它本身的算法就必须用到非常量复杂度的栈空间（就是下面说的直觉式，好像 John Backus 最开始 20 世纪的那篇 FP 创立论文 Can Programming Be Liberated from the von Neumann Style? 说的『inseration』插入操作符）

foldr (+) 0 [1,2,3]
= (+) 1 ((+) 2 ((+) 3 0))
= 1 + 2 + 3 + 0
= 6

但我惊恐的发现我 居！ 然！
不知道它是如何工作的...

最后给可能一样的大家，顺便给自己：（反正你们不看，傲娇。

reverse 1 : 2 : 3 : []

foldl f v [] = v
foldl f v (x : xs) = foldl f (f x v) xs

= foldl (\x xs -> x : xs) [] [1,2,3]
— 这里就简化 (\x xs -> x : xs) 为 f 了
= foldl f (f 1 []) [2,3]
= foldl f (f 2 [1]) [3] — (1)
= foldl f (f 3 [2,1]) [] — (2)
= foldl f [3,2,1] []
= [3,2,1]


哦我总算知道了... 先被模式匹配出来的先压入 (:) LIFO []（本质上不是压入，而是 cons 出链表，不过我觉得这里反正都一样），和之前的汉诺塔问题一样...

foldl (\x xs -> x : xs) [] [1,2,3]

上面的程序结果其实就是 3 : (2 : (1 : []))
(1 : []) 就是式子 (1) 的结果
(2 : (1 : [])) 就是式子 (2) 的结果

所以其实蛮 effective(#fix efficient) 的（比起 foldRight 定义的那个 ++ [x] 没效率来说

(++ ys) = foldr (:) ys

#SQL #recommended #blog https://blog.lilydjwg.me/2015/1/25/nine-pitfalls-of-mysql.77680.html

#life 打印机墨盒到货了，可以继续打印文章看喽（ 😆

#Backend 这个人绝对是有很老资历的软件工程师了，非常擅长后端这一方面的事情，现在 #Rust 社区里活动的人也应该能够看到他的身影

#JetBrains #dev #Android #IDEA #Kotlin #Java

https://mobile.twitter.com/JBToolbox/status/1085853883451219968
以后可以用 JetBrains Toolbox 安装 Android Studio 啦！！！

#Android #China #Low

#recommended #Ruby #Elec https://blog.lilydjwg.me/2012/3/24/flip-flop-in-ruby-jk-latch.32635.html