btw. 真是高产啊，才一周不见就更了两篇文章

duangsuse 自己对程序静态分析检查还不是很了解，when 表达式的语法上面各种糖都还好说（毕竟手写 Recursive Descent 我还是熟悉的）
啥分支覆盖问题我也想过，不过啥都不懂就是了，打算如果以后就这种水平去实现的话，尽可能多做一点（或许是启发式的...（这里启发式和机器学习无关，意思是「假设各种情况做检查」））检查，不要求绝对正确，保证体积和解释器本身健壮即可，类型检查器重要性优先于类型推导器

〖对应用层开发者（e.g. Android 开发工程师、PHP 或者管他什么没有达到完全抛弃任何框架的程度能力者，尤其是语言特性贫瘠或非底层语言 Lua、ES5、Java、Groovy、Python 程序员）来说〗
像这种写 Agda、Idris、ML 等「具有证明程序正确性的程度能力」语言水平的人，最好还是不要在他们面前炫耀自己写了多少前端应用什么的，说实话，等你以后（或许）有了更高的视角，你会发现你死记硬背的那些 CSS 属性，学的反编译器使用、Bash 编程、GNU/Linux 系统配置、Git/Gradle/CMake 等「最佳实践」等等根本不值得一提，不是一个抽象复杂层次上的东西

不过至少是冰封来看，他没有那种高高在上的架子，比较平易近人（虽然最喜欢研究的理论不平易近人，笑），但如果自己没有足够的水平，有些圈子不必强融就是了（反正以后赶上了可以再进嘛）

优化版的盒子堆（Haskell）（因为 InScript 还没有形式化的被定义出来，也暂时没有人实现它，我想看到自己的程序实打实在电子计算机而不是我的脑子里运行起来 XD）： 😸

其实这玩意是我从《算法图解》（内容简单像「故事书」，其实教的东西大学里都要上，体现了知识系统相同表达教学方式简单一点的确可以让学习更高效）里弄的一个伪代码例子

可出对应 OI 题，不过就是那种小学生都会写的那种（迫真），好吧，我不知道现在 OI 生们都是啥水平，有没有 OI 生给我科普一下？排序算法理解否？各种图各种树算法会否？动态规划 diff 会写否？线性规划会吗？网络流？

duangsuse 的算法水平依然需要严重学习（XD #algorithm #cs #china #tech #haskell #functional

（在网上找不到单独的中文 Haskell 社区，看来中国特色的（伪工业系）工程师们都喊着口号其实懒得动 FP（函数式编程），第一次作为小众群体感到由衷的自豪，哈哈（迫真））

（好吧，其实有一个，但包装得实在是不咋样（还不如 LetITFly BBS，甚至 LWL12 的个人博客），而且连论坛都是 GitHub issue 讨论版并且没有自己的服务，没啥实用价值，233）

可惜，一个星期只放假半天，所以我只能做这些实际上没啥卵用的玩意，哪怕写个 Sexp 解释器给自己玩玩或者写个 AXML 二进制流解析器都是好的，甚至写点 Gradle Groovy DSL 都行啊... 写点 Kotlin 的 Android 应用... Android 核心模型哪几个来着... 好像是 Intents... Boardcast Receivers, Activities, Services, Notificatoins...

（by the way, 刚才写的时候突然停电了，还好 Telegram 支持跨设备 draft 缓存，不会丢失写了半天的辣鸡玩意😋）

（再讲个很好笑的事情先😄）
Learn You a Haskell for Great Good(EN) 有个中文翻译，不过是我们台湾的同志们搞出来的，人家顺便弄了个简体的翻译 🙃

我之前把 Haskell 当 Ruby 用，我写过这种代码并且臆想它能正常工作的样子（你们知道，Haskell 里不兴 Helloworld 这种幼儿园小朋友写的代码）（吐嘈：你知道还坚持要写这种只比 HelloWorld 复杂二分之一的代码...）：

putStrLn getLine

原因很简单：我在 GHCi 里各使用这两个函数都能正常工作。然后我想说的其实是类似这样（之前嘛，我是完全不懂的，包括我也无法理解函数类型符号 Integer -> Integer 啥意思（并且，冰封博文上讲了我也看不懂，233333333））

do ln <- getLine; putStrLn ln

... 其实也不是理论上有问题，我之前一厢情愿的认为我是把一个 () -> IO String （一个无参闭包，或者说匿名函数，一般这俩都等价的）传给了 putStrLn :: String -> IO ()
（当然，据说 Haskell 里无参函数和变量是等价的，就是惰性求值变量？或者不是，是 call-by-need 变量？如果是纯函数的话，二者都差不多吧...）
所以现在我这么修改之前那个幼稚的例子（是的，我又 TM 去看了点 Haskell tourial） putStrLn $ getLine

其实是 IO String 不是 String 的问题，用 getLine >>= putStrLn 即可

getLine 是 IO String （没错，这厮不是函数...）
putStrLn 是 String -> IO () （type String = [Char]）
(>>=) 是 IO a -> (a -> IO b) -> IO b，绝配，稳如老狗（确信）。

IO String -> (String -> IO ()) -> IO ()

然后代码

module Main where

data Item = Item { name :: String } deriving (Eq, Show)
data Box a = Box { name :: String, items :: [a] } deriving (Show)
{- 打住，我不会写这种... 老出问题证明我 Haskell 还太菜 -}

data Item = Box (String, [Item]) | Atom String deriving Show
findItem :: Item -> String -> [String]
findItem b o v = []
| (Box n is) o v = findItem is o (n : v)
| (Atom n) o v = if o == n then print v

Haskell 弄分支函数老说我语法错误还不告诉我为啥，弄得我没法修... 只好自己又弄一个手动分支来的

module BoxDfs where

data Item = Box (String, [Item]) | Atom String
  deriving (Eq, Show) 

findItem :: String -> [String] -> [Item] -> [String]

findItem m v [] = []

findItem m v ((Box (n, xs)):bs) = findItem m (n:v) xs
findItem m v ((Atom n):bs) = if n == m then v else []

{-
findItem m v (b:bs) =
  case b of   
    Box (n, xs) -> findItem m (n : v) xs
    Atom n      -> if n == m then v else []
-}

还没测试，等下发文件。待会会弄（写、找）点 Haskell 和 FP 系教程发来，欢迎喜欢的来看

直接写出来我们再分析一下算了：

分析结果：如果找到元素的路径不止一个，可能会找不到元素，原因自推

冰封哥给回复了，说是我对 guard 语法（就是 InScript 里的 when 分支）的理解有问题，不过他没说是啥问题，InScript 设计时就打算以语法自然为上，也顾不上语法的统一性和可预测性了

https://www.tuicool.com/articles/Vzyy6ju

https://ice1000.org/gist/fp-dfs/

接下来我们来用 InScript 重写这个 Haskell 的 dfs 哈？

https://agda.readthedocs.io/en/latest/language/with-abstraction.html
#cs #pl #agda #plt Agda with abstraction
类似 Haskell 的 case of 但又不是，我也不知道为啥，别人总结的

https://raw.githubusercontent.com/mbinary/USTC-CS-Courses-Resource/master/%E8%AE%A1%E7%AE%97%E6%9C%BA%E4%B8%8E%E4%BF%A1%E6%81%AF%E7%B1%BB/%E7%A8%8B%E5%BA%8F%E8%AE%BE%E8%AE%A1%E8%AF%AD%E8%A8%80%E5%9F%BA%E7%A1%80(%E8%8B%B1)/IntroToHaskell.hs

#haskell #cs #learn #tutorial Haskell 入门好码

https://www.tuicool.com/articles/Vzyy6ju #Haskell #tutorial

#haskell https://www.haskell.org/hugs/pages/downloading.htm #share #software

https://segmentfault.com/a/1190000005137600

这个一 iOS 开发者的入门笔记，个人感觉参考价值不如第一个代码示例

https://wiki.haskell.org/Pattern_guard #haskell #pl #cs Pattern guards in Haskell

后来回复是 你这个语法好垃圾啊，不喜欢 （安心感） >>
去学习些好点的语言啊。别整天抱着拖人类后腿的语言看了。

顺推 关于依赖类型编程语言和完全函数的检查的一些想法

（狂）听到了吗？你们 JawaScript、Pascal、Basic、Perl、Ada、Smalltalk 等就是拖人类后腿的语言（Ada 这种知名老牌语言都拿出来鞭尸我有点过意不去...）

btw. 这只是 InScript 一小部分语法和定义风格了，InScript 被设计为更多情况下作为 Imperative 的语言，不是这种定义式的山寨 Haskell

InScript 里 A[] 实现的不是 Iterable （严格来说都是，但这里为了好看包容一下吧）不是 Collection 不是 Sequence 不是 RandomAccessable 也不是 Set 也不是 Queue 也不是 Stack
但它绝对实现了 interface java.util.List<E>



def <A : Comparable<in A>> List<A>.binarySearch(A target)
  var Int bound_bot = 0, bound_top = lastIndex
  while bound_bot <=> bound_top gtZero
    let index = bound_bot mid bound_top, guess = self[index] in
      when guess
        is target -> return index
        > target -> bound_top = bound_bot.mid(bound_top) sub1
        < target -> bound_bot = bound_top.mid(bound_bot) add1

8 行。上面的那个是六行

#cs #pl #plt #recommended 节选自 origin

前几天，我转载了一篇我的关于 dependent type 的自问自答到我的博客里。 这是我对于 dependent type 这个类型系统的功能的一些思考，毕竟这是整个 LambdaCube 中最难实现好的一个特性。

仔细地总结一下，核心就是这么几点：

+ Inductive data family
+ Type level functions
+ Dependent pattern matching
+ Totality check

第一个就是指 GADT 了，第二个呢顾名思义。第三个指 Dot Pattern、Absurd Pattern（实现上一般叫 inaccessible patterns），第四个包含两部分——exhaustiveness check 和 termination check。

———

第一个 Inductive data family 参考 here which 我都还没看懂
第二个 Type level functions here （Idris）我也没看懂 还有一个容易理解点的（Haskell）here
第三个 Dependent pattern matching
我根本找不到多少资料（DuckDuckGo 里）估计 Baidu 上更是不可能有了
这就是某些人所说的「你们在（大学）外面根本学不到的知识」（其实是因为你们太菜了，拿到资料也理解不了，即使英文水平好也看不懂，hhhhh）
here 有个 papper，不过我也看不懂，很想打印下来慢慢看...
第四个我勉强看过儿童书（没错，没完全看过两遍以上的在编译原理 & 程序设计语言里，连个「儿童」都算不上，只能算是「婴儿」<del>息子炸裂</del>）
Totality 就是指函数定义的「呃... 就叫它（完全性）「全函数」吧，因为我找不到别人有做的翻译」
total function 对应的就是 「不 total」的 partial function「部分函数、偏函数」，貌似属于数理逻辑知识范畴。

通俗的（The Little Schemer 即是）来说，全函数即为「处处有定义的函数」，而偏函数即为「未必处处有定义的函数」
这又不得不牵扯到一些数理逻辑方面的概念... 比如定义域... 范畴... 我不会... 算了

（我在百度找全函数，居然只有几个小知道问答真正提到了它，看来全民数学的激情还是不够高啊 hhh）

(define total (lambda (b)
  (* 5 (+ 2 b))))

这玩意是全的，因为我们知道 λb. b + 2 * 5 这乘法和加法都是「为所有输入 b 生成值的，b 是 1 也生成，b 是 -100 也生成」

; type of eternity is Noting ⏊
(define eternity (lambda (eternity)))

(define partial (lambda (c)
  (+ c (- 5 (eternity)))))

这玩意非常不全，因为它的定义用到了 eternity 这个纯纯的不全函数，它要拿到 (eternity) 的结果 Noting（like the one in Kotlin with the same name）就是 impossible 的

Rust 里就是（! means Nothing, NoReturn）

fn eternity() -> ! {
  loop {} // or eternity();
}

上面说的 exhaustiveness check 和 termination check
第一个是「匹配穷尽性检查」，Rustc 就会做这个 oc
第二个是著名的停机问题的... 相干的问题，就是问一个简单的问题：（子）程序会不会停止？

比如 eternity 就是一个永不停下的函数，它不会结束。至于其他的看 wikipedia

In computer science, a termination analysis is program analysis which attempts to determine whether the evaluation of a given program will definitely terminate. Because the halting problem is undecidable, termination analysis cannot be total.

The aim is to find the answer "program does terminate" (or "program does not terminate") whenever this is possible. Without success the algorithm (or human) working on the termination analysis may answer with "maybe" or continue working infinitely long.

总之嘛，就是说这是一种代码分析手段，目的是获取和「在求值指定程序时程序能否确定性的终止」，并且由于著名的停机问题（当然，你们不明觉历是真的，不过我告诉你们这停机问题可是大名鼎鼎的『阿兰·图灵』拿他那大名鼎鼎的图灵机计算模型（我快吐了...）证假的，然后你们就会瞬间... 瞬间... 哇好厉害啊... 为什么呢... 其实没必要的吧）

并且由于著名的停机问题，不可能对所有输入程序都能判断出会不会停下，所以这种分析是「部分」的，不能是「完全」的（不对所有输入生成值）

你有很强的直觉，你可以看一会代码然后告诉用户们函数 total 不 total 会不会 terminate
现代电子计算机可没有你那么强的直觉。

这就是那么多那么多 PhD 奋斗几年所做的，你看看他们在自己书上对人脑表示出多么大的敬仰啊... 最好的计算机... 有些人还在担心被电子计算机里的人工智能取代... 虽说人脑也或许是电子的吧... 不过一看一下 x86 一纯线性模型人脑一个比几何还几何的模型就知道谁输谁赢了，一个拼算力拼紧凑拼规模拼一个拼... 什么呢，或许是单元集合大小？