😶 接个外快写一下 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 来生成这些绑定是对的，至少不会写半天又加半天的 ? 记号...

现在看来 Swagger 的规范好正规呢，但是如果 GeekAPk API 要拿 Swagger 重写，那不知道要花多少时间呢

上面提到的 spec，我当时压根没写完，只定义了几个模型

但居然写了 503 行

我的脑子都快 struct 不了这个 YAML 文档了，一大堆二维文法，而且结构又复杂... 🤔
全是竖着的简直淡疼，如果没有 Schema 补齐、可以说 Swagger 这个工具就完全没有用了... （因为写 spec 将花费比现在很多 bootstrap 自动化方案更多的时间...）

  /{username}/token:
    get:
      tags:
        - User
      summary: Authorize user
      operationId: getToken
      parameters:
        - name: password
          in: query
          description: User password
          required: true
          schema:
            type: string
            example: sa1tedFi$h
        - name: username
          in: path
          description: User to get new token
          schema:
            type: string
            example: duangsuse
          required: true
      responses:
        200:
          description: Got app access token
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/AuthToken'
        default:
          description: Auth failed
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Error'

其实这么复杂的 OpenAPI 3.0 YAML 结构要表示的只是一个最简单最容易理解的定义（指民科的过度设计，但我觉得民科和前端打架还是民科赢 hhhh，实际上都没赢...）：

type datetime: string = Date

result OK: status = 200

data AuthToken "Authorization token"
  = { token: string, expires: datetime }


## Begin API definition

== user

'''
Authorize user
*password: User password
  'example_password'
*username: User to get new token
  'duangsuse'

>OK: Got app access token
>*: Auth failed
'''
getToken(password: string, username-path: string)
  -> (OK) AuthToken
     (*) Error
  = /:username/token

我真的不想去学习『如何阅读几乎全是竖排的 YAML』... 所以想来要 GeekApk 利用 Swagger 好像有点难受（迫真

（好吧，就是迫真自演 GeekSpec，但是，其实我希望能让它可以扩展一下来兼容 Swagger OpenAPI 3.0 YAML，我真的没有说骄傲什么的，比我牛逼的人很多，不缺一个只能写垃圾程序的 duangsuse
以后 GeekSpec 的更新版本或许会能作为 Swagger OpenAPI 的一种描述方式，也能有一个 OpenAPI 的后端

对类型系统了解不够，还停留在 Java 的幼儿园级别...

其实 GeekSpec 还是蛮工程的，所以什么类型系统实际上就没有，不是那种通常 General-Purpose 意义下的类型系统

考虑一下 GeekSpec 类型的用途，就是标记一种数据类型，这种 HTTP 协议其实都有兼容的...（Content-Type，MIME 类型）

比如说 datetime，可能就是说绑定到原生的某种结构对象，和泛型什么的其实根本没关系（当然泛型也不是什么高级玩意）

其实对于 POSIX C 的 time_t 来说，一个所谓的 datetime 或许可以这么表达？

type datetime: string
= (C Linux) time_t
(Ruby) Time

read datetime {
#impl C Linux
return (time_t) atol(str);
#end

#impl Ruby
return Time.at(0, str.to_i, :millisecond)
#end
}

put datetime {
#impl C Linux
size_t size;
char *out;

size = snprinf(out, size, "%l", datetime);
if (size < 0) return NULL;
size++;
out = malloc(size);
if (out == NULL) return NULL;

size = snprintf(out, size, "%l", datetime);

if (size == 0) {
free(out);
return NULL;
}

return out;
#end

#impl Ruby
return sprintf('%i', datetime.tv_sec * 1000 + datetime.tv_usec)
#end
}

validate datetime {
#impl Ruby
str.match? /[0-9]+/
#end
}

路漫漫其修远兮 吾将上下而求索 🤔