Relens to Lens 之前也写过一篇lens的文章，学了新知识之后，现在看起来觉得不满意，于是打算重新再写一篇。 脚趾头：First Lens to Lenses Lens的设计十分的精妙，是数学指导编程的一个非常典型的案例。 Lens要解决的问题 在Haskell中，只提供了模式匹配的语法来操作数据，操作深层的是一个非常麻烦的事情。比如我们要操作以下数据： data Point = Point { positionX :: Double , positionY :: Double } deriving (Show, Eq) data Segment = Segment { segmentStart :: Point , segmentEnd :: Point } deriving (Show, Eq) p1 = Point 1 2 p2 = Point 3 4 l1 = Segment p1 p2 我们要修改l1的第二个端点的横坐标： l1 {segmentEnd = (segmentEnd l1) {positionX = 10}} -- 如果没有部分修改record的语法，这样的工作会更麻烦，只能用模式匹配一项项填 如果数据结构更加复杂的时候，代码就会变得更冗长。但如果用lens，刚刚的表达式就可以重写为：...

前言 Haskell中有一个很强大的库，叫做Lens。 在Haskell中，只提供了「模式匹配」的语法来访问/修改数据结构。于是处理深层的数据就成为了老大难的问题。 比如在这样的数据结构里： data Point = Point { positionX :: Double , positionY :: Double } deriving (Show, Eq) data Segment = Segment { segmentStart :: Point , segmentEnd :: Point } deriving (Show, Eq) p1 = Point 1 2 p2 = Point 3 4 l1 = Segment p1 p2 我们要修改l1的第二个端点的横坐标： l1 {segmentEnd = (segmentEnd l1) {positionX = 10}} 如果数据结构更加复杂的时候，代码就会变得更冗长。 这时候Lens库就出场了,刚刚那段代码等价于： l1 & endLens . xLens .~ 10 其中endLens ....

因为我太菜了，虽然其实第一部分都做出来了，但也就想好第一题比较理想的 tacit 解 {(⌽⍣(⍺<0))(⍺↑⍵)(⍺↓⍵)} 显然的解。 APLcart 给了个 tacit idiom, 注意用到了 18.0 新出的 Over operator，在 17.1 只能用 $\{\alpha\; \omega\}$ Is(↑,⍥⊂↓)Y ⍝ ←→ Is (↑{⍺ ⍵}↓) Y ←→ Is {(⍺↑⍵)(⍺↓⍵)} Y 但不能直接用上去，因为在 $\alpha$ 是负数的时，结果和要求是反向的 ¯3 (↑,⍥⊂↓) 'FooBar' ┌───┬───┐ │Bar│Foo│ └───┴───┘ 这就是为啥我用了 reverse，并用 power operator 控制，对应 $\alpha <0, \alpha >0$ 两个 case。但用了 power operator 就很难转成 tacit form 了。那么上面的答案要如何写成 tacit 呢。 可以換个角度，在负数时转成正数。假设有 f 做了这个工作，那么 {(a↑⍵)((a←⍺ f ⍵)↓⍵)} ⍝ ←→ {(⍺ f ⍵)(↑,⍥⊂↓)⍵} ←→ f(↑,⍥⊂↓)⊢ 那么 f 是什么呢，是这个么？...

本人有个小小的习惯，就是在学习一门语言的开始，为了熟悉这门语言的基础设施，我都会写一个最最简单的parserc（当然那些9012年都没有支持泛型的语言，就不写了）。 这次就试着用Rust来写一个。 从Iterator中来 用过Rust的Iterator的人，一定会觉得这用起来十分的愉悦，这说明Iterator设计得很不错。而parserc的使用方式其实和使用Rust的Iterator的方式十分相似的——先将小的组合子构造成大的组合子，然后再使用，parserc是.parse()，Iterator是.next()。 所以借鉴一下Iterator的思路，Rust版parserc也试着由这几部分构成： parser的trait 一些adapter 自定义一些combinator 组合出来的一些combinator 用起来大概是这样： // a+(b|c) fn aaab_c() -> impl Parser<Target=()> { char('a').some() .and(char('b').or(char('c'))) .map(|_| ()) } fn main() { let mut src = ParseState::new("aaab"); let res = aaab_c().parse(&mut src); assert_eq!(res, Some(())); } Parser trait 先定义parser的一般行为parse，“照搬”Iterator的结构。 #[derive(Clone, Debug)] pub struct ParseState<'a> { src: Chars<'a>, pub col: usize, pub row: usize, } pub trait Parser { type Target; fn parse<'a>(&self, state: &mut ParseState<'a>) -> Option<Self::Target>; } 在Haskell中，最简单的parse function的类型是String -> Maybe (a, String)：吞进去一个String，得到解析结果a，还有未匹配的字符串，或者没有结果，也就是匹配失败。这里也采用了类似的结构，有所不同的是，因为Rust是有mut的，可以直接改变状态，于是可以去掉用返回值表示的状态，改为可变引用；然后，parse的状态加上了行和列，为了方便，用字符迭代器表示要解析的字符串。...

MetaPRL 的修理告一段落了。在这篇文章里我来介紹一下它用起來大概是什么感觉的。 MetaPRL 不是像 Agda/Lean 那样直接写 proof script 然后 type check，也不是 HOL 那样完全在 repl 里做 interactive 操作，而是一半一半：proposition 先全写在文件里，编译成 rewrite abstract machine 后，link 到 Toplevel 程序，再用 repl 来进行 interactive proof，或者查阅，也可以 print 到 html 或 latex。 MetaPRL 中 proposition, tactic, inference rule 之间没有分別。primitive inference rule 就是不需要证明的 tactic，proposition 就是具有证明的 inference rule。因为用的是类似 sequent calculus 的 language，所以能定义表现力强于其它 proof assistant 里用 lemma 或 tactic 的 metatheorem。这一点原版的 NuPRL 也只是能自定义 inference rule 而不能给出 conservative extension 的证明。比如 显然易见，对形式为 $\Gamma, x:\mathbb{B}, \Delta[x] \vdash C[x]$ 的 goal 应用这个 tactic，就会生成 $\Gamma, \Delta[True] \vdash C[True]$ 和 $\Gamma, \Delta[False] \vdash C[False]$ 两个 goal。在 Agda 里这要用 dependent pattern match, 在 HOL 要用 primitive inference rule compose tactic，而在 MetaPRL 里这只是个能证明的 theorem，而且做为 tactic 没有 HOL tactic 必須要用 primitive inference rule 的 overhead。...

这一篇开头讲一点 constructive real analysis。 Intuitionistic mathematics 中，实数用一个不断提高近似精度的无穷序列(Cauchy Sequence) 定义。 即 $\mathbb{R} =_{\it def} \{q:\mathbb{N}^+\rightarrow \mathbb{Q}\;|\; \forall n,m:\mathbb{N}^+ .|q_n-q_m|\leq n^{-1}+m^{-1} \}$ 这样的无穷的序列就是 free choice sequence 中的一种，表现出来是个 $\mathbb{N}^+ \rightarrow \alpha$ 的 function type。在这里 $\alpha \simeq \mathbb{N}$ ，即和自然数一一对应，众所周知地，有理数滿足这一性质。1 显然地，引入 choice sequence 的概念时，choice sequence 可以分成三种。 一种为 lawlike，即可以用某个 algorithm 表示的。 第二种为 lawless，是完全无序的。 第三种是由前两种 choice sequence 混合得到的，是为 mix。 注意即使是 lawless sequence，也符合 function 的性质，即 $\forall a. f(a) = f(a)$ ，也就是已经生成的数是不会变更了。 尽管 choice sequence 是无限的，但明显地，任何有限的 sequence 同时是无限个 choice sequence 的初始部分。...

本次要用 CTT 来写 Leftpad1，以说明即使不能实际运行 NuPRL 仍是个很好的 programming logic？(因为如下证明我是直接写的，没在 NuPRL 里跑) Takes a padding character, a string, and a total length, returns the string padded to that length with that character. If length is less than the length of the string, does nothing. 问題到手，首先定义的是 string 的 axioms $$\forall x: \mathbb{N}. Str(x) \in Type\\C \in Type\\ \forall x: \mathbb{N}, y: \mathbb{N}_x, a : Str(x). a\ !!\ y \in C\\ \forall x: \mathbb{N}, a : Str(x)....

首先这里不是用打表这种对于提高打牌技术没有实际意义的 baka 方法。 特殊型(国士，七对型)听牌先按下，字牌因为没有什么难度请读者自行作为课后作業。这里先只考慮由 1~9 的万，条，筒组成的牌形。 众所周知标准和牌形是由一对将＋四面子组成的。听牌则有单骑，两面，嵌张。对于如下简单的情形的只要是稍会麻将的就能不难看出是听 2 5 筒的(请忽略最右的白牌)。 那么来分析一下人类玩家在看到这一手牌时做了什么样的思考，然后如何把这样的思考转化为算法。 表示法 首先，根據花色拆为 (12366 索)， (345566 万)， (24 索) 三组。 我们要一个在 APL 中表示手牌的方法。假设己经有做了分组，那么如上圖的手牌就可以用一个 nested array 表示 ⊢hand←(1 2 3 6 6)(3 4 5 5 6 7)(3 4) ┌─────────┬───────────┬───┐ │1 2 3 6 6│3 4 5 5 6 7│3 4│ └─────────┴───────────┴───┘ 然而这样的表示对于处理没有什么助益，所以要把每一组编码成一个长度为9的array，对应每种花色 1~9 的牌每张出现的数量。 enc←{⍺←9⊣⎕IO←1 ⋄ ((⊢∘≢⌸⍵)@(∪⍵))⍺⍴0} enc 1 2 3 6 6 1 1 1 0 0 2 0 0 0 enc¨hand ┌─────────────────┬─────────────────┬─────────────────┐ │1 1 1 0 0 2 0 0 0│0 0 1 1 2 1 1 0 0│0 0 1 1 0 0 0 0 0│ └─────────────────┴─────────────────┴─────────────────┘ 己完成的面子 在上面所示的听牌中，人类可以一眼看出三组中 345 567 万是己完成的面子，那这「一眼」中发生了什么？...

函数式的动态规划 动态规划是一类很常用的算法，在C/C++/Java中一般使用于数组进行记忆化。而函数式编程语言一般无法方便地操作数组这些依赖副作用的数据结构，函数式的记忆化便要另寻他法。 本文就是一个简单的笔记，用一些代码片段展示我所知的函数式动态规划的技巧。 （2020/5/17，时隔五个月后的更新，新增Memocombinators） Course-of-Values Recursion Course-of-Values Recursion是我认为最直观的一种技巧，就是将遍历过的结果当作返回值的一部分保留下来，在递归的时候可以取得运算过的值。 对于递归函数f，定义一个辅助的函数bar $\begin{align} \overline{f}(n) = [f(n), f(n-1),...,f(0)] \end{align}$ 则原递归函数f可以用bar表示出来： $head(\overline{f}(n))$ 斐波那契数列： fibBar :: Int -> [Int] fibBar 0 = [0] fibBar 1 = 1:fibBar 0 fibBar n = let course = fibBar (n-1) in -- [fib(n-1)..fib(0)] let p = course !! 0 in -- fib(n-1) let pp = course !! 1 in -- fib(n-2) p + pp : course -- >>> fibBar 10 -- [55,34,21,13,8,5,3,2,1,1,0] -- Binary Partitions：...

上一篇 LdBeth：NuPRL 中的证明 III–我不做metavariable啦 Part I: Atom type 可能有之前用过 Agda 的人会在开始用 NuPRL 以后觉得，没有 inductive type definition，只有 product 和 disjoint union 但是没有区分 data constructor 的类型，好不习慣啊。 其实这个也不是什么大问题，data constructor 可以用 NuPRL 的 Atom 类型来模拟。 Atom 頋名思义就和 lisp 里的 symbol 类似，可以比较相等。 所以一个 inductive data type definition 的 tree data Tree a = Node (Tree a) (Tree a) | Leaf a 可以表示成个 dependent pair ${\bf DEF\ }Tree(a) = rec(T. \Sigma x : {\tt Atom}. {\tt if}\ x =_A {\tt"...