#blog #recommended https://ice1000.org/2018/11/16/BeyondDependentType/

顺推冰封哥新文 dependent type 之上还有更高级的类型系统吗？

当然我个人 PLT（这里意味 Programming Language Types）毫无水平，只会 Kotlin、Jawa、Crystal 系简单语言的类型系统
可以说是非常菜了

当然这个是要看发展的，拿别人的水平批判 duangsuse 的话是不接受的（比如，冰封几年前就在写 C++ 搞 OI，我去年才会写简单的 Java 7），拿没有作品批判也是不接受的（原因我在本频道上说过）

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 行。上面的那个是六行