#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 文也可以的 👍

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

😶 我目前没博客

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

.NET 现在这么可怜的么？

我哭了（

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