#Android #dev #sysadmin 是的，他们有 CLI 工具 twrp

破 TWRP 不能触摸……直接废掉
第一次了解到原来还有 twrp 命令行这种东西（

所以这个人呐，就是要不断的学习，不断的努力提升自己

（当然我不是说 Java 比 Kotlin 简单很多，简单很多是真的，但是很多人连 Java 有 @ label 语法、vararg 语法糖什么的都不会用，标准库的一些语言内部的接口比如 Iterable 都不知道，Annotation 处理机制也不了解，这样的话还是推荐先了解一下 Java 8，推荐自然还是看本本的。

Java 比起 Ruby、Python 这种重视语法灵活性的语言语法规则少一些（不是说语法层面的东西就不值得考虑，我相信在座的各位都没有一个人敢说自己了解 Java 8 所有的语法细节的，我也不敢说，有时候单单语法上面的东西还涉及一些更相关后面 AST 上面的东西... 比如优先级结合性求值顺序貌似吧），但是其标准库、运行环境也是有值得学的东西，相当可圈可点，比如 java.util.concurrent 包、nio、Unsafe 之类的，比如 java.net

说实在话，比起担心淫王所说的本本主义者，我觉得现在的前端开发者（这里包括 Android 里的前端）更应该好好的看看书们，因为里面真的有很多值得一学的知识，比所谓的单纯本本主义要重要得多。

不要以他这句话就不看任何书甚至以『实践出真知』、『x 年经验』为荣了，千万别这么想，不然容易被一些可能是比较 trivial 的东西蒙蔽，那就危险了。

一天比一天好，最后累积的就是一个更好的自己
否则，学如逆水行舟，别人进你不进等于你退。

其实我说的可能是和 Java 一些比较... 不是语法层面的东西吧（我好歹看书找了一下） #Java #Android #PL

呃... 比如 Java 方法（类们的）区、堆、虚拟机栈大小、动态扩容什么的，JDK 命令行工具、JDWP、OQL、Object 类一些基础的东西 #clone() #equals() 什么的，String#intern()、本地表（locals）、并发垃圾收集、JIT 解释混合模式、字节码校验、原生类型装拆箱、动态方法分派（java.lang.mh，invokedynamic，我想后面一个『名词』很多 Android 开发者都听说过，可未必所有人都知道这是干什么的... 你们大概只知道『Dalvik 没有它所以 Lambda 表达式就不能原生实现，只好 runtime desugar』，这个我下面简单讲一下，算是科普）、虚方法、特殊方法、静态方法、接口方法分派逻辑（invokevirtual、invokespecial、invokestatic、invokeinterface）、位运算和各种在计算机数字逻辑上面的东西什么的、泛型擦除、ClassLoader 和字节码技术诸如 CodeGenerationLib、ASM、JavaAssist、BytecodeEngineeringClassLibrary 什么的（总觉得我提这个就很 #low...）、还有最后 Java 运行时一些线程同步机制、安全区、绿色线程、协程什么的...

下面我就兑现诺言讲一下 Java 里（还有点 Kotlin 内容）方法分派之类的东西（ #Java #PL #JVM #Kotlin

至于这个计算机科学上函数（类 C 的那种，或者叫子程序）概念... OOP 里的方法、继承、抽象那些基础的东西我就不讲了（因为我不会（逃跑

（虽然的确是个很长的内容... 难受，因为内容比较多...
（以下内容涉及一些基本面向对象编程范式的理论，如果你是为了学习而来的（而不是作为帮我找茬的 dalao）不喜欢不要喷我哦（跑

就目前的 JDK 8 （Java 8）来看，貌似有 5 种方法调用派发逻辑

+ invokestatic 用来调用静态方法，这是最开心的
+ invokespecial 用来调用特殊方法如 constructor <init>（类似 Ruby 里的 initialize），私有方法和父类方法
+ invokeinterface 用来调用接口方法，可能类似 Rust 的 trait object？会在运行时再确定实现此接口的对象
+ invokevirtual 用于调用虚方法
+ invokedynamic 在运行时解析引用的方法，分派逻辑交给用户去实现

至于什么是方法分派呢，我想给大家举个栗子理解一下除了 invokedynamic 的

interface Flyable {
  public void fly();         // 公有接口方法
  private void __imp__Fly(); // 私有接口方法
}

class Foo {
  public Foo() {}              // 公开类构造器（架构器）
  public static void yoo() {}  // 一个公有的静态方法
  private void bar() {}        // 私有的方法
  protected void internal() {} // 受保护的方法
  public void pub() {}         // 公有的方法
}

invokestatic 和 invokespecial 逻辑都可以在编译过程的语义分析阶段确定他们所引用的方法量词（全限定符）
就是用来调用 静态方法、私有方法、实例构造器、父类方法

== 至于私有方法和公有方法为什么有区别，为什么不用考虑 Reflect 的 case 呢？

首先我们看看面向对象四大特性，『封装』、『继承』、『多态』、『抽象』

私有方法不是虚方法，所谓虚方法（面向对象术语）就是可以被子类继承和覆盖的方法，它是面向对象『多态』特性最重要的组成成分（给出定义了！） wiki

简言之，虚函数可以给出目标函数的定义，但该目标的具体指向在编译期可能无法确定。

比如我们有父类 FooOrBar，其一子类是 Foo 一子类是 Bar，含有一非 final 的公有方法 biz()
有一表象类型为 FooOrBar 的本地变量或方法参数（在 Java 的语义层面）
我们没法在编译期确定语义调用目标对象的 obj.biz() 方法是说在接受者 obj 上分派 Foo#biz() 呢还是 Bar#biz() 呢
这就是 invokevirtual

而公有方法就不能确定是不是非虚方法，猜猜为什么。
Reflect 是程序员自己决定分派逻辑，和虚拟机内建的分派逻辑无关

== 至于 final 方法和虚方法又是什么呢？

Java 里一个类成员被标记为 final 就是说它的子类不可以覆盖（override）这个成员
（btw. Kotlin 里默认所有类都是封闭类 sealed class，就是说不可被继承，Kotlin 里实例方法成员也如此，需要用 open 标记来允许子类 override

final 方法肯定不是虚方法，上面的上面我给定义了

== Java 8 里的 Lambda 表达式语义是什么呢？为什么它需要 invokedynamic 以前的 Anonymous Class 就不需要？

Oracle 爸爸的文档

One issue with anonymous classes is that if the implementation of your anonymous class is very simple, such as an interface that contains only one method, then the syntax of anonymous classes may seem unwieldy and unclear. 
Lambda expressions let you express instances of single-method classes more compactly.

怎么说呢，对于系统了解过 Ruby 解释器基础的人（知道 Ruby 中有 Lambda、Proc、Method、Block 四种『可调用』对象的人）来说，Java 里的 Lambda 表达式可能类似于 Block，因为它貌似更不像一个独立需要有自己栈帧的子过程

Oracle 官方的说法是 Lambda 表达式是对 SAM （Single Abstract Method）接口方法覆盖的一种语法糖，比如 Runnable 这种只有一个 run() 方法的，作为对匿名子类的替代

因为这方面（为什么 Lambda 表达式要用到 invokedynamic 这种看似好像无关的东西实现）我也不是很清楚（因为其实我也是比较菜的）所以很难讲，因为我也懒得拖太久时间（比如花时间写 examples、看字节码）
StackOverflow[origin] 真香 那么看这个问题，

Lambdas are not invoked using invokedynamic, their object representation is created using invokedynamic, the actual invocation is a regular invokevirtual or invokeinterface.

// creates an instance of (a subclass of) Consumer
// with invokedynamic to java.lang.invoke.LambdaMetafactory
something(x -> System.out.println(x));   

void something(Consumer<String> consumer) {
      // invokeinterface
      consumer.accept("hello"); 
}

Any lambda has to become an instance of some base class or interface. That instance will sometimes contain a copy of the variables captured from the original method and sometimes a pointer to the parent object. This can be implemented as an anonymous class.

Why invokedynamic

The short answer is: to generate code in runtime.

The Java maintainers chose to generate the implementation class in runtime. This is done by calling java.lang.invoke.LambdaMetafactory.metafactory. Since the arguments for that call (return type, interface, and captured parameters) can change, this requires invokedynamic.

== 为什么 Java 8 里 Lambda 表达式和 new OnClickListener() {} 这种（匿名子类）的方法覆盖/实现可以引用外部局部变量，但被引用变量必须为 final 呢？

看这里


首先我简单的说一下，invokedynamic 的逻辑是完全可以使用 Java 的反射 java.lang.reflect 特性实现的，不过反射性能可能比较低（至少比 invokedynamic 低，除非做了严重优化），基本上 JVM 程序员都知道（哪怕是 Android 程序员也都清楚吧... 至少他们会去考虑）。

有些概念 Dalvik 上是没有的，你们理解就好。Dalvik

不过 btw, Google 的 Android SDK 使用了很多 Apache Harmony （Apache 的 Java 开发环境，类似 GNU ClassPath？）项目的代码，看 AOSP Java 代码的人应该看到过

其实对于拿 C 程式设计语言开发 native ABI 应用的程序员来说应该都不难理解，但现在已经不是所有人都知道这些层面的事情了，软件工程师的门槛正越来越矮。

溜了溜了... 随手中文写一篇技术生活相关的广播就溜（ 🐕

对不起啊，因为 Telegram Desktop Linux/Qt 编辑框的一个小问题，太长的消息渲染可能会莫名爆炸，所以这个 #learn 我没写完就爆炸了... 加上我发现已经写了很长时间而且天寒地冻的决定还是先庆祝新年吧，有时间再说这个（rt.

其实怎么说呢，Java 它看似是『简单』的语言（相对 Kotlin）但是，其内涵也是可以说是有的，比 C89、Lua、Python、Perl、JavaScript 那些低级语言高到不知哪里去了（跑）（当然 Haskell、FSharp 之类的也很高，但是不是一个方向的高，Java 是 OO 语言，各有各的好）

OO 编程其实是个容易使用但不容易完全理解的玩意，彻底做到如 GoF 那种一份文件一个类图的理解层次是比较难的，需要长年 nontrivial 的积累，现在很多 Java 平台的开发者学的都比较 trivial，不懂的东西也懒得深究，看不透辅助类型开发者们对底层复杂性所做的封装，重视实践轻视理论，但这其实是不利的（如果前端们没有做到人尽其用的话，不能空下应该拿来读书学习的时间就是），理论和实践应该兼而有之，不理解这些『无用』的东西不会妨碍你成为称职的程序员，但会阻止你成为好的程序员。

@JvmName
@JvmStatic
@JvmField
@file:JvmName
@PureReified
@Contract

这些注解可能我觉得对，如果想多了解这些八卦知识最好还是去关注一些高理解层次的 Kotlin 工程师，这里当然我就只知道冰封哥（ice1000）和 R 大（rednaxelafx@iteye）了（

reified 这个 type parameter modifier 也可以了解一些
至于 Kotlin 里 super 关键字调用祖父类（父类的父类）里的方法也可以学习一下

https://kotlinlang.org/docs/reference/classes.html#overriding-rules

open class A {
    open fun f() { print("A") }
    fun a() { print("a") }
}

interface B {
    fun f() { print("B") } // interface members are 'open' by default
    fun b() { print("b") }
}

class C() : A(), B {
    // The compiler requires f() to be overridden:
    override fun f() {
        super<A>.f() // call to A.f()
        super<B>.f() // call to B.f()
    }
}

Kotlin 语法的确非常的灵活非常有表现力，但是，我觉得现在学 Kotlin 的程序员最好还是看看诸如《Kotlin 极简教程》之类的东西，不要连 mapOf(1 to 2, 2 to 3) 这个东西的 AST 是什么都看不透（注意 infix notation 中缀方法调用表示和 vararg）

祝大家新年新气象，技术无论在深度和广度上都得到提升。画画布局的越做越好看，灵感各种报（爆）表（_），身体健♂康万事如意

说完了。It's over.

#yearPassed #life #dev

#LWL的自由天空 新鲜出炉：《2018 年度简报》，小伙伴们快来围观吧！(/・ω・＼)

#Haha #PL #CS #China #dev

今日笑死

#Low #China #recommended hhhh 『洋』程序设计语言 禁止过洋节 NB.

我本来想法是吃瓜看戏，不过这个越看越觉得不对劲，越看越火大。
这伙人是脑子进屎了吧？智商不达标？
比如 这个
afc163: 早就做好了被骂的准备。

果然没写。上面那个是 https://example.org/咕咕咕

#PLT #Learn To #Proof 我也是刚刚注意到 (p -> q) 是一个单独的命题... 描述的是『由命题 p 成立可以推导出命题 q 成立』（p 『蕴含』 q）
命题 (p -> a) -> (q -> a) -> (p ∨ q -> a) 不一定要 p 和 v 都成立才成立... 可惜我现在才看得懂

写成 Agda 代码就是（基本是抄的，这里说了，所以不要喷我拿别人的代码『装饰』我自己的技能栈，至于前端和 PHP、JavaEE 系后端那一套我后来自会学不消吐槽）

data _∨_ (P Q : Set) : Set where
  ∨-intro₀ : P -> P ∨ Q
  ∨-intro₁ : Q -> P ∨ Q   

∨-elim : ∀ {P Q} {R : Set} -> (P -> R) -> (Q -> R) -> (P ∨ Q -> R)

∨-elim pr _ (∨-intro₀ p) = pr p
∨-elim _ qr (∨-intro₁ q) = qr q 

看不懂的话好好复习一下函数式基本理论，什么映射、定义域、递归函数、集合论、lambda 演算什么的，当然我马上就以小学老师的耐心讲解：

当然上面的那个

data _∨_

是一个代数类型（Algebraic DataType），

_∨_

那两条<del>斜杠</del>下划线表明这是一个 mixfix 类型操作符（类似 Kotlin 和 Haskell 里的 infix notation），或许类似 Haskell 里的 -XTypeOperators



(P Q : Set) : Set

P Q 都是集合，然后结果也是一个集合，这完全是我根据 Haskell 等简单语言态射（函数映射）理论造出的臆想，当然其实我还不够了解函数式


下面 where 之后的缩进块『二维文法』是定义的

_∨_

类型架构器们，有两个，分别叫

∨-intro₀

和

∨-intro₁

∨-intro₀ 由 P 构造出一个 P <or> Q 类型实例
∨-intro₁ 则由 Q 构造出一个 P <or> Q 类型实例

∨-elim : ∀ {P Q} {R : Set} -> (P -> R) -> (Q -> R) -> (P ∨ Q -> R)

: 是类型定义
val n : Int 这种

∀ 是 forall 

[全称量化]

在谓词逻辑中，全称量化是尝试形式化某个事物（逻辑谓词）对于所有事物或所有有关的事物都为真的概念。结果的陈述是全称量化后的陈述，我们在谓词上有了全称量化。在符号逻辑中，全称量词（典型的"∀"）是用来指示全称量化的符号。

比如定义 2 为一个参数的乘法（Haskell 里用 (*) 2 表示）

2·0 = 0 + 0 以及
2·1 = 1 + 1 以及

2·2 = 2 + 2

...

对任意自然数 n，都存在 2·n = n + n。
∀n∈ℕ -> 2·n = n + n （伪代码）

当然这是一个比较简单的例子。

对于此例，就是说命题对于所有 {P Q} 的可能情况都成立
<del>这就可见数理逻辑对于 chatbot 开发者来说是多么重要的知识范畴了</del>

P Q 你们都知道（但是我不知道是不是指在 data _<or>_ 里定义的那个，R 也是 Set）
后面的 -> 的后面就是我们逻辑上的定义了

(P -> R) -> (Q -> R) -> (P ∨ Q -> R)

∨-elim pr _ (∨-intro₀ p) = pr p
∨-elim _ qr (∨-intro₁ q) = qr q

然后两种情况模式匹配（Haskell 爱好者们肯定知道，ES6 和 Kotlin 说不定也知道），第一种是匹配 P 成立的情况

(P -> R) -> (Q -> R) -> (P ∨ Q -> R)
   pr    ->    _     -> (∨-intro₀ p) -> R            

我们最后的命题大概是

(P ∨ Q -> R)

，然后 pr 是 (P -> R)，p 是 (P ∨ Q) 里的一个架构器参数，类型为 P，直接 (pr p) 就拿到了 R，结束证明

第二种自明。仿照上例显然，请自己理解（喷，没有那么骚的念诗么

（理论上其实是会 Haskell 的基本都看得懂，因为逻辑方面也有这种比较 trivial 的内容非常容易理解，小学数学。还不是奥数。）
（是的，Agda 的函数签名语法我现在还看不太懂更难独立写出来，因为我不理解它后面的那些 theory，不过目前我还不太在乎这些）
（不过，反正你们也不会，那我不会就是有理有据的了，逃）
（这和过程式那一套理论不一样，更 naive 一些，🐸）
（好吧，扯远了，不是一个层面的东西）

说实话，那篇『简单的 Agda 定理证明教程』我也是看了两个星期以后才有能力做到那个『仿照上例显然』的证明的... 好菜啊

然而现在 ∀v -> rev (rev v) ≡ v 我还是不会证明... rewrite 语法糖要替换的逻辑关系也暂时无法理解，呵呵
where rev [] = []
rev (x :: xs) = (rev xs) ::ʳ x



rev : ∀ {n m} {A : Set n} -> Vec A m -> Vec A m

（都还是抄的... Haskell 我还会写，至于形式化证明那一套映射关系还不怎么了解）

如果对这一套 Mathematics 上的东西感兴趣的话不妨随便看看某些定律的证明，不管是数论范畴的还是逻辑学上的 🐸 比方说：五点共圆 hhhhh
其实偶尔弄一下这类无聊的东西也怪好玩的，不过不能实用。所以一直都是诸如我这种无聊的人干诸如理论学习这种无聊的事情，真的是相当无聊啊。

是这篇博文的配套阅读，当然里面内嵌的是 MathJax/TeX，当然我比较菜所以就讲不好。算了，总觉得可能... 即使不一定完全正确，也是有价值的。你们有心情学了就好。
结束。

#Github #Kotlin

🔨 1 new commit to MiPushTester:canary:

54fdfd3: refactor(app): use Kotlin

Signed-off-by: Trumeet <17158086+Trumeet@users.noreply.github.com> by Yuuta

一晚上 + 一上午，搞定 Kotlin 基础语法，用到哪学到哪（