一直很羡慕那些 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 实在太长，不好列出。

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

……其实我们的 LiterateKt Script 部分完全不止可以兼容 Kotlin 的，我正准备进行进一步的泛化，适配更多类似 Kotlin playground 的东西

LiterateKt 本身其实只不过是兼容文章的结构类型而已，它应该提供一个对外 code area 和 hidden dependency text area 的结构接口，并且针对 language 选择特定的常量配置，从而兼容更多 playground。

也就可以给所有『可执行』的代码，提供一个在文章内有结构、有依赖组织地嵌入的接口。

但是为了我们这个计划，必须要能够从某 tag 的 class 里面提取出它使用的语言

literateCodeFilter: has.cssClass("language-kotlin"),

这个改动是不向前兼容的，不得不再发布一个大版本

刚才听到有人提及 PHP Laravel 开发 #web 应用的……

其实也可以谈一个这里不必解决的问题， #JavaScript
唉现在居然还为这种问题困扰，虽然 chain fold 这个东西也不一定必须用于『编制程序』，也可以用于逻辑推导……

function joinBy<T>(join: (p:Predicate<T>, q:Predicate<T>) => Predicate<T>, ...ps: Predicate<T>): Predicate<T>

然后我们可以实现它

{
  return ps.reduce((a,b) => join(a,b) );
}

比如有许多 has.CSSClass 什么的，

joinBy(or, has.CSSClass("language-java"), has.CSSClass("language-kotlin"))

或者

joinBy(or, ...["language-java", "language-kotlin"].map(has.CSSClass))

当然也可以使用不常见的名字 foldr 什么的

function foldr(f, v, ...xs) {
if (xs.length == 1) return f(xs[0], v)
else return f(xs[0], foldl1(f, v, xs.slice(1, xs.length)));
}
foldr f v [x] = f x v
foldr f v (x:xs) = f x (foldr v xs)

foldr1 f [x] = x
foldr1 f xs = foldr f (head xs) (tail xs)

所以我们在能够区分 case 制造 Element Tree 之前，还需要一个 Map<string, [PlaygroundDefaults, PlaygroundFnGlobalId, PostprocessFn]>
其中 PostProcessFn 可以帮助一些与 #Kotlin Playground 对元素树的结构要求区别很大的 playground 完成兼容，比如修改 hidden text area 的 class 什么的。 #project

type PlaygroundDefaults = Object
type PlaygroundFnGlobalId = string
type PostprocessFn = Consumer<Element>;
type Consumer<T> = (item:T) => any;

我们的辅助模块依赖是可以用 require() RequireJs 来完成的

#JavaScript #web #Kotlin https://t.me/dsuses/3094

大概又咸鱼了半天，不过没有关系，可以不用太着急…… 🤪

https://github.com/darkreader/darkreader
#recommended #web #Firefox