有没有协程大师解释下（

#Rust 的 struct/impl-fn 设计非常好(好像还能作union.. ) ，也支持闭包
std 有一些 box,ref,Vec,Map 的对C++ 习惯也很直接，而且有unsafe 能取代C
值类型&mut和(i8,i8)、流控匹配， FFI 和 Emscripten 也很好 (尽管不如Kt重视语义性
总之和 #Go 这种民科语言是完全不同的，mivik/kamet,rin 都是以rs 为原型（尽管不支持匹配解构）

但是设置环境是要花时间的，如果你的程序就那样，用什么语言其实没必要。 Rust 的分配期推导越来越好了，语言工具也完善内部。基本可以直接从其他语言翻译，但是什么语言其实都一样的..

#js [Forwarded from 每日 AWESOME 观察]
francisrstokes / super-expressive
一个轻量级 JavaScript 库，它允许您用可读性非常高的代码构建正则表达式。让你在几个月后，仍然能读懂自己写的正则表达式。

Rime RainSlide, [2022/1/18 下午2:08]
那么，能把已有的正则表达式转换为它的函数链吗

duangsuse, [2022/1/19 下午10:22]
魔怔了， Kiot 也是这样的，但还是有正则解析

根本无关可读性， 等人学会了正则只会烦于无法重构，你多写几个试试。 又不能config ，concatRe("^" , ()=>rand()? "a":"B" ) 都强
如果一个人不懂正则.. 那他第一次是怎么写的，而且这货都不知道有没有 converter , 不能反向兼容，有整这些字串拼接的心不如写个科普文档

和 Javapoet 一样都是属于低级抽象，某知乎大佬的 ObjectRegex 或 py _re.SRE 正则对象多好，列表/嵌套文法都能处理，不会弄这种类似C宏的低意义代码。 regexp101.com 才真好呢

这是正则引擎…… 不是 regexp code 封装

呃... 现在缩进文法的语言 lexer确实应该识别 : 后的空格 ，但这是整个 lex-yacc的问题（？？

脸黑君 （我會很生氣, [2022/1/19 下午10:46]
那你想重用的时候是亲自封装还是搞个这东西

duangsuse, [2022/1/19 下午10:48]
这个是实验，我是说那个 "a".repeat() = "(a)*" 的东西，还弄什么 .end() ，怕是内部维护了一个 [] push pop 吧，估计才学会这个就整框架了，还把API做成这样，没有误人子弟的嫌疑吗
如果没做 re 到他框架的转换，就只会带来麻烦(虽然类似的“正则简化” 不是第一次了

duangsuse, [2022/1/19 下午10:42]
至少这个re 可以写成 Re().inpStart.maybe('0x').capture(repeat("A-Fa-f0-9",4) ).inpEnd.ok 这样的形式，调用链也别整太长了
调用链应该起到强化可选配置的作用，如果没有，那应该写成 User().alsoIt{name="xx";age=9} 和 {clas:"main", } 的直接形式，滥用不是很好

这个高大上的语法，我来个 this 上的调用归个类：
start/end ^$ 是 当前层+='^|$'
optional 不创建新层，其上 string 这些append 行为直接写入当前层[]
capture 和 exact(N) 是push(a=['()'|'{}'])，等它们 end() 时按 a[0] 信息 join 一层 — capture^.exact(2).str('x').end.str(y).end 的^ end 时会拼合 x{2}和y
anyOf 看当前层是不是只有 a-b 类的单项，若是则 [a-b] 否则 (a|b)

所以说技巧是好的，但是学会就用还需要多思考


他不会用 {noop: ``}["noop"] 吗... 果然像是JSer会做的 🌑(虽然我也是

还好吧，我觉得火不起来，要不然就说明前端只能靠 重写既有代码play 了
毕竟是涉及"二进制格式"的东西，刚才可能有点过火

http://www.yinwang.org/blog-cn/2015/04/03/paradigms
“JS 没法访问外层的 this，非得“bind”一下。Python 的变量定义和赋值不分，所以你需要访问全局变量的时候得用 global 关键字，后来又发现如果要访问“中间层”的变量，没有办法了，所以又加了个 nonlocal 关键字。Ruby 先后出现过四种类似 lambda 的东西，每个都有自己的怪癖…… 有些人问我为什么有些语言设计成那个样子，我只能说，很多语言设计者其实根本不知道自己在干什么。

🤔其实这是半对半错的。var self=this 问题可以用 ()=> 解决了，Python3 的 nonlocal 也不是没意义的，比 Java 的 int a;new T(){a=1;} Error: effective final 好，因为闭包一般不会mut变量，乃至 global ；然后 Ruby 的 ->(){} 和 do|| , Proc.new(&f) 确实是有严重问题，这方面它不如 Python , Matz 对技巧太贪心了。像 C# 尽管技巧多也不会出现函数值有几种写法的问题，但一入 Ruby 你就要学会 1.yield_self{|x| } 和 do|x| end 这些... 坦白说不值,但Rb是有历史包袱.

尽管它们都不如 Kotlin 。你看王垠批判Go，质疑 Rust ，但他敢直接怼Kt 的语言设计吗？只好捡了没 throws Exception 强制检查的问题(然而 runCatching{}.getOrNull 用的香谁会管他呢

http://www.yinwang.org/blog-cn/2013/04/01/lazy-evaluation
Haskell 的参数惰性计算确实需要一个0参闭包，而且是运行时的，较难优化 🤔 所以我觉得如果用指针set 去init 一个变量比较好，然而实际上 if(!init)x=initizr(); 里这个if确实要执行成千上万次，除非动态改汇编。也不是编译能优化的”解释器开销“
Unification(值/变量归一求解) 能用于简单类型系统，且不能推导 subtype 交集，他的逻辑性质名词(symm对称性)也是对的
代数数据类型(带类型参的 Sumtype brach) data A t { Lit :: Int->A Int ; Obj :: t->A t } 其实在 subtype+typeparam 里也能做吧
后来我还在这里看到 recursive type 是指 type R= T0+ Int*R (常规意义: +=| *=,)，于是 T0*Int*Int 都是这种.. 就是编译期允许递归 Type.check(inst:Type) 吧.. 算了，唉，我只是讨厌没有编译期计算
我以前都把 Bool*Bool=4 state, B+B=2 当冷知识看，没想到真有人把它当东西，置顶一个计科专业还说类型 +* ，还有 0=Void 1=() .. 于是 0*1=0, 0+1=1 ？还不如 insect/union 直白呢. [绝对报错/无尽]计算&T=Nothing, 它|T=T ，因为能算到的Nothing?就肯定不是throw,exit()等，所以意义？ 我跟数学老师说 Sigma_i=0^6 表示不如 (0..6).sumBy{} ，老师说那不过是个形式，无关意义。

乱ref英文名词和小众概念，老实说我现在是完全不吃这一套，要么你给我讲明白、指出我的误解，要么拿代码和解决的问题来， 抽象代数x编程，只当耳边风；要是具体一点还夸你厉害，毕竟大家都没空了解这些碎片，我怎么知道你有逻辑自恰性，或者只是碰巧通过检查的数学摘抄？

不过缩进文法(layout) 是香的..也没严重影响解析器的复杂性

http://www.yinwang.org/blog-cn/2014/04/18/golang
这个点评就写得不错，尤其是 TSorter{Swap,Len, Less} 真的比java.Comparator弱智了。
妈的， callback 都能叫 CPS(不返回编程/面向程续编程)，这么一想也是噢，调用能决定之后的取舍，怎么不是CPS形式.. Kt协程就是把 suspend fun 加个 callback 交互，因为它没有 TS 的 __awaiter 也不便用闭包this做Generator吧. 再通过StateMachine yield恢复 #kotlin

这里就体现了王垠这人是有真才实学的， 他的知识集不比 #zhihu 一众(公知都算不上,因为从不做科普)的PLT人差
很可惜后来越来越极端，而且也不乐意分享他的compiler.ss外一些其他成果；但就讲课&讲故事而言，

我觉得知乎的大家都没资格评价这个人，因为你们在这点甚至不如他.. 他的博客确实没逼格，话也没轻没重，但对CS科普的贡献是巨大的，真的不夸张。
大家都喜欢轻视「娱乐编程界」，但仔细想想，我们何尝不是娱乐编程人士？ 你的回答里贴了多少思路和代码，有多为提问者和公众程序员着想？
如果是为自娱自乐，不算在另一种娱乐编程吗？

ps. 我是不认为太自我的「个人博文」能算科普的。科普必须对不同做法有一定了解，有穿插和客观解读比对，告诉大家好坏要点，而不是代码的解说。不然本质上和"Java入门"教程也没区别

https://zhuanlan.zhihu.com/p/34064655 #zhihu #fp 这是个物理爱好者18年的 CPS 解释器实现文

这个代码质量.. 其实我是讨厌看lisp 系的，非常讨厌嵌套括号，而且这个人似乎在代码里插debug print ，以C的方法写Racket .. ，那我就把要点挑出来看看

函数式除了伪递归也可做尾调用优化，当 f=()=>g(), g=()=>1 时g可return 到f.retAddr ，类似函数内联。CPS也是尾调用
显然return/即 callstk.pop() 两次不叫优化，那么我们就需要 pop 外的方式使用调用栈，即保存 continuation程续 。(call/cc setAs-f) 抓住了调用后的步骤, (f) 就能跳回原位(可用ES6 func* 体验)；在工业语言里程续被用于断续执行一个函数，意味它可yield暂时回交执行权， call/cc 也一样，不过能替换调用栈。 这样调用栈就变调用图了，因为你可 longjmp() 到之前的栈帧..

call/cc 可在 generator 里实现yield ,乃至throwcc-恢复 (不过认为Lisp throw更高科技真的不现实。
想实现程续可不容易，因为解释器的执行是不可暂停的，而我们还要替换调用栈 ，于是要手写新的..

cps 解释器可以实现 callcc 。考虑 "1".eval() 时要等待、更大的 "1+2.." 要等待，若碰到 "(call/cc f)" 也等待，f 就拿不到 callcc f后的程续，因为callcc 是立即执行f的?

他是用了 handle-decision-tree , 一个 (eval exp env cont) 扩展，x[0](res=>res? only(decision=x[1])? exec(d=decision) : decide(d) : decide(tail))
eval-continuation-call 简单让 eval 的 cont=被闭包状态 ，因为[接下来的步骤 回调] cont 本身就是解释器状态

CPS化 eval() 就能保存状态..我之前只想过 func* 化，确实对 #PLT 了解不够。 比如 a+1 里 add: lit(v=> a,b=v) , cont(a+b) ，那如果 lit 把 add() 闭包保留住，确实就留住了当前程续，如果env 参数也在内，就是整个状态副本…… 不过没看懂单步操作为啥需 decision-tree (好像说 eval-fcall 的没这个就不能在 callcc 函数内运行

文末说要点是 callcc f 创建了 continuation 喂给 f，我只看到 cps 使得后序树遍历 Expr>Add>Lit 变成 Lit>Add>Expr 的反向形式，因此可回馈值 而非等待值，就能suspend ；我之前设计的 tvr 求值步骤模型里 r(treeRes) 好像也是这个效果，能保留树路径。从自顶向下组合 到自底向上化简,碰到callcc抓callback..我好像明白下面那个GLL 是什么意思了
eval-conti-call 则把包住的 env ,cont 重设，就替换了调用栈和当前 scope
如果 f=(k)=>的程续k没被恢复，callcc f 的值就是f()值。 callcc的eval(里cont= "call f" ) ，就指定此默认值

不过说起来函数式解释器 env 表全复制也挺高明的，就没有什么继承综合语法的破事了，解析期都构造好的深先序
以前那些人都说得太复杂…… 之前还有个CPS写解析组合子的，能实现memo..用了什么CPS特性? tramp(循环转化)和memo? GLL文法? 代码太长.. 就没发现CPS有啥特殊技巧的说

🥲我想起了去年冰封说”Kotlin coroutine 的 Context 就是CPS Context“ ( runBlocking{ launch{ delay(1000) } } 两个suspend调用里啥算内部协程,还是两个孤立调度的)，然后我一脸蒙蔽- 断续函数就是可暂断回调度器的函数，和CPS有啥关系？ ES6 里也只和 __awaiter 自动.then(resume) 有关啊，现在才知道 Kt coro 是自动callback:Continuation{suspend,resume} 化suspend fun，内部调用等待，完成后交给最外层...

函数式妙……实在是妙啊, callback 这么的土，Kt 竟然用它实现协程？它竟是CPS? 真的大跌眼镜。看来相同的东西，动手操作不同，名词也就不同了

解释器，我自己也在写一篇。
http://www.yinwang.org/blog-cn/2012/08/01/interpreter
王某这个racket 再定解释器就是S-expr 系非常经典的写法了， 变量/常量和env, lambda/call, (eval expr env) ，但其实要说短也有更短的：好像删了..
😐坏耶，只是个后序遍历还藏那么深，殊不知Lisp系解释器作用域是代码最低的... 改天我写一个

看到这里，其实这些人除了S-表达式看起来很牛逼，代码质量真的不行；不是我讨厌圆括号，而是 (def prechk(x) (if (not (ok x))(err "fxxk") 正常逻辑 ) ) 还占缩进这种写法真的难看，我最讨厌平铺直叙的程序 🙏
许多人尽管是大佬，但写的代码仍不敢恭维，或者有改进空间；而因为他的思想正确、领域牛逼，言辞有特性，就觉得他什么都好， 我大可不必。错就是错，风格是慢慢改进的。 尽管牛逼，如果言不及义，也只能说他不善表达..意识到才有改进空间

除了PLT，我也在发展一些其他的API见闻，在我眼里什么领域都是平等的，表达只有目的和废话，没有谁更牛逼的说法。

看看人家函数式在干什么，这群魔法师在干什么。 CPS 不比那个 eval() 都不会写的 parser状态机魔法师强

AST with Scope - 脚趾头的文章 - 知乎
https://zhuanlan.zhihu.com/p/75073557

SKI 是”替换、重命名、即得“的意思吗， de Bur.xx Indices 是拿编号替代参数？
代表一个变量的索引 为 距离 该变量所定义的 作用域之间 的距离（之间嵌套了多少个作用域），比如：

这tm不就是词法域编译期变换吗？ de Bur .. 干掉了α-conversion(重命名. eta是规约=单步)，还干掉了shadow和capture (层叠域和 dict.copy)
我们将变量区分为“绑定”/“自由”变量：

你认真的？Lua 里有完全等效的逻辑

data Expr a 
  = FV a -- 自由变量不一定用String表示
  | BV !Int
  | App (Exp a) (Exp a)
  | Lam (Scope Exp a)
deriving (Eq,Show,Read,Functor,Foldable,Traversable)

—叠Buff呢,不然没灵魂了
这货上的FV(key) 还得用特殊函数来检出和替换。woc ，动态作用域表1次解决的事情，DBI 写得如此麻烦，仿佛它看不到工业界通用的方法存在一样，或者改个名字就是”lambda技术“专有的了

现在这个AST可以看做一个放着FV的容器，并实现了Functor，Foldable，Traversable（甚至可以实现Monad），可以通过一些通用的函数对AST进行操作，比如说判定一颗语法树对应的项是否是闭项(无Upvalue.. 不对,无global var)：
DBI是一个很好的让变量带上作用域信息的方案，但是就上面定义的AST的定义来说还不够安全，还无法禁止构造像Lam (BV 2)这样的不合法项。

First-Order Abstract Syntax —最简单直接的方法就是直接用字符串保存变量名 —有必要起FOAS 这样的”术语“？y
High-Other Abstract Syntax — HOAS???
这种函数式有资格说 OOP 术语是废话吗？直接学编译原理就成， HOAS 希腊字母? 除了语义丢了，有变化吗？

不过HOAS的缺点也是十分明显的，我们不能“看进”一颗HOAS里，于是就不能对其做很多操作，比如pretty print、优化 —Expr|=(Hole v) , 即内联注释...
^请问您说的Hole，是不是指符号的元数据(metadata)啊？
这真的需要代码示例？！ 一句话就全说明白了，然后我再贴这些废话代码示例

在有dt(datatype? dependent type...)的语言里，HOAS过不了strictly positive check(Agda, Coq 严停机检查)，也过不了total check。

data Vec : Nat -> Type -> Type where
  Nil  : Vec Z a --带长列表
  (::) : a -> Vec n a -> Vec (S n) a

data Expr a
  = Var a
  | Lam (Expr (Maybe a))
  | Expr a :@ Expr a

—DBI 也可以用Expr 编码住,不专门分支
-- λx.λy.x y z
-- Lam (Lam (BV 1 @@ BV 0 @@ FV "z"))
就很inductive，很abstract，很safe，很nice。（来自于paper）

装模作样..好像JS和Lua不是如此处理变量一样 ；顺序又不是人眼来填充的
移植的一个算法，仿佛是 lambda 自有的东西一样，还起个啥 de Bur啥的名字，带空格哈

https://dannypsnl.github.io/blog/2021/05/02/cs/strictly-positive-check
这个检查是针对程序即证明的，只要写出符合类型签名的程序就OK，因此类型系统比较强大，甚至都能不停机(死循环)啦

data Bad{ bad : (Bad -> Bottom) -> Bad }
absurd : Bottom —荒谬
absurd = notBad isBad
isBad : Bad
isBad = bad notBad

notBad : Bad -> Bottom --由Bad得到空集，是不可能的，但这里
notBad (bad f) = f (bad f) —f:Bad->Bot , (bad f):Bad


data Term{lam: (Term -> Term) -> Term}
type T=Term
app : T->T ->T
app (lam f) t = f t

w,loop : T
w = lam (\x -> app x x)
loop = app w w

前排提示: Y组合子(匿名递归)是 \f. (\c. f cc)(\c. f cc) 的形式，这个是 ((\x. xx) (\x. xx))
问题是这个 loop的值会在检查时计算(dependent type=type依赖值,即编译期计算) 会死机
其实可以从检查上预否决 Bad,Term 的问题
已有 A->B , A是逆变 B是协变，在那个类型轮用 -A,+B 表达，推广到 Pi(product,组合) type (有点像Scala
检查： Arg/Type 的左边(受值处)和本身属性相反 ； 的右边和本身属性(正负)相同；

比较怪的是我听说 type checker positive代表有错，negative代表通过…… 唉，总之别相信理论。 我想起某门CS公开课录屏上说，计算机是工程学科…… 理论界不统一啊，都是和数学拓扑啥的杂交来的啊……


我算是知道为啥这些不能实用了，因为实用领域有更通俗的等效做法了。而对另外一些能实用的，它们又太复杂(其实是有简单形式的但这些”语言“研究者不在乎,主不在乎) 😂 真是太可惜啦...

把我给整不会了。之前冰封每次念叨“你会 de Bur啥 Indices”，什么HOAS， 竟然是“善”用 #Haskell 实现 Lua(Upvalue,closure)早有，C语言(尽管无词法闭包) 早有了的函数参编号化/作用域闭包，而且装作不知道这回事一样？

是没有人教过他们怎么写 native 编译器吗，还 alpha conversation ，还 name shadowing 和 env-table capture ，a-自动重命名防冲突是不？先整体遍历 substitute 替换完再规约是不？文本repr 和变量实质的关系都没搞清楚，搁这学 ANTLR/PEG 呢！它们连JSON列表的',' 都没法忽略；
函数式连变量名String的语言分配都要搞“系统”！AST的阴影面，那我就用 First-order/首次 AST 和env表浅copy存储咋了，变量解析好好的为啥要动呢？Lua 的首次不仅把 free/bound 啥区分了，连寄存器都分配了，序列化也完成了；函数式是玩AST树玩疯了吧，个求值序 单步走之前最简单的值ref 还整幺蛾子，有种你和任何一门正经IR编程语言比，不要搞窝里斗

刚才我还夸函数式闭包CPS支持程续值的 interpreter approch 牛逼，现在就看到阴暗面了——env-copy，不思进取，等到想改进的时候，一大堆有的没的“专业术语”就出来了。 函数式根本不适合搞这个优化(每次写visit都得好长,还链表解构呢)，好不容易写出来。也难怪非得用术语显得牛逼，
然而并没有暖用，复杂性是多参列表处理带来的，JS完整实现要不了10行， Hs 的遍历法注定了它要给 extract instantiate 这样的树重构写些无用分支 make compiler happy——因为要纯要exhaustive穷举啊，于是你转换半天，最终还不如首次用嵌套表就分配好了函数的内外关系，而且你起一大堆“数学性”名字，也不能让代码跑得更快或更好读

或者是没写过 typeparam 或 unification 吗？类型参数的意义就是一致性、unification 的前置条件就是a=b=1的传递性，变量的语义是:第j参、上i层第j参、全局键名k ，统一个语义指代就得了，closure 就是把这些上层的Upvalue 复制保留下来，它是一个函数值的创建动作，因为函数内引用了外局部值也要存储空间

我就不服了，同样一个东西，就像lam叫抽象我们叫函数子程序，lam里叫应用，我们叫调用，lam叫bound/free我们叫局部和全局量，lam 里叫替换参数我们叫变量和存储空间，lam叫beta规约我们叫执行单步，eta规约我们叫内联，项我们叫返回值；Hs里查instance overload我们用subtype多态override；Hs 写伪递归 case/参数guard匹配我们用 forEach ；哪里有不一样，凭什么函数的就牛我们就土？他们就像拿刀背切菜， 如果不是为研究；如果自以聪明；就是蠢。 那人家刀锋你刀背，和人切得一样才你牛啊、比人切得效率才厉害啊，仅仅会几个等价 没意识到智商是搁在那的 人类极限是在那的 表达费力成品就辣鸡 只是分出了亏本精力用刀背就牛， 这叫做和plain编译器等效了？还有一大堆变形你没做呢，市面上没有多少AST形式的虚拟机！
我们把鬼都看不懂的lam 整理成了大家都实用于代码简洁复用的程序工具，而且本质就是lam，而 lam 呢？停留在纸面和扭曲符号莫名"严谨"记法里，写不出几个算法、适应不了大千世界；空洞夸张还自诩是原理，去你的原理，好像 eat(makeSoup(boiler,plate)) 任谁想不出一样，好像代码有定a=1 不letin就算副作用。整理几个重构就能叫优美，咋不说现在随便一个linter 都更能修改问题呢？

现代语言除了有替换和单步化简，还支持主语this、同名不同义、非侵入式拓展的特性，这些lam理论都描述不了，它的再生理论也说得迷迷糊糊，它有什么资格说自己是编程这个巨大集合的本源和“理论”？就因为最迷你？

而且Scheme 那套 eval(exp, env=copy) 根本就不能放编译器上用，编译时命名就消失了，变成调用栈上位置了，在解析后就已没有"a b c" 这种名字了，也就动态语言能玩 env 表浅复制当存储空间用，编译器的闭包创建哪可能把所有外层局部量，乃至全局量复制下来蛤？ 那也不比预先知道啥变量是 upvalue 更简单啊！
而且Lua 的func(){global=g+1} 编译结果，看有没有 getglobal 指令就知道是不是“闭合”函数了，比你信息量还大，你就只能知道有没有FV节点，它直接平展为列表了，这种引用统计性的分析不在话下
一大堆废话，变量就是和作用域名绑定的，从函数式和符号表看都是如此，还什么方案，这就是唯一途径；而且它也一点不 abstract ，相反更靠近汇编了；它当然很 inductive(归纳性) ，因为0年以前汇编和JVM就是 work as this way —哦，JVM是把Upvalue存在匿名子类上 也算内部field

这个 paper 就仿佛是在那个珠穆朗玛峰卖冰棒，还是在大兴安岭滑雪呢，怎么就这么飒呢，拿人东西改名还不礼貌用语，在代码里也不加致敬不给credit，直接把工业界通行的做法来了个狸猫换太子，我思量着Lua的作者93年 一个“民科”怎么可能知道函数式的这些呢，怎么就“英雄所见略同”呢 ，那JVM里 aload_0, getfield Main$0.lvar 又是干啥的呢 ，摇身一变蹭 lambda 热度，我球球您了 Lam 它是 1920s 年的老人了，别再混血了

S f g x = f x (g x); -- 值复制S(f,g(x)). a=1; f(a,a); = S(f,I,a) . jvm dup指令
K x y = x; -- 值选择. 见Church编码 (true a b)
I x = x; --S K K x = I x = x

那个红姐(thautwarm)脾气又不好，上次(木兰)听什么 Py3to2 Lambda lifting 我还挺感兴趣的，网上搜到1资料，最后看代码-不就是匿名外提为局部吗？ see(Lam)=lv.add(it.code); see(Def){...; for(lv.unnamed){stmt.unshift("k=v")} return it}
自己也说简单，那就在标题写明是兼容变换backport(lambda extract)啊，美其名曰lambda提升，我还以为是优化呢. JS也tm有var 提升呢，怎么还被人喷呢

真是受不了他们，Lam 演算由 单项Subst 函数Abst 调用Apply 甚至let这种语法糖构成，显然apply有些东西时(如 + 1 2)会直接得值,类似Java的native。函数可以引用任何绑定变量(词法域)
还把 Abstract 简写为 abs 、name 写成 n，这是数学？？绝对值和函数有毛线关系？你可以起短像f,fn,e，但语义不该含糊，更不能错位！
相比之下，王垠把 Currying 瞎起了个咖喱就好太多了，至少不是拽无意义洋文；反正对于不知道 Haskell B. Curry (一个组合数学家) 的人这个名字毫无语义

真不知道写过的人为什么会把这个当哲学，两个等价的东西，进入函数层深++ ，看见变量求个层差，就没什么好说了；亏纯函数戏多，所以我不太喜欢不实际的纯函数写法\

那段时间冰封知乎挂的都是这个 de Burj啥和HOAS+啥理论 ，我有关注他的博文，但都不是关于这些的入门级的东西；他的 slogan 还曾是“你懂(这个啥)Indices”吗？弄得我以为是高级类型系统的应用，没想到是这个代数杂交。那他是像让人知道所以问，还是不想让人知道 但害怕人不知道 所以问呢？

本文并不是讲解 Finally Tagless 的，只是讲解它和 Visitor 这种设计模式之间的对应关系的。 对于 Finally Tagless 本身的讲解和推导，可以看下面的文章。一个语文极好的人写的『一不小心发明 de Bruijn Indices, SKI 组合子和 Finally Tagless』一个语文极差的人写的『解决 HOAS 无法 look into 的问题，同时一不小心发明 SKI 组合子』

作者：老废物千里冰封

链接：https://zhuanlan.zhihu.com/p/53810286

类型系统简介 - 知乎用户frBud6的文章 - 知乎
https://zhuanlan.zhihu.com/p/65626985
超市买菜 - 圆角骑士魔理沙的文章 - 知乎
https://zhuanlan.zhihu.com/p/66349646

#PLT 魔法店里一些文章还是不错的(lambda类型系统, SystemF一大堆TypeNode 集)，可惜表达方式太弱了.(他们写LaTeX时仿佛不知道这些在Rust等土直里就是tuple/struct/enum-union ，所以只是贴了无语序的“数学公式”，没有告诉读者这些严谨符号, Product=tuple, Record={} ，其实和user视角是一样的，换了“除法”语序和符号而已，甚至没告诉他咋写typecheck，只是举了程序形式的 with a,b=M:=A*B do N:=R 类的例子，还有(Type inBasic)(Type Arrow AB) 后Valx/fn/app 一致性；我就觉得奇怪了，难道作者不知道这些在“工程世界”都有对应更直白的名词和示例写法？没见过另外一个世界？
一个简单的问题都找不到联系来比对，所以我可以合理推测更有意思的依赖值-类型 其实是因为他们语言和归纳能力的贫瘠，才弄得非常隐晦。可惜那样我就不懂了。

现在我也真是很草，喜欢用自创名词，
Continuation程续 reduce单步 tailrec伪递归 Unification值变量归一 CPS不返回编程=传程续=传回调 Currying颗粒化喂参
polymorphism同名多义 variance型参in-out位 closure变量域闭包 coroutine断续函数 prod/sum组合分支类型 first-class值
combinator可组合器具 callByName传闭包晚求值 EDSL码构语法树 Exception非局部级联返回
gradual-type部分类型 duck/dynamic-type无类型 <T,R>类型一致位
常量Lit 引用Var 表达式Expr 语句Stmt|组合句Block post-order-walk深先树重写/遍历 rev-polish算符执行序重排 recursive-descent前缀提取-return解析 数值类型提升-数值拓宽


还真是挺不严谨的呢🌚 几个字就定义，果然还是不如多态好，那样涵义就不确定了，可以随便外链和修改了。 再加上杂交数学表示法，就能过滤不少外行呢

“ 所以 co- 有了太多太多的译法：coerce 是围在一起，成了约制；covariant 是一起变型，成了协变；collect 是选出来放在一起，成了收集；conjugate 比作马车曲木的两端，成了共轭。coauthor 是合作者；codomain 是陪域。余、共、互、逆、陪、伴、协、同、交、合、配、对、逆、反、偶、上……我们在看到这个词头时，不必像意呆利那个把胸部当成 jiba 的曲直不分的家伙那样直译，而是像徐光启那样，直接看清它的本质是什么。知其变，守其恒，为天下式。当我看到陈意云老师把 coinduction 翻译成「余归纳」的时候，我很困惑：「余」在哪了？而当我发现 coinduction 就是把归纳的过程反过来后，自然就有了它的译法：逆归纳。「反」是一个静态的描述，而「逆」是一个动态的表述。当归纳的箭头有了流动的方向，逆流而上便是把箭头反过来最自然的想法了。于是在英语世界，有了很多关于 co- 的妙语：Q : What does a category theorist call a reader?A : A "co-author".问：范畴论学家把读者称为什么？答：「协作者」。
负负得正，看来 co- 是对合（involution）的。

如果你对知识进行了彻底的分析而非某种机械的套弄，在你脑中生成的概念与生硬的文字之间已经没有很强的相似性，我们就认为这个概念是被理解的。彻底的分析和非凡的变换，是获得真知的标志性特征。

作者：Oling Cat
链接：https://zhuanlan.zhihu.com/p/56285253

得了吧。天下没有一个理论那么简单，理论能涵盖自己，却忘了世界有许多它描述不住的东西。这只是个游戏，情绪自信什么也优化不了 #statement
知其变，领域太多你知不穷，更何谈变化。守其恒，抽象太多涵盖万物等于什么没抽象，抽象徳不配位、言不及义，仍需再优化学习。
从变中得不变，这种一时的欣喜终究是因为接触不够广导致的，它只是发展的第0步。人作为大自然的产物，一种动物，是永远无法获得真理的。
如果你总是自认为彻底理解了知识，你仍在排斥它。因为真正的理解彻底是与之相融，让它成为自己的语言，而不是把它当成独立概念；这个过程和那真知亦无不平凡，只是朝朝暮暮，反复出现，边角不断消磨，本质才得以显现； 一个人一类知识是有时间线的，哪像编译器那样彻底变换 一次成功；得到之后，只是相处的开始。获得真知 只是冷落了真知


"SICP"附近有点好玩的内容，像关于 表述-函数-描述式编程（不过描述式解释器我写过,感觉还是不能实现函数式的功能.. 那就要看 SWI-Prolog.org 啥的能不能用于查询外的功能，应该不能独立存在

👆 😐好了好了不看了，待会相关新文会在这贴链接。
” 如果你对知识进行了彻底的分析而非某种机械的套弄，在你脑中生成的概念与生硬的文字之间已经没有很强的相似性，我们就认为这个概念是被理解的。彻底的分析和非凡的变换，是获得真知的标志性特征。

如果你总是彻底分析理解了知识，你仍在排斥。毕竟将其归为自己的语言、与之相融才能真正实现理解，而非视其作独立概念；学习过程与真知亦无不平凡，只是朝朝暮暮反复出现，边角不断消磨，本质才得以显现。
一个人一类知识有时间线。哪像编译器那样彻底变换、一次成功；得到之后，只是相处的开始。获得真知 只是冷落了真知


文字不该是生硬的。我觉得。 如果作者足够好，概念就不会和文本相差甚远；别忘了 parse 也是种转化、逆语序也是弱相似性，精力全放在表达方式上，会看不见许多更重要的东西。

AI 有望让字幕成为过去

2022-01-20 14:59

观看外国影视剧通常会用到字幕，一则可能是没有当地配音版本，或者配音版本没有达到原版的满意程度。要让原版的演员说不同地方的语言是不可能的事情。如今 AI 技术的进步有望让不可能变成现实：AI 通过训练能使用原版语音合成出逼真的新语音。新语音不再是另一个人的声音，而是演员本人比如汤姆克鲁斯说着另一种语言。这一技术也 引发了音频深度伪造的担忧。AI 公司 Veritone 透露了它开发的名为 MARVEL.ai 的产品，允许内容制作者生成超现实的合成声音。

#math #plt 公开课. 是仿造数学语言 https://github.com/DSLsofMath/DSLsofMath
Introduction: Haskell, complex numbers, syntax, semantics, evaluation, approximation
Basic concepts of analysis: sequences, limits, convergence, ...
Types and mathematics: logic, quantifiers, proofs and programs, Curry–Howard, ...
Type classes, derivatives, differentiation, calculational proofs
Domain-Specific Languages and algebraic structures, algebras, homomorphisms
Polynomials, series, power series
Power series and differential equations, exp, sin, log, Taylor series, ...
Linear algebra: vectors, matrices, functions, bases, dynamical systems as matrices and graphs
Laplace transform: exp, powers series cont., solving PDEs with Laplace

#typescript #TT 科普 TypeScript Type-Level Programming - lsdsjy的文章 - 知乎
https://zhuanlan.zhihu.com/p/54182787

TS是支持静态类型的JS。有 number,string 等值，也有常量作 literal type: number, .. "div" "body"..
<K extends keyof ElementMap> :R=Map[K] 是入门级子集定义吧！TS里{a:1,b:""} 的类型都是这种表。此外 {[K in keyof T]: } 可作转化
这个表里[num,str] 是 num|str 的意思，因此若有 P={a:num,b:str} 则 P[keyof P] ，就是并集类型。类同{}类型， {[K in KS]: }[KS] 给并集list 作转化

let v: (() => void) extends Function

的类型是true(lit type). 以下 is=extends
type T={a:num,b:str} //v:{a:Num|never} ，never=kotlin.Nothing |的不动(0值)点
let v:{[K in keyof T]: T[K] is number? T[K] : never }[keyof T] //收集并转换

子类型中 Int is Num, Num is Num 。is是 <= (never不大与任何类型)的意思，如何实现(=)呢？

type Equal<T, U> = T is U ? (U is T ? true : false) : false //TS类型上无&& || !
let v: Equal<Func, Function>  // v: true //最后一遍:这是编译期可知

TS只支持 recursive mapped types，“递归函数”只能返回 dict。设想 T={xx: T|Promise<U>} ；把T内所有Promise.resolve 的函数类型是啥？
type Unwrapped<T> = { [K in keyof T]: T is Promise<infer U> ? U : Unwrapped<T> }
type Unwrap<T> = (wrapped: T) => Unwrapped<T>

这里也以infer语法来引入新的 typevar <U> ，算是某种意义上的“模式匹配”。在Haskl 对 ADT 的值作模式匹配；在这儿，我们对有着“代数类型 类型”的TS类型作模式匹配。
ADT 有普通的函数状 data constructor；Type 也有 type constructor，比如 Promise就是 T->Promise<T>的“类型函数”。它是 lit,list,dict 外第三种组合方法
type:
Nat<N> = Zero | Succ<N>
Zero = void; type Succ<N> = { pred: N } //0, +1
_1 = Succ<Zero>
_2 = Succ<_1>

IsNat<T> = T is Nat<infer N> ? true : false
q1 = IsNat<_2> // true
q2 = IsNat<number> // false
IsNatIsNat = IsNat<IsNat> //err: IsNat require param

然后是:
一开始的时候，我把 Coq induction 和数学归纳法搞混了。要用数学归纳法证明一个命题 P，你需要先证明一个基础步骤 P(0)，然后在 P(n) 成立的情况下证明一个递推步骤 P(n+1)。但是在 induction 里面没有“基础步骤”和“递推步骤”之分，甚至 induction 产生的小目标的数量都不一定等于2。之后，我发现你可以把 induction 理解成数学归纳法的一种扩展。数学归纳法是作用在自然数上面的，而自然数是一种递归定义的归纳类型：

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Lemma len_repeat:  --n(s rep k)=k*n(s)
  forall s n,
    String.length (repeat s n) = n * String.length s.

intros s n. induction n
(s rep 0)=0*n(s)—无归纳假设, 下递归定义,有.
(s rep N+1)=(N+1)*n(s)

Lemma len_app_plus: --n(s+s1)=n(s)+n(s1)
  forall s1 s2,
    String.length (s1 ++ s2) = String.length s1 + String.length s2.

要证明 len_repeat，我们就要对 n 进行归纳，因为 repeat 是定义在 n 上的一个递归
证明 len_app_plus，就对 s1 进行归纳，因为 String.length 在每次迭代中会消耗字符串的第一个字符。当你对 s1 进行归纳的时候，第二个情况会是 s1 = String char s，这就对应了 String.length 的定义


作者：陈乐群
链接：https://zhuanlan.zhihu.com/p/54164515 能够看出来写得很好，还带FAQ..可对外道入门逻辑式还不够唉

#rust #PLT 自由程续-阴阳谜题 手动脱call/cc解
Rust 阴阳谜题，及纯基于代码的分析与化简 - 知乎用户FGAvTw的文章 - 知乎
https://zhuanlan.zhihu.com/p/52249705
#Python 5行yield解 https://zhuanlan.zhihu.com/p/43207643

如何制造SCP018 - 圆角骑士魔理沙的文章 - 知乎 — 函数式尾调用优化
https://zhuanlan.zhihu.com/p/43163820
形式验证、依赖类型与动态类型 - 老废物千里冰封的文章 - 知乎 讲了 Nullable,静态长Vec,运行时报错的type兼容
https://zhuanlan.zhihu.com/p/50792280

#math 证明 a.rev().rev()=a 。不敢保证准确 但一定不会烧脑，实际上我也没见冰封外的人讲过 #haskell
首先， rev (r:xs)=(rev xs)++[r] -- rev[1,2] =r[2]++[1]=r[]++[2]++[1]
((x:xs)++r)=x:(xs++r) --[2]++[1]=[]++[2]++(r=[1])=[2,1] --链表的Nil即[]替换为r
([]++r)=r
是执行原理。 可以先得 x:(rev a)=a+x ，如 b=rev a, 证明 rev b=a 时已知b就是(rev a)，可把 x:b=a+x 对应，毕竟 rev 其实也有一种 fold (:) [] 的写法，能做到两边相等

s => // x s. rewrite rev_cons. case: (rev s) => [|x1 s1]<- ==

至于 x:reva=a+r ，靠 rev(r:xs)=revxs+r 直接是得不出的?，但翻过来 rev(revxs+r) 其实就是原来的 r:xs 首先在 xs+r 位置，然后还原过来 revxs+r=rev(r:xs)

rev_cons (x1 x2 : T) s : (x1::rcons s) x2 = rcons (x1 :: s) x2
rewrite cons_rcons rev_rcons 

讲得迷糊是因为我也很迷糊，但，幸好在网上找到了 revrevid.v ，不然就绝对不正确了。因此完整证明(反正也看不懂. 上面链接也讲了rewrite是换个参数来证)：

Lemma cons_rcons T (x1 x2 : T) s : x1 :: rcons s x2 = rcons (x1 :: s) x2.
Proof. done. Qed.

Theorem rev_rev_id T (s : seq T) : rev (rev s) = s.
Proof.
  elim: s => // x s. rewrite rev_cons. case: (rev s) => [|x1 s1] <- //=.
  rewrite cons_rcons rev_rcons => //=.
Qed.

冰封的“科普文”和上楼类型编码没有区别但对验证更细，之前好像还有构造 &^ 性质，然后可以组织证交换律的，但是集合论参数语法都没说清楚，好像是匹配几个变量换个位置；现在冰封删文了，我也没兴趣管这些。想必喜欢函数式的人也受不了这种逻辑学吧，真的毫无逻辑可循，毕竟等式变形已经完成了， n(s+s1)=ns+ns1 这种特质却不能 forall? 想必对我们这些俗人还是太高深，Coq Idris 等形式验证，它用的集合论我也不知道是咋回事，比<图解范畴论>里高次数范畴还迷糊，只能放弃喽

Nginx 的核心开发者、公司创始人 Igor Sysolev 决定退出开发。
https://www.nginx.com/blog/do-svidaniya-igor-thank-you-for-nginx/

Igor 坚持在 Nginx 上工作了 20 年，其中有近 10 年都是一个人在开发。他的成果已经成为了现代互联网发展的基石。

#algorithm UnionFind、三角分形(精简版)

如果要实现 Set 你会怎么做？每次 add(x) 时去重遍历 uniq() 吗?
现在按数组Array(N).fill(0).map((x,i)=>i) 实现 Set<Int> 。每位与一个索引关联，初始是和自己
当加一对 a-b ，把它们的位置赋上彼此，就能知道在不在同集合内——不行，如果还有a-b-c 咋赋值？
答案是 a->b 关联 b->c 再关联，因此 find() 变成链表遍历后最终同一。然后 add(a,c) 先找这个"b"，把它->c
最终这个 Map<Int,Parent=Int> 会变成树状数组，只是不被遍历。UF集也有a-b小size侧优先-> 权重,和max()时顺便合并快查法

UF=(N,up=Array(N).fill(0).map((x,i)=>i) )=>(a,b,eq=true)=>{
let max=i=>{for(;i!= (i=up[i]);); return i}, iA=max(a),iB=max(b)
if(eq&&iA!=iB)up[iA]=iB; return eq||iA==iB //不上obj,写不好..
}
let o=UF(3); o(0,1);o(1,2)
o(0,2, false)==true

//给不懂的同学：N是(Map状数组)项个数,up是“父数字” ，eq代表不仅查询还建立a-b 连接关系。 UF算法与up[] 是1:1 ，所以随便起了个o=UF() 数据来功能test
这个相当于List<Set<Int>>
另外 UF,BFS 都是在节点图上判断两点是否联通，如果需要路径则用 DFS ，如从节点 2 的[+3,*3]边怎么走到 "9":
dfs=(link,flink,out,chk=(e,e1)=>{let k,k1;if(e==e1)return[]; if(!out(e)) for(k of link){k1=chk/*找!*/(flink(e,k),e1); if(k1)return k1.concat(k) } })=>chk
ten=dfs(["+3","*3"], (a,k)=>eval(a+k), a=>a>10)


ten(2,9)

->+3*3 (chk完还应reverse下.)
//当然比较hack,如果是专门讲我就会用正经let函数
然后最短路径可以用Dij狄图算法(也可优化权重边)，也有A*啥的寻路法。 pip,apt 等依赖工具就是简单BFS可达搜索搞定；我不搞OI懂的不多
#inm 比较喜欢的数字论证生成器可以是这样 11 = 11*-4+51+4

我找了两个与算法解读比 较差的博文:
https://blog.csdn.net/dm_vincent/article/details/7655764
https://www.cnblogs.com/SeaSky0606/p/4752941.html
还有正经算法解读: https://zhuanlan.zhihu.com/p/63123489
大家可以比比它们的信息量。
—
你要咋画 Xecades大佬的三角分形 (三角内接倒三角，其三边与我顶点继续如此)？
本来是要在中线拿3点(shift遍重组,或者手写配对)和带深度递归的，可看起来只需要
#js #code
document.write`<canvas id=eg>`
{
let sq=Math.sqrt, dim=(e,[w,h])=>{e.width=w,e.height=h}
y = Math.min(innerHeight, innerWidth * sq(3) / 2)
g = eg.getContext("2d");
g.fillStyle = "blue";

let P=[[0,y],[y / sq(3),0], [2*y / sq(3),y]],p=[...P[0]] //左顶右
dim(eg,P[2]);dim(eg.style,["100%","100%"])

setInterval(() => {
let j=0,i = Math.random() * 3 >>0
for(;j<2;j++) p[j]=(p[j]+P[i][j])/2 //随机选方向游走
g.fillRect(...p,1,1)
})
}
//g;画布,dim:宽高wh ,sq:三角(点->点)xy距离的计算, j:仿造向量的计算同时应用于xy

就够了。GLSL 里画三角

#define v1 float
v1 PI=3.14;
v1 ply(int N,vec2 p){
//多边形. 三角[0,y],[y / sq(3),0], [2*y / sq(3),y] 都没了..
v1 d, TURN=2.*PI;
// space to -1~1.
p = p *2.-1.;

// Angle and radius from the current pixel
v1 r = TURN/float(N);
v1 l = atan(p.x,p.y)+PI;
d = cos(floor(.5+l/r)*r -l)* length(p);//distance-shape

return 1.0-step(.4,d);//也可smoothstep(a,b,v)模糊锐边
}
void mainImage(out vec4 bg, vec2 P){P/=iResolution.xy;
P.x *= iResolution.x/iResolution.y;
bg=vec4(0,0, ply(3,P), 1.);//左中 蓝三角
}

// 这个我没法注释，因为SL图形和数学几何关系大。有的时候看不懂也不是因为故弄玄虚，而是那个领域本身难懂。比如我define v1=float 和rld仨变量变 degRee(不用a因为编程有数组要命名),length,distance 后对第三块代码难度影响不大，因为核心不是浮点有几个字

(不过要画三角分形就会难许多了,而且Xe的游走三角是靠边点累积来的，SL不支持累积..)
可以看出，物理的矢量是非常高明的代码复用，少做了很多结构性的事，却照样实现图形效果，而且更可调参——例如靠点集计算就做不到 ply() 边缘模糊的效果

#haha #inm #bilibili 搜到了几个野兽先辈的自动化工具 😂 (好啊！来啊！ 啊！？啊啊啊啊啊！！！)
https://lab.magiconch.com/homo/ 数字论证生成(map:Int,Str 数据集里选最大不大 拼接)
https://wyusagi.github.io/Proof_Yajuu/ 自动迫害机(文字模板)
https://www.cnblogs.com/lcyfrog/p/13181450.html #oi C++ 数字论证cli