现在对示例程序的编写方式已经比较成熟了，都是直接在一个 literate 写一个模块的某层次的基本构件，再在里面写 depend 它们的示例和辅助示例的算法。
想了半天，才想起来冰封当时讲的 coinductive 的那个 copattern 其实是指『以如何被解构定义一个数据对象』
冰封当时说，数据对象的结构可能是无穷的，但解构使用肯定是有穷的。
冰封当时说，数据对象的结构可能是无穷的，但解构使用肯定是有穷的。
head ones = 1
tail ones = ones
这样是 ones = 1 : ones
duangsuse::Echo
https://ice1000.org/2019/11-13-AgdaTac.html 看完了 #math #cs
都很容易理解吧？还不会 Agda 语言的我用中文翻译一下：
"lemma1" 是『引理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 是『一致』的意思）
排版有修改，算了好像依赖
算了，看来不懂还真是翻译不了啊……
"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 实在太长，不好列出。算了，看来不懂还真是翻译不了啊……
Stack Overflow
refl in agda : explaining congruence property
With the following definition of equality, we have refl as constructor
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
and we can prove that function are congruent on equality...
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
and we can prove that function are congruent on equality...
……其实我们的 LiterateKt Script 部分完全不止可以兼容 Kotlin 的，我正准备进行进一步的泛化，适配更多类似 Kotlin playground 的东西
LiterateKt 本身其实只不过是兼容文章的结构类型而已，它应该提供一个对外 code area 和 hidden dependency text area 的结构接口，并且针对 language 选择特定的常量配置，从而兼容更多 playground。
也就可以给所有『可执行』的代码，提供一个在文章内有结构、有依赖组织地嵌入的接口。
LiterateKt 本身其实只不过是兼容文章的结构类型而已，它应该提供一个对外 code area 和 hidden dependency text area 的结构接口，并且针对 language 选择特定的常量配置，从而兼容更多 playground。
也就可以给所有『可执行』的代码，提供一个在文章内有结构、有依赖组织地嵌入的接口。
duangsuse::Echo
……其实我们的 LiterateKt Script 部分完全不止可以兼容 Kotlin 的，我正准备进行进一步的泛化，适配更多类似 Kotlin playground 的东西 LiterateKt 本身其实只不过是兼容文章的结构类型而已，它应该提供一个对外 code area 和 hidden dependency text area 的结构接口，并且针对 language 选择特定的常量配置，从而兼容更多 playground。 也就可以给所有『可执行』的代码，提供一个在文章内有结构、有依赖组织地嵌入的接口。
但是为了我们这个计划，必须要能够从某 tag 的 class 里面提取出它使用的语言
literateCodeFilter: has.cssClass("language-kotlin"),
这个改动是不向前兼容的，不得不再发布一个大版本
duangsuse::Echo
但是为了我们这个计划，必须要能够从某 tag 的 class 里面提取出它使用的语言 literateCodeFilter: has.cssClass("language-kotlin"), 这个改动是不向前兼容的，不得不再发布一个大版本
其实也可以谈一个这里不必解决的问题， #JavaScript
唉现在居然还为这种问题困扰，虽然 chain fold 这个东西也不一定必须用于『编制程序』，也可以用于逻辑推导……
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)
唉现在居然还为这种问题困扰，虽然 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)
duangsuse::Echo
但是为了我们这个计划，必须要能够从某 tag 的 class 里面提取出它使用的语言 literateCodeFilter: has.cssClass("language-kotlin"), 这个改动是不向前兼容的，不得不再发布一个大版本
所以我们在能够区分 case 制造 Element Tree 之前，还需要一个
其中 PostProcessFn 可以帮助一些与 #Kotlin Playground 对元素树的结构要求区别很大的 playground 完成兼容，比如修改 hidden text area 的 class 什么的。 #project
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 来完成的#TypeScript TS 也有『半dependent type』的特性——输出类型可按照实际参数而定。
interface Monkey {
Hou: HappyMonkey;
Jun: SadMonkey;
}
function getMonkey<K extends keyof Monkey>(name: K): Monkey[K] {/**/}
duangsuse::Echo
现在对示例程序的编写方式已经比较成熟了，都是直接在一个 literate 写一个模块的某层次的基本构件，再在里面写 depend 它们的示例和辅助示例的算法。
在更新自家 Fedora OS installation 的时候顺便说一下。
之前的模型是一个 Literate 对 N 个 language-kotlin 的代码块，然后显示代码的时候拼起来创建 <code> tag 交给 KotlinPlayground 做后续工作。
现在可以一个 Literate 对 N 个靠“可配置”的
所以 show code 时也不能直接拼一起了，不得不把 filterCode 这个工作流程给取消，直接让 enableCodeFilter 程序靠 filterCodeTag 滤出内部 language-* Element 分语言拼合处理，加 button，其实也不太难，要用到我之前定义的 hist(ogram) 直方图来组织按语言的 <code> 创建，然后可以沿用之前的 <code> 创建工作流，这个过程是按 language 分的 for-each，目标是 appendChildElement。
我个人觉得，应该是给每个 literate 选择一个语言，也更加符合现在 LiterateKt 的设计原模型。
之前的模型是一个 Literate 对 N 个 language-kotlin 的代码块，然后显示代码的时候拼起来创建 <code> tag 交给 KotlinPlayground 做后续工作。
现在可以一个 Literate 对 N 个靠“可配置”的
Map<LanguageId, [ElementConfig, Consumer<Element>]> 来（之前那个 ElementConfg 是 DOM ElementAttribute Map、Consumer<Element> 是 PlaygroundGlobalId）所以 show code 时也不能直接拼一起了，不得不把 filterCode 这个工作流程给取消，直接让 enableCodeFilter 程序靠 filterCodeTag 滤出内部 language-* Element 分语言拼合处理，加 button，其实也不太难，要用到我之前定义的 hist(ogram) 直方图来组织按语言的 <code> 创建，然后可以沿用之前的 <code> 创建工作流，这个过程是按 language 分的 for-each，目标是 appendChildElement。
我个人觉得，应该是给每个 literate 选择一个语言，也更加符合现在 LiterateKt 的设计原模型。
type ElementConfig = Consumer<Element> // defined in dom.ts
type Consumer<T> = (T) => any // defined in util.ts#recommended bpython
dreampie
两个都是 Python interpreter 的包装
bpython version 0.18 on top of Python 2.7.17 /usr/bin/python2
dreampie
两个都是 Python interpreter 的包装
[DuangSUSE@duangsuse]~% sparkleshare
exception inside UnhandledException handler: The type initializer for 'Sparkles.Logger' threw an exception.
[ERROR] FATAL UNHANDLED EXCEPTION: System.TypeInitializationException: The type initializer for 'Sparkles.Logger' threw an exception. ---> System.InvalidOperationException: ValueFactory attempted to access the Value property of this instance.
at System.Lazy`1[T].CreateValue () [0x0003a] in <373b6e083d6e45e498c9082a8eebd27f>:0
--- End of inner exception stack trace ---
at SparkleShare.SparkleShare.OnUnhandledException (System.Object sender, System.UnhandledExceptionEventArgs exception_args) [0x0000c] in <330346ba25694cbab2d9ef3ec7a020a1>:0