想证明 add operator 对于一个参数为 0 情况下的交换律（其实也就证明了 0 加任何数都得原数的定律）

data Nat = Zero | Succ Nat
add :: Nat -> Nat -> Nat
add Zero n = n
add (Succ m) n = add m (Succ n)

我开始的思路可能是证明 add one zero 最后等于 add zero one（就是说第一个参数最终会『转移』到第二个参数上，然后能 match add 的第一个 branch 得证）

后来乱了... 算了吧（

那么最后再 #轻松一下 #Haskell

什么是 Currying 的 Point-free style 呢？
其实这个问题太 trivial 所以基本都懒得说，一言以蔽之『两边约掉一个参数』

for example

product l = fold (*) 1 l
等于 product = fold (*) 1

为什么等价呢，这里当然懒得做形式化证明了

考虑一下下面的例子：

parseBaseInt :: Int -> (String -> Int)

这是一个函数，接受一个 base （进制）参数，返回一个函数，而这个被返回的函数接受一个 String 类型的参数，返回一个 Int 类型的值
它其实也可以这么表达：

parseBaseInt :: Int -> String -> Int

parseOctalInt :: String -> Int

parseOctalInt s = parseBaseInt 8 s

其实这就是说

parseOctalInt = \s -> parseBaseInt 8 s
也等价于
parseOctalInt = \s -> (parseBaseInt 8) s

但是也可以这么表达，反正 (parseBaseInt 8) 已经是一个 (String -> Int) 了，那就不需要再加一层 \s 上去，只是为了覆盖掉这个 s 的来源作用域...
所以有一种『Point-free 的写法』

parseOctalInt = parseBaseInt 8

记住这个做法的本质是利用 Currying... Currying 是为了能让单参函数变成多参函数... 所以也可以这么说：利用 Haskell 里『都是单参数函数，或者说一元函数』的特点
有时候（比如上面那种情况）这种做法有价值，有时候它会令代码更不容易看懂（比如说上面的 product）
反正具体怎么弄自己取舍，很 trivial 的东西

#Android #dev dalao（

😶 接个外快写一下 Android App in Kotlin

😐 我想看看我的天赋和学习能力到了什么程度

刚才上 #Bilibili 站，发现国人做的语音处理方面的项目还真是多啊... Powerpoid、Emvoice

排除 Sharpkey 这种算是老项目（指公开开发时间）和 Upslink（主要是基于 Praat 的音高修正）、Moresampler、MUTA 这种有源头的，一大堆新引擎... 这是怎么了呢？

Android 开发也不错的选择（
设计模式，我上面默写的那个你也来默写一下（

对了，上面的那个 Nat 的确是 Coinductive 的，来源冰封博客

... 可是我不知道怎么证明也不可以啊（迫真
（为了证明我的确有基本 inductive 的证明能力，现在默写某关于 fold operator 相关属性的证明：

fold :: (a -> b) -> b -> ([a] -> b)
fold f v [] = v
fold f v (x : xs) = f x (fold f v xs)

sum = fold (+) 0

证明 ((+1) . sum) = fold (+) 1：

使用 universality 属性展开 sum 定义：

g [] = v
g (x:xs) = f x (g xs)
<=> g = fold f v

((+1) . sum []) = 0
((+1) . sum (x:xs)) = (+) x (((+1) . sum) xs)

（在这里 g 是 ((+1) . sum)、. 是 compose （函数组合）函数，定义为）

(.) :: (b -> c) -> (a -> b) -> a -> c
(. f g) = \x -> f (g x)

简化变形

sum [] + 1 = 0 + 1

sum (x:xs) = (x + (sum xs)) + 1

第一个等式

sum [] + 1
= 0 + 1
= 1

第二个等式

sum (x : xs)
= (x + (sum xs)) + 1
  {- 加法结合律 -}
= x + (sum xs + 1)

归纳出来了

后来想想，其实

add (Succ m) Zero
  = add m (Succ Zero)  

因为两个参数都修改了所以不能只考虑第二个参数是 Zero 的情况，到不如再抽一下成

add Zero n = n

add (Succ m) n
  = add m (Succ n)

其实它就是说
- add 0 n = n
- add m n = add (m - 1) (n + 1)

最终的『基线』其实就是 m = 0，然后每一层递归都把 m 减去一（匹配掉一个 Succ，也即『取前驱元 predecessor』） n 加上 1（取后继元），最终就是『往 n 上加 m 次 1』，就实现了加法的语义

这样是不是对于 Coinductive 证明来说就能直接得证了呢？

大佬也来学 Agda 什么的吧（
https://ice1000.org/lagda/MuGenHackingToTheGate.html 这个比较偏向入门级别


顺便问问：大佬的 GitHub 在哪里呢？（其实是想问问之前那个 AST 处理的程序是怎么写的了解一下）
大佬看没看过 GoF 的那些 OO 模式的本本呢？ 🤔
觉得好像看过会更有底气一些，我没看过... 所̶以̶经̶常̶会̶被̶ ̶A̶n̶d̶r̶o̶i̶d̶ ̶的̶开̶发̶者̶们̶吊打̶̶ #Android
觉得好像自己会画图更有底气一些，我没画过多少

其̶实̶我̶很̶想̶吊̶打̶做̶ ̶A̶n̶d̶r̶o̶i̶d̶ ̶开̶发̶的̶，̶可̶是̶不̶了̶解̶ ̶O̶O̶ ̶没̶底̶气̶

#Tools #Linux 删除线生成。

strikeout() { sed 's/\(.\)/\1̶/g' <<<$1 }


zstrikeout() { zenity --entry --text=请复制 --entry-text=`strikeout $1` }

strikeout 'Unicode Strikeout composition test' | xclip

大佬要不要试试入门 ANN（ #CS #PL
魔理沙学姐也写过这种文章

图论和函数式编程也挺好玩的

编译原理是个很实用的内容，我给 GeekAPK 搞的 GeekSpec DSL codegen 就是比较 naive 的一种应用（现在也没有写过自己的 LLVM 编译器，惭愧）
大佬的博客好像没有找到（给个链接？
如果没事的话写点玩转 PostgresSQL 文也可以的 👍

我觉得这个东西还挺好玩的 ，可是有点难... 🤔
尤其是数学我 ****🐔🐒***&%$^$@$

😶 我目前没博客

我去，这么点钱房租够么... #China #Life

.NET 现在这么可怜的么？

我哭了（

哦，大概是 Android 开发现在最吃香，哭哭。

为什么不去开发手游呢

技术就不值一个钱，不如多写几个应用

弄了半天居然是因为这些我手写的代码（而不是由 GeekSpec 定义自动生成的）我疏忽少加了 Nullable notation... 🤔看来我岔开去写 GeekSpec 来生成这些绑定是对的，至少不会写半天又加半天的 ? 记号...