The Future of Programming is Dependent Types

Read the example in this excellent blog for explanation of Dependent Type (ie Type depends on its Value) :
eg.

Type ArrayOfOne with value ‘length’ of INT 1.

Type ArrayOfTwo with value ‘length’ of INT 2.

Type ArrayOfThree with value ‘length’ of INT 3.

Then compiler will know if correct (before run time error) :

ArrayOfThree = ArrayOfOne + ArrayOfTwo

or wrong if:

ArrayOfTwo = ArrayOfOne + ArrayOfThree

https://medium.com/background-thread/the-future-of-programming-is-dependent-types-programming-word-of-the-day-fcd5f2634878

Advertisements

小算盘 大乾坤 Abacus

浙江临海市 国华珠算博物管主人 木匠 雷国华 收藏算盘20年,凭个人力量,保存中国算盘发源地的文化遗产,为此散尽钱财借债,免费开放给公众参观。说到家人因支持他而受苦,感慨激动不已。

中国的算盘上面2珠 (2×5),下面5珠(5), 共15,加1 = 16 进位。古代是16位 (Hexadecimal) 制, 半斤 八两 (= 1/2 斤 x 16 两 = 8 两)。

日本改良成10位制: 上面1珠 (1×5),下面4珠(4), 共9,加1 = 10 进位。

明朝万历年间的 “平民王子”朱载堉 (1536 AD – 1610 AD) 发明现代音乐的 十二平均律 (12-tone Equal Temperament) , 用81档的大算盘算出:先开立方根,后开平方根 2 次

\boxed { \displaystyle \sqrt[12] {2} = 2^{\frac {1}{12} }= 2^{{\frac {1}{3}}.{\frac {1}{2}}.{\frac {1}{2}}} = \sqrt {\sqrt {\sqrt[3]{2}}}}