#recommended #blog https://codeday.me/

😐 今天暂时就到这里了，如果觉得太少了的话也可以去隔壁的欢乐谷看看《好耶，是形式验证！》

程序设计语言类型扩展起来说多了还是逻辑... 逻辑... 逻辑...

类型是什么？类型就是对程序逻辑本身的高层抽象



; one = λf x. f x
(define one (lambda (f x) (f x)))
; two = λf x. f f x
(define two (lambda (f x) (f (f x))))  

(define inc-abs add1)
(define zero-abs 0)

(define to-number
  (lambda (coded)
    (coded inc-abs zero-abs)))

(define result (+ (to-number one) (to-number two)))

👆 意义不明确，但是可以观察到函数式编程用 abstraction 的时候类型有点被抽提出来的感觉...

对一段程序而言，没有比它本身更好的描述它类型的方式了（这也是为啥 Python 这类语言没有被称为『无类型』 "untyped" 语言，因为它实际上是将类型和程序逻辑本身绑在了一起，只能边执行边检查），而类型系统尝试以更简洁有效的方式对特地用途（类型检查）描述一段程序

类型也是逻辑。

看完上面这些资料（我可花了整整一个假期... 的四分之一来写他们啊！）以后，你最大的感想应该是：

我艹，这些都真 TM 的好好玩啊！

如果不是，请擦亮眼睛再仔细的阅读一遍，直到你觉得他们很 excited 🐸 或者放弃为止

当然，你也可以完全跳过和我这种喜欢一遍一遍辣鸡重复强调的普通人（而不是天才，我觉得冰封很天才，而且除了他我不认识其他同龄同水平的 PLT 爱好者，可见就是所谓的 PLT 高中阶段中国，哦不是中国留学第一了呢，说不定）一起学习的话，也欢迎去隔壁冰封岛和众多知乎真·大牛那看看

如果无视自然发展规律的话（今天在乡下放牛，第二天就站到 MIT 台上讲学尖端量子物理走向人生巅峰，我觉得即便是天才也是不可能的，这被称为“童话”）

#PL https://ice1000.org/languages-cn/#covscript

现在我想起来 CovScript 那个 Parser [include compiler.hpp]... 想想还蛮符合直觉的?
@LEXUGE 在写化学等式解析器的时候也写出了一样的程序算法...

说实在话，我觉得他写的这个... 还真的很复杂，真的，我甚至看了好一会还找不到很多我认为有的东西被放在哪里

https://github.com/covscript/covscript/blob/8c32e7593097c59b3bffc3540209aa6f79c7cbc1/include/covscript/impl/compiler.hpp#L54

这里他还写了个自动机... 虽然我现在还不想从 eval 函数开始找解析过程，但我已经找了好一会还不清楚解析器的是什么样的，说明要不然 CovScript 的解析器架构我不熟悉要不然它太复杂了，不够简洁易理解
即便只是预先处理词条们，自动机（但是无状态）这种方式... 我都没有想出来过，因为我一直在用 Stream 的... 而且 cs 所谓的 compiler 其实基本上还包含了半个 parser 的代码... 而 parser.cpp 里却只是一些辅助 compiler.hpp 工作的方法实现...

我想如果我是第一次写，我也会想出把词条线性表按优先级拆分（在 C 里面就是直接走指针运算）然后子程序下去规约的形式... 🙈

虽然现在我是直接使用递归下降法在词条流上解析二元表达式组。

总之等我同样是自 GC 的 Ra 语言定义好实现了再看吧，现在稍微有点感觉了.... 但还是很累，总感觉可能在词条列表本身上一遍一遍做了很多处理，不是一次完成解析的

#GNU GIMP 好像就有这个功能(XPM) 的说

https://t.me/one_real_world/1809

https://javl.github.io/image2cpp/

看上去有点意思。

#计算机

我一定是闲的无聊了....

默写就不用了，使用了 JQuery 的一些函数基本会用
... 算了还是写一点（

#web #html 之前的盒模型参考这里; 这次花了多久呢... 足足有 20 分钟！太长了呢...

#web #html 使用 JQuery，CDN 是 CDNJS (Cloudflare)

https://duangsuse.github.io/Essay-HTMLs/

1+ 发布

#Haskell 1+ 重写

其实不是 Point free 的，不过那也只是风格问题而已

#Haskell 又修改了一下，很无聊啊... 明明我还有事情的...

更加好看的版本，不过也不是完全 Point-free 风格，毕竟 cyclicIndex 函数的 (!!) 要连着收两个 xs 没办法简单的拿到，而且那样也过了，反而背弃了函数式编程的原则... 这（这里指王垠喷过的 Haskell 对纯函数无副作用和引用透明性『属性』的吐槽，也不是没有道理但没有惰性求值还是 Haskell 吗；上面没有 Monad 的 Type Instance）和 Monad 自不自虐不是一回事了，另外我其实也不完全理解范畴论，只是准备去写 Haskell 而已，这周本来想写篇 Literate Haskell 的说... 可是好像事情不少，算了 #Haskell

范畴论和 Monad 真的好难理解的，我又不想从了阮一峰老师那种简单粗暴的高层抽象，
学范畴论本来就是要彻底理解理论，为什么我要为了实用时能『简单理解』而去把范畴看成容器呢？虽然使用起来也没有大问题

本来我主要还是部分理论方向的... 虽然应用编程系统编程编译器...什么的肯定也要包括喽；但是理论是绝对不能少的
啊... 这周本来打算多弄点代码的，顺便尽可能多写点应用吧，最近总是感觉老讲理论会被人喷是装 B、没有实践能力、 废物人间之屑

果然还是有问题呢... 🐱 尽可能努力吧！

说起来，这个 TCO 函数我现在居然能直接通过原理自己想出来了（虽然和上面的不一样）

//export default tailrec;

function tailrec(rec_fun) {
  let stack = [], isTailCalling = false;
  let lastresult;  

  let tailcalls = (args) => {
    while (stack.length !=0)  
      { lastresult = rec_fun(...stack.shift()); }
    return lastresult;  
  }   
  let cont = (...args) => {
    stack.push(args);
    if (isTailCalling) return;
    else { isTailCalling = true; }

    let result = tailcalls(args);

    isTailCalling = false; return result;
  };
  return cont;
} 

module.exports = {tailrec};

Node 对 ES6 的支持折腾了半天.... Node 的 ES6 Module 支持，真的很辣鸡
看起来，大部分 JavaScript 前端甚至『全栈工程师』的平均水平，还真是不如纯 Java『后端』呢，因为 James 他们给 Java 9 加了很好的模块化系统，可 Node 作为『最流行』的玩意，这方面比起 Java 来就显得 Java 很『学术派』了，emmm...

debug 了半天.... 对 Expansion operator 使用不够熟悉；现在还有点鬼畜，不能好好 Handle optional arguments
但是我 REPL 的时候没有问题，辣鸡 Bable CLI；前端程序员的细节水平果然辣鸡，如果你写的程序无限运行，你甚至不可以用 SIGQUIT 和 SIGINT，它给我的感觉就是 Node 太可怕了... 居然退出不了...

啊，终于发现问题在... 我的测试程序写错了，我这个数学渣渣... 应该拿去给 Engima 的设计者好好批判一番... 😭

function factorial$() { var rec = (ac, n) => n===0?ac: rec(ac*n, n -1); return (y)=> rec(1, y); }
tailrec(factorial$())(100)

当然 sum2 函数就好写多了

sum2 = tailrec((x, y) => x===0?y: sum2(x-1, y+1));

我忘记了，任何数乘 0 还得 0... #math
说起来这还是我最不搞笑的低级错误；最搞笑的莫过于把 『除数不能为 0』弄成『被除数不能为 0，除数可以，如果除数是那结果是 Infinity... 等等』

ghci> 0/0
NaN
ghci> 1/0
Infinity
ghci> 0/1
0.0

Prelude> 1 `div` 0
*** Exception: divide by zero
Prelude> 0 `div` 1
0

显然分母不能为 0...

哦对了 #fix 一个之前关于 #PLT 的隐式定义：在 Product type 里；如果两个乘类型都是 Zero sized type，那结果也是 Zero sized type
我之前说过 ZST 好像就是 Product /sum type 的 1 来着，1*1 可是还得 1.... 啊？好像也没错...（说了 1 是 ZST... 所以说数学辣鸡 duangsuse...）

替换了原来的短路式伪分支逻辑

if (!active && (active = true))

因为我觉得它不够明确
并且也没有使用书上的两个 if 风格，而是使用了 return 在更大区间上操作控制流
至少；现在的我比以前又强了一些，需要继续努力！

（别人之前的是）

function tco(fun) {
  var value = null, active = false, accumlated = [];
  return function accumlator() {
    accumlated.push(arguments);
    if (!active && (active = true)) {
      while (accumlated.length != 0) value = fun.apply(this, accumlated.shift());
      active = false; return value;
    }}}

上面的代码会在过会的一些（当然会往 gh 上发的）文字上出现

#Haskell 一个关于 Haskell Rank-N-Polymorphism 的小贴士

虽然不是很明确，Haskell 是一门崇尚彻底抽丝剥茧的语言，它应该拒绝我这种一知半解的...

说起来，最近又学到了点 Agda，也是幸运，因为我有在学 type theory 的说，所以 Agda 写的是什么我能猜出来，加上之前我已经猜过了（只不过那时我还太菜；类型系统对我来说就是个黑盒，我只知道一点点微不足道的知识甚至不足以使我看懂 #Agda...）

这里也不会教大家啥是 Monad, 啥是 Functor, 啥是范畴（含宏半群）啥是 flatMap 操作；只需要看懂 do notation

上面就是这里喽

main = do
  print $ natToInt (add one three)    
  putLine
  foldl (>>) (putLine) os
  putLine
  print $ natToInt (add three five)
  putLine
  printNat $ mul three five 
  printNat $ mul five three
  printNat $ mul Zero five 
    where printNat = (print . natToInt)
          os = print <$> (natToInt <$> [one, two, three, five])
          putLine = putStrLn []

好辣鸡... 其实我可以用 Destruct 的，那时候我还 Niave 🐸 些不知道

(Succ four) = five

—
比如这里有一个小 IO 程序

{-# LANGUAGE ExplicitForAll #-}

module ExplicitForalls where

main :: IO () 
main = do  
  printLn "1 + 1\n  = "
  printLn 2
  where 
    printLn :: forall a. (Show a) => a -> IO ()
    printLn = putStrLn . show

这里是没有问题的；可是如果用 TypeClass、TypeInstance 的话会怎么样呢？

（然后就突然发现自己讲的很没有意义）

🐕
自作聪明以为把下面的 a 换成 (forall a. a) 就可以解决类型推导失败的问题呢，可是

Illegal polymorphic type: forall a1. a1

GHC doesn't yet support impredicative polymorphism

这已经不是 rank n polymorphism 了，rank n 是（当时我打印的版本好像比较老旧，作者使用的表达方式我看了好久也只有一点感觉....）

rank 0:
单态 t
1:
变态 forall a b. a -> b (Rank 1)
2:
forall c. (forall a b. a -> b) -> c

看 Rank 几直接数 forall 有几个就好了

总之，这很明显嘛。Haskell 的 RankNTypes 默认是 Rank2

∀c → (∀a b. a → b) → c

这里假设给柯里化过的第二个参数起名 f, 那 f 的类型就是可以确定很多次的，只要是 forall a b. a -> b 就可以了
∀ 是 Universal qunatifier，相关知识是高二的推理和证明，这里 forall a. a -> String 表示对于任意类型 a 都有某个名字的 a -> String 这个操作存在，比如 a 是 Int; Int -> String, a 是 IO Int; IO Int -> String （这里不是 Constraint，何况 IO a 本身也是一个类型，Haskell 的 => instance 查找只是隐式了一点而已）
→ 就是一个 Function 类型架构器；放到 Kotlin 就是 Function<in Q, out R> (kotlin.Function<_,_> 当然是做了声明处型变的，我这里写出来只是强调）
a b c 都是 Hindley-milner 的 Type variable

而如果不开 ExplicitForAll，就默认是

∀a b c. a → b → c

那 f 就只能是第一次推导出的类型喽，比如 String -> Int; String -> IO ()



{-# LANGUAGE UnicodeSyntax, RankNTypes #-}
play :: forall c. (forall a. Show a => a → c) → [c]
play f = [f 1, f "Int"]

ok = play show

然后

ok 是 ["1","\"Int\""]
总之，就是要记住类型是命题... 然后不要老想着去抄别人的，对于理论们，真正的理解不是抄能抄过来的。
— 这个是复制的

rank2 :: forall b c . b -> c -> (forall a. a -> a) -> (b, c)
rank2 b c f = (f b, f c)

rank2 True 'a' id
-- (True, 'a')

— Scala 没有 RankNTypes 就只好模拟喽

def rank2[B, C](b: B, c: C)(fnk: Id ~> Id): (B, C) =
  (fnk(b), fnk(c))
rank2(true, 'a')(FunctionK.id[Id])