1.4给了 fun interface的SAM

说起来我看 ice1k 的 agda 群组常年没人讨论，还打算加两条OT一样的
https://t.me/ice_learn_agda_chat/267

后来发现我这好心根本就是鬼扯，其实人家根本不缺废话；何况我不处理 Haskell/Scala 系语言和其它编程范式的

感情很复杂，这个语言 ice1k 也不是没讲过，只是他把老的入门性 agda 博客都删了，何况这些问题即便讲不好也没啥可怪的，它本身就复杂。

譬如递归 reverse 链表：

rev (x::xs) = [x] ++ (rev xs)
rev [] = []

要把这个思路切换成怎么归纳证明 rev (rev xs) = xs 从而 forall x xs. x:xs = (rev xs)++[x]
或 =(rev xs)++r x 是很困难的

（怎么今天看了就好像只是构造数据结构再相等性一样平常，之前可是很不解的……）

好吧，那我就不用 Agda 先讲讲
归纳证明是对序列的俩成立：对首项『基线』成立，对每项都基于前命题成立（命题证明不是布尔，没有失败一说）

比如咱有 listOf(1, 2, 3).fold(0) { a, b -> a+b } 需证明结果不小0:
基线 [] 恒成立
递归 (p, x) x不小0

当然加数都不小0 只是一种子集情况。
我们能以 xs.fold(true) { p,x -> x>=0 } 测试输入成立性，如果你觉得这玩意是类型，那说的就是“那个”编程了。（看不惯我混乱理论可以自己科普）

我们知道类型系统就是可以“否决”某段程序的东西，所以它实际上是在定义某种关系性的约束（比如 paramType in type.impls 这种 trait(interface) 实现约束）

如果这个可以在约束上定义些计算，或者说类型检查期也能做递归匹配的话，就是 dependent type 了（刚才的例子结果 >= 0 的实际情况只能算全再判，更像编译期计算了）。


好了看看 rev (rev xs) == xs 怎么证明，肯定一头雾水，但想想如果你构造的不是『类型』而是判定器会怎么做？肯定是算完再试等……😂 不要那样。

等式的右侧是数据，左侧是两层调用；如果下手得从左顶层的 rev, 而要证明就必须得出 (rev xs) 与 xs 本身的关系再作归纳，好像你能“解构”这个调用一样，你会怎么解构？肯定是 xs++[x] == x::(rev xs) ，当然等号反过来也一样（自反性 identity/reflexive 的交换律）

想到 xs++[x] （把 xs 全串到 x::[] 上）你一定记得 xs 在这里意味着递归栈了，因为 (xs++ys) 隐含着二者长之和+1([], nil) 的递归栈

(xs ++ ys) = cat xs ys where
cat zs (x:xs) ys = cat (x:zs) xs ys
cat zs [] (y:ys) = cat (y:zs) [] ys
cat zs [] [] = zs

这里我们用了第三个链表，是因为必须从 xs 的尾部，逆序 ::(cons) 到 ys ，其实不嫌麻烦也可以 foldRight(用栈逆序) :

(xs++(y:ys)) = xs++[y] ++ ys
(xs++[]) = xs

嘛，这个非常不动态编程(DP)弱缓存，例一用 tuple 保留zs也可实现，不得不说 Haskell 的模式匹配函数的确直观反映了各种流算法。

跑题了，假设你得出 forall x xs. x::xs == (rev xs) ++[x] 呃不是 x::(rev xs) == xs++[x]

（好吧二者是不一样的，记得主语始终在 ++[x] 的部分）
（注意要解构等式两边，都必须用到递归栈，第一个实际上是正向 rev 的定义😞）
可以通过以下方法证明 rev (rev xs) == xs ：

-- x::(rev xs) == xs ++[x]
xEqTail : (a, [a]) -> [a] -> Bool

idp = (==) -- eq path
revId (x::xs) = -- xs++[x]
xEqTail (x, ) && (revId xs)
revId [] = (idp [] [])

等等， x:(rev xs) == xs++[x] 这个等式不对，我没注意到 (rev xs) 和 xs 本身的区别…… 其实是 x:(rev xs) == (rev xs)++[x] ，意味着 x:xs == rxs++[x] ……
算了写不出来😢不多说了，入门科普而已。
顺便：代码部分可以理解为交换 ::(has type) 和 :(cons) 语义的 Haskell, 反正我不是说正经的。

上面证明 rev (rev xs) = xs 里我解构施用层 (rev xs) 到 x:(rev xs) = xs++[x] ，其实是 rev (x:xs) = (rev xs) ++[x] 的反向变形。

我显然把右边的 xs 理解成其参数了（虽然对正常程序猿 等式左边才能有未知量是直觉😂），没注意到关系解构的部分必须以 (rev xs) 描述，例 rev $ [1,2,3] 可不等于它++[1] 呢…… 但是 [2,3] ++[1] 就对了

这个点子是我在提示下独立想出来的，但思想和实践总是隔着基础模型的桥梁，虽然能设计、找到特色点也远不等于能细分并逐步实现，知道理论不等于善于实行。
不过，我仍希望这对大家有帮助，哪怕是理解别人的误区和失败。

只要可能对人有帮助，我才不怕出丑丢脸；毕竟相比技术和创造，自尊太微不足道了。

把 rev (rev xs) = xs 里的 (rev xs) 与 xs 互换即可得到 rev xs = rev xs 全等，可这不是“移项变号”或“两边同时减”那么简单（虽然也可理解为“把rev移到另一侧”呢），但不管怎么样显然是重组 a:rev$v=rev$a:v 这种关于 rev 结果的关系

以我目前这层面的水平当然仍是无法做到定理证明啦，虽然它也有意思。 #cs #plt

话说部分读者你们也被不明觉厉加入那个讨论组唉，还是劝退好了

人家千里冰封说的明明白白，必须有 dependent type 基础，并且他是不负责给你打基础的，狠心点：

菜鸟别以为和大牛在一起、或者看大佬做事就能给自己涨知识，没用的。

接近那个领域，也别以为自己看它的文档、用它的术语你就属于它。
系统的知识网络和直觉不是靠生硬的文字和无聊的名词能表达的，名词和定义规则背后隐含的是前人真切的思考，你不学他所学怎么能真懂他。

有些人就是天才，你和他差的就是人家能独立得出而你无法get到的一句话、一个小思路，有时候是因为知识和经验，有时候 1% 的灵感就是靠努力无法填补的。

不要以为自己足够热血或者“非常想”就能成功，科学说了算。

也不要自作主张认为“我需要那些东西来帮助进步”，不你不需要😡。阻塞在一个目标上不懂变通、提升知识广度，那叫环形等待、死锁。

说错了话他们不耐烦你也不开心，本就不是一路人，派系不同何必凑数。

#China #web 🤔

【品葱】
看到这个，我只想说：意料之中。

整天内斗吵架，不维护社区氛围、不鼓励创作，那么就只能慢慢的死亡了。因为品葱本身的竞争力不大，很容易就能找到替代品。真正让用户持续在品葱发表内容，都是靠用户维护出来的氛围。肆意将用户污蔑成网军，对原创内容的不重视，极大的破坏了这一氛围。品葱自然就丧失自己的独特性了。

更不用说趾高气昂的管理员。这点相信如果大家有和某些管理员接触过就知道我在说什么。

不重视内容，不重视用户体验的恶果已然显现出来。品葱站长无论是公开还是私下都多次表示品葱的目标是要“活下去”，而不是“做大”。但是品葱目前面临的问题是自身在失去“生命力”。错将维护讨论氛围、改善用户体验视为“扩张”。对于提出问题的用户刻薄与打压（甚至污蔑对方为网军），对于不满管理员决策的用户嘲弄与侮辱。品葱与半年前提出的《习惯法》沦为废纸。所谓“用户自治”彻底失败。可以说，品葱作为公共讨论空间，已完全失去“讨论”。目前品葱的定位更多的是内容农场而不是“问答式社区”

品葱的例子令人惋惜。曾经的旧品葱无论是氛围还是内容都无法挑剔，可惜在中共的威逼利诱下被迫关闭；新品葱在最初的时候虽然小众，但是质量、氛围、人气随着反送中运动的爆发而爆发，往后无论是反送中，新冠肺炎，都有着非常大量且用心的内容发表。可如今再去看品葱，关于国安法的讨论寥寥数个，首页大半部分被搬运新闻和旧贴占据。质量也不尽人意。看了看品葱曾经的archive，看到曾经品葱上的人们乐观而且满怀希望得为自己心中的信念与他人据理力争，再看看如今少有答案/评论超过一百个字。曾经置顶各种活动贴，多方联动。如今躲在角落里自己一个人玩泥巴

不禁感叹一句“时过境迁啊。

品葱已死，我们还要继续走下去。希望大家永远都要记得品葱，记得它曾经大放异彩，更要记得它是怎么落寞的。

各位晚安。

#gui #android

请教一个相机相关的问题。打开相机以及设置预览回调都在同一个子线程内。但是在onPreviewFrame回调方法中打印当前线程却是 main。 何故？

Callbacks from other methods are delivered to the event loop of the thread which called open(). If this thread has no event loop, then callbacks are delivered to the main application event loop. If there is no main application event loop, callbacks are not delivered.

#Kotlin #collection 怎么把两个List合为Map?

可以 (xs.zip(ys) as Iter<Pair<A,B>>).toMap() 但不一定真是 Iter
可以用 xs.associate { it to yz.next() }
可以 ys.associateBy { xz.next() }
据说还有 xs.associateWith(ys) { (x,y) -> x to y }

如果连 Pair 都不想创建，可以 zipToMap 组合+归纳:
while (xz.hasNext() && yz.hasNext())
map[xz.next()] = yz.next()

api依赖就是compile的