才体会到工程的难度，原来测试不过不能 push 是真的！我刚才发布了一个 v1.2 一上来就是修完 bug 没修好，不能用的版本！
一个新版本居然不能用？？就发布了？？工程管理不善？？太难了！！！

看来测试不是谎言…… 除非真是大师级的人物，不然一次写对真的不容易呢

有点怀念当年用 subslice 写『解析器』、分不清 call-by-value、call-by-name、call-by-need 的时候了，现在设计实现语法、模式什么的根本没有难度……
但是工程总是需要时间，而对这个时间的预估我目前仍是眼高手低

https://duangsuse-valid-projects.github.io/Share/Others/essay-kotlin-parser
#Kotlin #blog #PLT 自从有了 Literate Kotlin，旺财再也不用担心我写不出代码了。 🤪

#Kotlin #dev #life #CS #PLT 多少人幻想着香槟，却只有喝速溶咖啡的命…… 眼睛好疼。

LiterateKt 真是很赞，虽然它也还没用上啥非常不得了的技术（用上也不该是以网页脚本的形式）

但是，就目前而言好像也没发现任何问题，偶尔处理不好文章的依赖组织，发生了多层嵌套的情况错误了，其实也是因为自己没组织好文章分区的关系，重新组织发现很够用，自动依赖关系解析也不会对循环依赖多给结果导致 Kotlin redeclaration。

唯一还不够的是文档里没写明两种依赖求解方式对输入结构是否递归的要求，明天考虑修一下……

https://github.com/quickjs-zh/QuickJS#DOCF3

QuickJS #JavaScript #PLT #CS 不支持尾递归呢

#dev #JavaScript 😂 写着写着就写了个笑话上去

#ML #CG #ANN

一直很羡慕那些 VISA(Video Image Speech Audio) 和 ML 的研究者啊，什么 2D、3D、透视、正交、旋转、空间、对应…… 然后效果都好得多的多了，可我还要做很久的基础，也不能说实操 #PLT 领域一些高级的工作如逻辑式定理证明

好像 dependent type、逻辑式、关系式之间不存在直接联系。

呵呵，有什么用呢？我不懂也只是被喷，不会有人理解我，他们也都喊着谁懂我、谁来救救我…… 难道就是这样？一定有更好的方法……

我对文章的代码依赖进行了一些整理，现在整个文章的 Kotlin 代码结构相对规范了很多，不存在为了教学目的设置的不成熟 code 被放在顶级 literate 里的情况了。

如果有 LiterateKt 的 CLI 项目生成工具被写出，这整篇文章甚至都可以直接拿去编译。

现在对示例程序的编写方式已经比较成熟了，都是直接在一个 literate 写一个模块的某层次的基本构件，再在里面写 depend 它们的示例和辅助示例的算法。

#Chinese 『你说的』引用的是『你说的东西』
『你说得』引用的是『你说某事的这种行为』

想了半天，才想起来冰封当时讲的 coinductive 的那个 copattern 其实是指『以如何被解构定义一个数据对象』

冰封当时说，数据对象的结构可能是无穷的，但解构使用肯定是有穷的。

head ones = 1
tail ones = ones
这样是 ones = 1 : ones

https://ice1000.org/2019/11-13-AgdaTac.html 看完了 #math #cs

都很容易理解吧？还不会 Agda 语言的我用中文翻译一下：

"lemma1" 是『引理1』，可以认为是辅助“函数”

（我们知道，自然数是跳通过 data Nat = Zero | Succ Nat 的方式定义的，不解释了，就是任何自然数可能是 0 或其他自然数的后继元 (x+1)）
注意上面是 #Haskell 代码，下面 (q -> r) 是喂一个 q （类型的）值，可以拿到一个 r 值的意思。
(Zero :: Nat)、(Succ :: Nat -> Nat)

引理甲：对何a皆有 a+0 == a
引理甲 zero = 自反 （此时 a=0，0和0自己完全一致）
引理甲 (suc a) = cong suc (引理甲 a)

（归纳证明 0+0=0、(a+1)+0=……）
归纳是有一个基线，然后对所有情况都可以通过某种手段归到基线得证，和递归一样。
（cong 是 congruence relation 的缩写，congruent 是『一致』的意思）

cong : ∀ {a b} {A : Set a} {B : Set b}
(f : A → B ) {m n} → m ≡ n → f m ≡ f n
主要看上面的类型签名，(suc : Nat -> Nat) 0+0=0，forall m n，0 equivalent 0、(suc 0)+0 == 0、(suc (suc 0)) == 0、……
cong f {x} {y} p = J {C = \x y p → f x ≡ f y} -- the type of equality
-- of function results
(\_ → refl) -- f x ≡ f x is true indeed
x y p — Sassa NF
排版有修改，算了好像依赖 J 实在太长，不好列出。

算了，看来不懂还真是翻译不了啊……