#China #Low #life #jvbao 不解释。

这位先生也真是 🌚👍厉害厉害。

服，服，服。
可惜我没有某先生那么好的口才、没有大佬们那么犀利的语言，不然这种情况，这个大佬恐怕是要被公裁了（实际上已经是这样了）。

值不值：你骂得越多，他赚得越多

我的回答是不值，所以我选择不回骂他。
既然侯先生要拿这事说话，而且丝毫不顾及一点道德行为规范也不像机器人，我想请问我哪天在哪里问候过除了先生您之外您优秀的家人们了。

我非常诚恳地相信，您妈对她的儿子有这样优秀的语言和行为一定是无比的骄傲和自豪吧。为国争光在被国墙了的 Telegram 上举报不法翻墙。

也衷心祝愿先生您能在反违法 fq 的路上越走越远，离实际越走越远。
到时候已经肉身翻墙的人们可能会在墙外对着自己的孩子指着您，说千万别学这个人，和『不『法』』翻墙斗争一生，结果既没有做到什么有意义的事情，也没有被任何有关部门采纳自己的优秀情报，而且连墙是怎么工作的都不知道。

真的是两边走不通啊。

正在测试 Times 服务的 API 接口定义...

spectrum(0.6)> conn.url_prefix = 'http://0.0.0.0:234'
=> "http://0.0.0.0:234"
spectrum(0.7)> apiVersion
=> "0.1.0"

Spectrum 可以十分成功的完成基本接入...
不过，其实 Spectrum 的代码质量不怎么样（甚至对于目前的一些 Ruby 应用来说，要加个『很』字才行）

用打开类修改需要修改的方法，凑合着用吧... 🤔（把技术债务压给 Ruby 的元编程灵活性解决）

#Github 湖北襄阳这里偶尔有时候出现 SSL 证书异常，不知道你们有没有 🤔

累死，算是学习（确信）了一下 Ruby 和测试了 Spectrum... 感觉解耦合做得不是很好，response mapper 根本一点用都没有（因为要很多 mapper 必须要拿到一个 ClientShowcase 实例），另外给 ClientShowcase 添加一个 Hash 表来放诸如密码这样的东西隐式传递不错），考虑重构。

Times 是之前老 GeekApkR 里唯一一个能用的后端服务... Ruby + Sinatra 写的，其实现在看来都很不良实践（跑）
凑字数（代码行数）吧（

不过它的测试套件也算完整，虽然持久化层的不是 Mock，但也可以用，缺点是如果在生产环境用了很可能导致数据丢失

Times 没有使用 DBMS，而是，这是因为我以为它不会有太大的数据集性能要求，我觉得很可以重构（比方说，使用类似 MongoDB 的面向文档数据库替换纯手动）... 尤其是难看的 API...

值得注意的是我以前智商还低一些的时候，连常用的序列化这种弱智能力都没有...
JSON 序列化（Times 的数据持久化方式）当时非常的混乱，我非常智障的套模板（或许，因为我想我那时就是瞎搅合...）

我没有么写：

[foo, bar, baz].to_json

而是：

[foo, bar, baz].map { |o| o.to_json }.to_json

然后反序列也一样... rofl.

回来了（因为身体素质真的开始有点 🌶🐔 了，而且非常需要休息，然后老是熬夜容易变丑，虽然其实长的就不咋地，大嘘），顺便添了一些任务

1. 部署文档添加 Systemd 低端口权限配置提示（服务程序部署安全，这样如果我们的 upstream 有严重的，例如 RCE、可以拿 Shell 的安全问题别人不至于一下子迫真 rm -rf / 殃及池鱼）
2. 把所有 Endpoint mapping 的 Int? 换成 java.lang.Integer? （要不然错误，说 int 不能是 optional 的，虽然本来有默认值 0）
3. 为了 Clients 数据交换开心，添加 PATCH Json API（现在创建用户之后可以直接拿 JSON 去 patch 属性了，不用一个一个属性去 update）
（现在还不是 RESTful 的）
4. 添加用户和管理员权限验证的 Middleware（WebFilter）、其中用户的权限验证和 Rate Limit 一起做（GeekHits API 也一起开放了）
5. 为 CI Intergation 添加 Node.JS 和 MRI Ruby 依赖，并且开始使用外围的 Spectrum Ruby 客户端接口测试（从 JUnit 启动服务器和 RSpec 客户端自动化测试程序）

GeekApk v1b 完成后可能有别的打算（包括 Android 客户端，不准喷我不会什么设计模式）（有些人不准喷我菜...）（虽然我有时候的确很菜，但我自己觉得我很有前途，嗯嗯。）

希望以后都是艳阳高照。冻死了天又黑...

#Math Tips: 为什么任何数乘 0 都得 0，乘 1 都得原数？（放松一下系列）

（好吧，虽然我平时都不是很轻松（大嘘））

考虑一下自然数（正整数）的定义

data Nat = Zero | Succ Nat

我们这么说：一个自然数可能是零，也可以是另一个自然数的『后继元（Succeeder）』
那么 1 就是 Succ Zero（1 + 0）、3 就是 Succ (Succ (Succ Zero)) （1 + 1 + 1 + 0）

那么，对于 Nat 这个 GADT（不准喷为什么用 GADT 而不是 plain 一点的 struct 或者 OO 的 class），怎么定义加法呢？

很简单，

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

因为逻辑实在太弱智（是的，喷的是我自己弱智）所以不讲
当然 fold 是针对列表的，而且这里插入操作可能很迫真而且没有太大意义，而且我的智商很低，所以就不用。
那么乘法是什么呢？

数学告诉我们，乘法就是

n × 0 = 0
n × 1 = n
n × 2 = n + n
n × 3 = n + n + n
n × m = n (+ n){repeat for m - 1 times}

对于 Nat 怎么定义乘法呢？

一样很简单，

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

因为我比较菜，而且这个问题非常弱智，所以我们来检验一下：

natToInt :: Nat -> Int
natToInt Zero = 0
natToInt (Succ m) = (natToInt m) + 1

five = Succ (Succ (Succ (Succ (Succ Zero))))
one = Succ Zero
two = Succ one
three = Succ two

最后的代码 #Haskell

data Nat = Zero | Succ Nat

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

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

natToInt :: Nat -> Int
natToInt Zero = 0
natToInt (Succ m) = (natToInt m) + 1

five = Succ (Succ (Succ (Succ (Succ Zero))))
one = Succ Zero
two = Succ one  
three = Succ two

main = do
  print $ natToInt (add one three)    
  putLine
  foldl (>>) (putLine) os
  putLine
  print $ natToInt (add three five)
  putLine
  printNat $ mul three five 
  printNat $ mul five three
  printNat $ mul Zero five 
    where printNat = (print . natToInt)
          os = print <$> (natToInt <$> [one, two, three, five])
          putLine = putStrLn []

== 那么，为什么任何数乘 0 都得零？

mul Zero one = Zero

这个逻辑简单易懂，因为 mul 的定义就是这个

mul one Zero =
  add Zero (mul Zero Zero)

对于 mul one Zero 是的，但是我们肯定要问是不是对于所有 Nat "n" 都有 mul n Zero = Zero 这个等式成立
那么我们就可以做一个非常 immediate 的归纳证明（大嘘）
就是说

mul Zero Zero = Zero
mul (Succ _) Zero = Zero

第一个等式肯定成立不用说（基线，数学上叫奠基，只求你们别喷我知乎 @证明 民科，我一直在做科普从来没有做什么民科的意向...）
第二个我们可以考虑一下展开：

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

好吧，这个不是递推的，所以我们换个角度考虑，首先我们证明 mul one Zero = Zero，它是成立的（考虑 add 的定义）

mul (Succ Zero) Zero = (add Zero (mul Zero Zero))

然后是 mul (Succ one) Zero = Zero


mul (Succ qa1) Zero = (add Zero q1) = Zero
  where qa1 = (Succ Zero)
        q1 = (mul (Succ Zero) Zero)

我们（求不打）注意到对于任何 Nat (Succ m)，都有 mul m Zero = (add (mul m Zero) Zero)

，只是我读书少不知道是不是应该怎么着才算是完成了（的确是比较
只要证明了 (add Zero Zero) 是 Zero，是不是就可以说 ∀o∈Nat. mul o Zero = Zero 呢？（迫真自演）

唉我数学还是差了，别打我，我是从数学书上看的数学归纳法（暴论）

首先我们（为了方便）证明为什么任何数 + 0 还得原数，换句话说，

add Zero n = n (1)
add n Zero = n (2)

(1) 直接得证不用说
对于 (2) 么

add Zero Zero = Zero (3)
add (Succ m) Zero = add m (Succ Zero) (4)

考虑我们的 Nat GADT，任何 Nat 只能是：

- Zero
- 另一个 Nat 的 Succ

证明等式 (2) add n Zero = n 可以转化为证明等式 (3) 和 (4)

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

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


  = (Succ Zero)

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

（其实我感觉我是在给加法证明交换律，可是我太菜证明不了 23333）
因为那个 Nat 的确是 Coinductive 的所以我只能这么做了（迫真）
为什么说是 Coinductive 呢？

inductive 的长什么样子呢？

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

sum [] + 1
= 0 + 1
= 1

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

这个是往 sum [] 的方向弄的... 上面那个的 Nat GADT 好像不是（跑）（但应该也是 inductive 的，我太垃圾还不能理解）

证明不下去了... 太不熟悉了，耗时间...

想证明 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 文也可以的 👍

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