（狂）听到了吗？你们 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 一纯线性模型人脑一个比几何还几何的模型就知道谁输谁赢了，一个拼算力拼紧凑拼规模拼一个拼... 什么呢，或许是单元集合大小？

MSI 主板的虚拟化选项竟然在 Overclock 设定里...

BF5 光线追踪 RTX 支持需要升级 Windows 10 1809

https://corei9.intel.com
Intel 又一次抽奖
包含一个第九代酷睿 i9 处理器(型号目前未知)和悉尼场电竞朝圣之旅

#math #cs #pl #scheme #lisp #haskell 计算模型们

#windows #sysadmin

调试（乱搞） OpenWrt 的时候想用 JuiceSSH 连上去永远没反应
一开始还以为是又弄坏了什么
然后突然发现 Android 没网时会自动切换到移动数据（— Rachel (ﾉД`)ｼｸｼｸ (@tangrui003) November 18, 2018

#android #sysadmin #embedded #hackPi emmmmm 🙈 喔，有时候 OpenWRT 还断电来着，就没信号了...

pic.twitter.com/dGYjnPLn1E
— 抠脚肥宅大汉 (@hakureyuyuko) November 18, 2018

in GNU C > 99

#include <stdio.h>

int main(int argc, char *argv[]) {
  char c = ' ';
  while (c = getchar() != EOF)
    putchar(c);
}

in Haskell
main = readLine >>= putStrLn

in Ruby
puts(gets) while true

in Python 2/3

while True:
  print(input())

in JavaScript

let stdin = process.openStdin();

stdin.addListener("data", (d) => console.log(d.toString()));

in InScript

loop |> gets >> puts

in Ada

with Ada.Text_IO; use Ada.Text_IO;

procedure AI is
  S: String(1 .. 500);
  Last: Integer;
begin
  loop
    Get_Line(S, Last);
    Put_Line(S);
  end loop;
end AI;

in Perl

while ($i = <STDIN>) { print i }

in Kotlin

fun main(vararg args: String) = while (true) { println(readLine()); }

in Julia

while (true)
  println(readline())
end

in Lua

while true do print(io.read()) end

#reveng https://t.me/PureWriter/62

我去，除了我还有人尝试破解纯纯写作了

Disclaimer: 我之前逆向分析纯纯是因为 @drakeet 觉得程序保护的很好，所以我忍不住想试验一下到底有多好

我知道这个说法很欠打但我的动机真的仅仅是因为 @drakeets （之前是 drakeet 的个人频道）上在发纯纯代码保护技术相关内容的，当时的广播是说代码保护得很到位并且作者自己都破解够呛，如此几次自然想试试分析纯纯写作

不过我们看更新日志可以看出，drakeet 是个很擅长做小改进的人，这着实是很不错的，因为各种小细节上的优化是极好的，而且我们也看到了特别特别小的改动没有发布新版本号，版本也基本按照 semver 的惯例命名了

不过纯纯更新了 MD2 的图标看着怕是有待斟酌

notice: 我之前的水平比现在菜多了，而且暑假逆向分析的三天中间有两天都开小差去分析调试修改了个二进制 AXML 文件解析库（后来还被 @drakeet 喷是足足花了三天才破解纯纯写作，其实是总共花了三个小时，其中大部分时间都是在熟悉分析工具使用和部署分析环境），当然目的是为了能在自己的手机上 ADB JDWP （当然，不是直接 DDMS） AndBug 动态分析纯纯写作，最后结果很成功，不过 drakeet 表示他没费心，

当然我现在不可能再碰他的应用了

才没时间....

rt. 👆