duangsuse::Echo

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

26 viewsduangsuse ¯\_(ツ)_/¯ |学渣|母上千古, edited 14:27

duangsuse::Echo

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

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

23 viewsduangsuse ¯\_(ツ)_/¯ |学渣|母上千古, edited 14:37

duangsuse::Echo

This media is not supported in your browser

VIEW IN TELEGRAM

22 viewsduangsuse ¯\_(ツ)_/¯ |学渣|母上千古, 15:22

duangsuse::Echo

Forwarded from 神奇的笔记 (神楽坂立音)

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

2 viewsduangsuse ¯\_(ツ)_/¯ |学渣|母上千古, 15:29

duangsuse::Echo

Forwarded from 神奇的笔记 (神楽坂立音)

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