呃，其实 infixChain3 写的不对，它必须 peek 才能做到预判是否直接 expr = op.join(expr, scanAtom())...
修复版本是这样，必须有一个共用变量 op , 用于 peek

fun infixChain3(): Atom {
var expr = scanAtom()
var op = scanInfix() ?: return expr
fun scan(op1: Op): Atom {
val rhs = scanAtom()
val op2 = scanInfix(); op = op2
return when {
op1 <= op2 -> rhs
op1 > op2 =-> scan(op1 = op2)
else -> impossible
} }
while (op != null) expr = op.join(expr, scan(op))
return expr
}

这也太迷你了，我还有一个差不多迷你的，不打算测试了，我打算去看 #acg 动漫《一人之下》了：

class Recursion<LAYER, R>(private val placeholder: LAYER, private val reduce: (LAYER, R) -> R) {
private var top = placeholder
private val frames: MutableList<LAYER> = mutableListOf()
fun mapTop(transform: (LAYER) -> LAYER) { top = transform(top) }
fun newTop(value: LAYER) { frames.add(top); top = value }
fun reduce(initial: R): R {
var accumulator = reduce(top, initial)
for (i in frames.lastIndex downTo 1) accumulator = reduce(frames[i], accumulator)
top = placeholder; frames.clear()
return accumulator
}
}

可以像这样用
val rec=Recursion<Int, Int>(0) { r, acc -> r+acc }
rec.newTop(2)
rec.reduce(0)

举个实际例子，链表化

sealed class Linked<out T> {
  data class Cons<T>(val head: T, val tail: Linked</*out*/T>): Linked<T>() {
    override fun toString() = "$head : $tail"
  }
  object Nil: Linked<Nothing>() { override fun toString() = "[]" }
}

fun <E> List<E>.toLinkedOld(i: Int=0): Linked<E> = if (i < size) Linked.Cons(this[i], toLinkedOld(i+1)) else Linked.Nil

listOf(1,2,3).toLinkedOld() #1 : 2 : 3 : []

fun <T> List<T>.toLinked(use_fold: Boolean = false): Linked<T> {
  val rec = Recursion<T?, Linked<T>>(null) { it, acc -> Linked.Cons(it!!, acc) }
  forEach { rec.newTop(it) }
  return rec.reduce(Linked.Nil)
}

尽管不能做到需要返回地址保存的 a.eval()+b.eval() ，但通过 newTop/mapTop 可以更自然地写部分需要部分递归的算法
而且这个 Recursion object 还可以加 ThreadLocal 复用，不需要每次使用递归函数都分配新 frames: MutableList

看来递归算法还是博大精深，这个抽象根本不可能做到 Kotlin suspend function 能做到的 DeepRecursiveFunction ，只能拿来写类似 infixChain 的这种算法，给它起名为 FlatRecursion 吧…… 因为有 mapTop/newTop 的区分

如果打算不用 Infix 树了，换成 reduce 栈之类的来减小开销， Lua 的嵌套深度算法也可以用 FlatRecursion 抽象来完成，不过必须多提供一个 reduceUntil({ limit < it }) {} 部分归约才行……

昨天晚上突然想明白 #Kotlin 的新 inline class 有啥用了，我之前一直以为就是个 typealias 的语法糖（比如 inline class IntHandle(val num: Int) 不就是其所有成员作 extension val/fun 加个 receiver=Int 么）

才发现即便限制构造器属性的个数为单个，它的类型参数也仍然是有用的，比如可以实现 Either<A,B> 么，这样 Kotlin 就和 TypeScript 一样可以弄 String|Int 的并集类型了？|･ω･｀)

inline class Either<out A, out B>(private val item: Any?) {
  val left get() = (item as? A)
  val right get() = (item as? B)
}

之前我一直不解类为什么可以内联，最开始给绝句设计的内联类，可以有多个构造属性但“不能有this”（就是说只能在局部构造，使用其成员但没法直接用），现在我知道单个构造属性可以特殊处理了。
零开销抽象真是太有趣了！

这两天我想实现最近设计的逆向计算表达式生成（就是把 +* 变 /- 的这种逆序+反向，只是未知只能有一个，具体要实现一个 findPaths { it !in globals } 细节不多说）

顺便也进一步理解了 ParserKt 最常用的结构们：
Stmts (Stmt ';'|newline) -- elementIn
Stmt ('L' Expr '=' Expr) | Expr -- OpChain.disambiguate, Seq(a,b,c)
Expr opChain(Atom, "+- *\")
Atom Int|Name|Paren where
letter [a-zA-Z_]
digit [0-9]
Int {digit} -- Repeat, toDefault
Name letter {letter|digit}?
Paren '('Expr')' -- Decide, Deferred

总结就是 Seq,Decide,Repeat,item,elementIn; Deferred,toDefault,calm 以及这次要测试的 OpChain(包含 .OpTree 和 .LazyStack 的版本, 这次的 DSL 你不给 infixl/r 提供 join 那就默认是 OpTree 了哈, 真给力)
以前 Seq 不是基于 Pair/Triple 的时候肯定还有 Pattern.convert, 哈哈

悟出了一个道理，就是如果对问题的理解不对，技术越高结果乱得越吓人。

在 funcly-ParserKt 的可用化过程中，我了解了如何处理 !(obj.prop[0])+1这种常见的算符链实际上需要左递归(chainl 也行) 不然 !xs[0] 的优先级会错、明白了 Java 的 field/method 成员、 Python 式 name: type = init 如何用 concat(p1, p2) 和 OpChain.disambiguate(Name) { if (peek == ":") /**/} 表达式前缀关键字的消歧义（其实不需要真正的 lookahead 来解决）

加强了 Piped 组合器(包含 showBy,run,greedy,leftRec 等便利组合)，解决了 ParserKt 通往实际可用于 C/Java/JS/Kotlin 解析乃至文本链接/日期/关键词读取的“最后一公里”（迫真）

不过在我解决 LexerFeed 的时候出现了个问题：
首先说明，这个 LexerFeed 是利用 ParserKt 最具特点的 peek/consume() Feed 流预先跳空格的过滤流，利用嵌套流是最近才想到的点子（之前一定要像普通 PEG(parser exp. grammar) 一样非得在 Pattern 里侵入式读取/略过空格 违和感太强，是我傻逼了） （老实说这次重新设计我感觉自己以前的就是傻逼设计，竟然不把 BidirMap 提出来…… 害的存在 PairedTriePattern 这种莫名其妙的东西，简直和因为没有 peekMany 而造成的 StickyEnd 问题一样草）

如果是 C 式辣鸡文法，用单层状态机也就可以了，可咱的 Kotlin 当属语言小王子，我的 LexerFeed 是为下一层的文法定义自动过滤掉所有空格（当然也可以选择保留缩进或者剔除换行，只要不影响语义），这样 "1 + 2" 过一遍就只见 "1+2" 了。

至于 /* */ 式必须再 peek(1) 的注释就需要有请子类 SkipWhiteFeed 处理了，它实现 FeedControl.peekMany （话说我最近的设计对 instanceof interface 用得真多…… 太过分了），当然注释也是可以保留的， SkipWhite 类会有一个 beforeWhites: MutableMap? 保存 AST 对应的前部空白，具体做法是用 pat.alsoDo 。

但 Kotlin 首先支持 "${"a"}b" 这种嵌套模板字符串（现在很多语言如 C#, Groovy 都支持），其次是它的中缀链有不能跳过空格的部分（ a+b*c 你能跳， a to b in args is Boolean 你敢跳么？跳了就变单个标识符了）

对这两个问题， Kotlin 官方“利”用 ANTLR4 的丑陋回答是 KotlinLexer.g4 几乎包含了所有 Kotlin 的文法结构，远远超过词法定义该有的范围，要不然没法处理空格啊呵呵呵→_→

幸运的是 ParserKt 才没有这些破事，作为一个拥有组合解析器优越性和强大生命力的框架，它不必分出什么 tokenizer 和 parser 所以自然不会把 fun :List<T>=1 这种搞混（即便现在我部分隔离出了一个 LexerFeed 流过滤器来跳过空格）

对于第二个问题的前置部分，要么然利用原有 Function 值的解析器来读取需要保留的 字符串/关键词("fun ", "class " 里的空格，但这不科学（ funcly-ParserKt 是基于函数式内联提升性能的，不可能窥见 Seq,Decide 到底得到了。啥参数）

确实可以让部分组合读成字符串或计数的形式，但这样 LexerFeed 必然在下层请求 consume() 的时候从一个队列里拿结果，而且这等于字符串什么的都读了两遍（只能是字符流， "\"s" 这种转义还是要处理），这与 ParserKt 所推崇的 single-pass 解析是背道而驰的（本来递归下降法都会在调用栈上分配相当多的空间了，何必预读甚至多遍处理）

当然也可以选择加个 QueueFeed, 然后在另一线程同步运行 "keep" Pattern, 只要发现在运行就不跳空格，但为保证 wait condition 会调度上，每 accept(peek) 一次都得 Thread.sleep(0) 保证同步，看起来是只过一遍，实际上比过10遍还费资源（而且不支持KJS）。

于是，只能从主动读取的自顶向下解析换成被动状态转移的自底向上…… 只要 state != 0 就不跳空格

我设了几个基于 Array<Int> 的猜想，最后创建了一个基于 MutableList<LexerStateMover.T/*(chars,next,fail)*/> 的编号状态机及其构造 DSL
比如 "\"s" 的字符串可以表达为

val mover = LexerStateMover(s_zero=0)
mover.build { seq("\"") then br("\\" to seq(any), "\"" to seq("\""), any to keep) ) }

这样鬼畜的状态转移式而不定义式（其实也比较巧妙，我给它制订了 charTest 和 action 这些基础功能）

好先说第二个问题，我发觉 Lexer 流根本不可能比 parser 先知道是 "1 +2" 还是 "1 to(2)"，它连合并空格都做不到（毕竟视口只有1）

于是看起来唯有通过 peekMoreWhile {it.isBlank()} 这种黑魔法来做了，它看起来有点像 chunked():

fun <T> Iterable<T>.chunked(chunk_size:Int, op: (T)->Unit) {
  var n = chunk_size
  var list = take(n)
  while (true) {
    for (i in 0..n) op(list[i])
    n += chunk_size
    list = take(n)
  }
}

大概就是不断以 0..i<n 的 list 子集调用 op 且以 chunk_size 为批量来预取，比单层循环每次看 size 够不够再扩充或许快一些。
我应该是魔怔了，竟然觉得这个好像很有意思一样。

后来我发现了个绝妙的解决方案：让解析部分和流部分合作，不必复制粘贴解析器来写分词器。
解析器只负责处理表达式部分的空格，与 Lexer 交换解析状态和跳空格方法
这也意味着状态栈——ParserKt 部分是递归的，所以不止嵌套表达式能读取，字符串内联的递归问题也解决了（如果要跳过可嵌套注释，也能解决）
本来用 action 也能手动实现状态栈，现在给标准化了，嘿嘿(º﹃º )

总之，遇到总觉得不优雅之处还得多想想，或许会有更好的解决方法呢？

kotlin 怎么传 Function<T, R> 的参

1.4给了 fun interface的SAM

说起来我看 ice1k 的 agda 群组常年没人讨论，还打算加两条OT一样的
https://t.me/ice_learn_agda_chat/267

后来发现我这好心根本就是鬼扯，其实人家根本不缺废话；何况我不处理 Haskell/Scala 系语言和其它编程范式的

感情很复杂，这个语言 ice1k 也不是没讲过，只是他把老的入门性 agda 博客都删了，何况这些问题即便讲不好也没啥可怪的，它本身就复杂。

譬如递归 reverse 链表：

rev (x::xs) = [x] ++ (rev xs)
rev [] = []

要把这个思路切换成怎么归纳证明 rev (rev xs) = xs 从而 forall x xs. x:xs = (rev xs)++[x]
或 =(rev xs)++r x 是很困难的

（怎么今天看了就好像只是构造数据结构再相等性一样平常，之前可是很不解的……）

好吧，那我就不用 Agda 先讲讲
归纳证明是对序列的俩成立：对首项『基线』成立，对每项都基于前命题成立（命题证明不是布尔，没有失败一说）

比如咱有 listOf(1, 2, 3).fold(0) { a, b -> a+b } 需证明结果不小0:
基线 [] 恒成立
递归 (p, x) x不小0

当然加数都不小0 只是一种子集情况。
我们能以 xs.fold(true) { p,x -> x>=0 } 测试输入成立性，如果你觉得这玩意是类型，那说的就是“那个”编程了。（看不惯我混乱理论可以自己科普）

我们知道类型系统就是可以“否决”某段程序的东西，所以它实际上是在定义某种关系性的约束（比如 paramType in type.impls 这种 trait(interface) 实现约束）

如果这个可以在约束上定义些计算，或者说类型检查期也能做递归匹配的话，就是 dependent type 了（刚才的例子结果 >= 0 的实际情况只能算全再判，更像编译期计算了）。


好了看看 rev (rev xs) == xs 怎么证明，肯定一头雾水，但想想如果你构造的不是『类型』而是判定器会怎么做？肯定是算完再试等……😂 不要那样。

等式的右侧是数据，左侧是两层调用；如果下手得从左顶层的 rev, 而要证明就必须得出 (rev xs) 与 xs 本身的关系再作归纳，好像你能“解构”这个调用一样，你会怎么解构？肯定是 xs++[x] == x::(rev xs) ，当然等号反过来也一样（自反性 identity/reflexive 的交换律）

想到 xs++[x] （把 xs 全串到 x::[] 上）你一定记得 xs 在这里意味着递归栈了，因为 (xs++ys) 隐含着二者长之和+1([], nil) 的递归栈

(xs ++ ys) = cat xs ys where
cat zs (x:xs) ys = cat (x:zs) xs ys
cat zs [] (y:ys) = cat (y:zs) [] ys
cat zs [] [] = zs

这里我们用了第三个链表，是因为必须从 xs 的尾部，逆序 ::(cons) 到 ys ，其实不嫌麻烦也可以 foldRight(用栈逆序) :

(xs++(y:ys)) = xs++[y] ++ ys
(xs++[]) = xs

嘛，这个非常不动态编程(DP)弱缓存，例一用 tuple 保留zs也可实现，不得不说 Haskell 的模式匹配函数的确直观反映了各种流算法。

跑题了，假设你得出 forall x xs. x::xs == (rev xs) ++[x] 呃不是 x::(rev xs) == xs++[x]

（好吧二者是不一样的，记得主语始终在 ++[x] 的部分）
（注意要解构等式两边，都必须用到递归栈，第一个实际上是正向 rev 的定义😞）
可以通过以下方法证明 rev (rev xs) == xs ：

-- x::(rev xs) == xs ++[x]
xEqTail : (a, [a]) -> [a] -> Bool

idp = (==) -- eq path
revId (x::xs) = -- xs++[x]
xEqTail (x, ) && (revId xs)
revId [] = (idp [] [])

等等， x:(rev xs) == xs++[x] 这个等式不对，我没注意到 (rev xs) 和 xs 本身的区别…… 其实是 x:(rev xs) == (rev xs)++[x] ，意味着 x:xs == rxs++[x] ……
算了写不出来😢不多说了，入门科普而已。
顺便：代码部分可以理解为交换 ::(has type) 和 :(cons) 语义的 Haskell, 反正我不是说正经的。

上面证明 rev (rev xs) = xs 里我解构施用层 (rev xs) 到 x:(rev xs) = xs++[x] ，其实是 rev (x:xs) = (rev xs) ++[x] 的反向变形。

我显然把右边的 xs 理解成其参数了（虽然对正常程序猿 等式左边才能有未知量是直觉😂），没注意到关系解构的部分必须以 (rev xs) 描述，例 rev $ [1,2,3] 可不等于它++[1] 呢…… 但是 [2,3] ++[1] 就对了

这个点子是我在提示下独立想出来的，但思想和实践总是隔着基础模型的桥梁，虽然能设计、找到特色点也远不等于能细分并逐步实现，知道理论不等于善于实行。
不过，我仍希望这对大家有帮助，哪怕是理解别人的误区和失败。

只要可能对人有帮助，我才不怕出丑丢脸；毕竟相比技术和创造，自尊太微不足道了。

把 rev (rev xs) = xs 里的 (rev xs) 与 xs 互换即可得到 rev xs = rev xs 全等，可这不是“移项变号”或“两边同时减”那么简单（虽然也可理解为“把rev移到另一侧”呢），但不管怎么样显然是重组 a:rev$v=rev$a:v 这种关于 rev 结果的关系

以我目前这层面的水平当然仍是无法做到定理证明啦，虽然它也有意思。 #cs #plt

话说部分读者你们也被不明觉厉加入那个讨论组唉，还是劝退好了

人家千里冰封说的明明白白，必须有 dependent type 基础，并且他是不负责给你打基础的，狠心点：

菜鸟别以为和大牛在一起、或者看大佬做事就能给自己涨知识，没用的。

接近那个领域，也别以为自己看它的文档、用它的术语你就属于它。
系统的知识网络和直觉不是靠生硬的文字和无聊的名词能表达的，名词和定义规则背后隐含的是前人真切的思考，你不学他所学怎么能真懂他。

有些人就是天才，你和他差的就是人家能独立得出而你无法get到的一句话、一个小思路，有时候是因为知识和经验，有时候 1% 的灵感就是靠努力无法填补的。

不要以为自己足够热血或者“非常想”就能成功，科学说了算。

也不要自作主张认为“我需要那些东西来帮助进步”，不你不需要😡。阻塞在一个目标上不懂变通、提升知识广度，那叫环形等待、死锁。

说错了话他们不耐烦你也不开心，本就不是一路人，派系不同何必凑数。