#dev #tech #English

boot 靴子 引导
stub 存根 占位
review 复习 评审
render 提出 渲染
map 地图 映射
console 安慰 控制台
frame 边框 帧
image 图像 镜像
bus 公交车 总线
access 入口 访问
log 伐木 日志
dump 倾倒 转储
cache 隐藏住所 缓存
port 港口 端口
performance 演出 性能— adolli🍮7️⃣🎏咕嚕靈波（●´∀｀）ノ♡ (@adolli) January 3, 2019

#media #drawing 练习（第二张其实是有第一个版本的，不过画的太难看了（非常之崩），不发

为了画好这第二张，我是足足画了几百只眼睛... 又改了 50 多次... 眼睛，最后手还是有点不对称（ 🤪

另外的一种 BW（也可以说是 blacK/White） 着色方式（不过这里是 4B 铅笔（准确的说是考试涂卡笔

最终没能完成的 #Agda 证明... #Proof 我还是暂时不理解归纳证明

是这道证明题

因为我当时没有 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