是这道证明题

因为我当时没有 Agda 环境而且没看过 Agda 的语法参考，不敢随便修改这些东西，不要以为我只是抄了点代码然后啥都不理解

我好歹还抄了两节课...
我好歹对于 reverse 这种简单递归程序还分析了一会...

不准喷！不准喷！平时你们写那些 Android 应用.... Java 的 Web 后端程序我后来有时间了自然会学...

为了让你们不会喷我只会画个画没前途，特地发我在信息工程方面还会的一些东西...

我真的不是样样通样样松（虽然还并没有样样通）
我真的不是只会画个画，或者只会写个简单的程序或者算法什么的... 真的不是... 别喷

btw. 我这里说的 reverse 是 Haskell 里那种简单的 List reverse

使用 #Haskell 定义如下

reverse' :: [a] -> [a]
reverse' [] = []
reverse' (x : xs) = reverse' xs ++ [x]

当然也可以使用 fold 这种非常具有普适性的 operator 来写，那就是说

foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
reverse'' :: [a] -> [a]
reverse'' = foldr (\x xs -> xs ++ [x]) []

题外话，我以为 infix operator (++) 的类型签名是

(++) :: [a] -> a -> [a]

但其实是

(++) :: [a] -> [a] -> [a]

结果出了很奇怪的类型问题，Couldn't match expected type ‘[a]’ with actual type ‘a’
而我作为 Haskell 初学者居然没有看懂是什么意思，即使人家连是哪里的问题都说出来了（In the second argument of ‘(++)’, namely ‘x’）
我真蠢...

main = do
print $ reverse' [1, 2, 3]
print $ reverse'' [1, 2, 3]

#Haha #coolapk

歪果仁居然用这种 Sticker.....

文化输出（

哪天外国人也学会两开花了（x

#sysadmin #life duangsuse 回来了！这次我更新了 Fedora 到 F29(Twenty Nine)

说个好笑的，Dnf（Dandified Yum，Fedora 28 的软件包管理器）离线更新的时候那个下载日志还是什么居然积累到了 18G，把我的 SSD 塞炸了... hhhhh #Haha

#yearPassed 新年新系统 release version！（Fedora 28 :> Fedora 29）

#archive #life #consumer 我买了一个 499 的 Wacom 数位板（指 18 年淘宝上最火的那个）（别喷我用淘宝，我爸的）

顺便又买了新墨盒... 又可以打印新 papper 们看了（指 HP 810（好吧，反正就是适配 HP DeskJet 1112 系列的

#School 这周马上就要放寒假了（还有一个月） 🤔

duangsuse 的安排嘛... 其他的都好了，本来每周就是讲东西为主，然后本周买了别的东西，画了几张画，最后书什么的基本没看。嗯嗯。

这周就是讲点东西，发点照片，没了。

顺便说一下，推荐有打印机又看过书的大家可以没事带几张 papper （比如之前那个代数程序逻辑的 fold.pdf，我在 USTC 中科大学生的分享里淘到的，当然论文基本都是公开的你们可以随便找个大学比如 Illinois 的 CS 系看...）到例如公交车的地方看看，因为我觉得吧，公交车之类的地方可能思维都比较开放一些，学习起来比较有效果，可惜就是很慢就是了

至于我上面提到的 papper A tutorial on the universality and expressiveness of fold 可以在 这里（Nottingham in UK 大学）下载 #papper #FP #CS
个人觉得... 虽然有些不常见的词，但是有一定函数式编程和程序分析变换、形式化证明基础的人虽然可能看很久但收获不错。

见好就收。

#GitHub #dev

萨摩终于挤进 githubrank 了，然后上下一翻发现了好多熟悉的面孔（🌚