## 定義 ```idris data Term = TmPos Position Term | -- 剩餘的 term constructor ``` 對應的 error report monad ```idris report : String -> Either (String, Maybe Position) a report s = Left (s, Nothing) addPos : Position -> Either (String, Maybe Positio

Idris 的 effects 模組可以用來管理複雜的副作用，只要觀察最右邊的效應代數列表就可以看出當前可以使用的副作用。下面的程式是一個簡單的案例，展示 `STATE` 跟 `STDIO` 的使用方式。 ```idris inc : Eff () [STATE Int] inc = do put (!get + 1); pure () hello : Int -> Eff () [STDIO] hello i = putStrLn $ "Hello world! " ++ show i

在開發一些 theorem prover 程式的時候，常常會需要打出像是 Γ、λ、ℕ 之類的字元，這時候用 [packer](https://github.com/wbthomason/packer.nvim) 安裝 [arthurxavierx/vim-unicoder](https://github.com/arthurxavierx/vim-unicoder) 就很方便 ```lua use 'arthurxavierx/vim-unicoder' ```

之所以有這個需求是因為 m1 上目前 9.2 系列就只有 9.2.5 可以運作，同時 hls 對 9.4 系列的支援似乎還不完整，我之前是手動開關 `stack.yaml` 裡的 compiler flag 來控制。這裡我的解法是編譯一個目標是 ghc 9.2.5 的版本 ```shell ghcup --verbose compile hls --cabal-update --ghc 9.2.5 --git-describe-version --git-ref aeb57a8eb56964

用指令 ```shell brew install git-delta ``` 安裝。去[設定頁面](https://dandavison.github.io/delta/configuration.html)看更多細節

今天要解析的是 [elaboration-zoo](https://github.com/AndrasKovacs/elaboration-zoo/blob/master/02-typecheck-HOAS-names/Main.hs) 中的一段程式，其中用到了 conversion check 的技術。 ### 型別檢查 這裡列出重要的兩個定義： - environment：儲存變數的計算結果 - context：儲存變數的型別 ```haskell type Env = [(Nam

## Identity in group is unique ### Proposition If $h \in G$ is an identity of group $G$, then $h = e_G$ ### Proof $$ h = h \cdot e_G = e_G $$ 1. forall $a$, holds $a = a \cdot e_G$ 2. forall $a$, holds $a = h \cdot a$($h$ is an identity). ## I

很長一段時間內，數學家都認可 $1$ 是一個質數，畢竟它「只能被 $1$ 或是自己整除」。 直到要唯一化質因數分解的結果，讓它具備特殊性，才將 $1$ 排除掉。 因為 $6 = 2 \times 3 = 1 \times 1 \times 1 \times 2 \times 3$， 其中 $1$ 要乘上幾個都可以，也讓我們越來越常說「除了 $1$ 的質數」。 這就構成了好理由寫出 $1$ 不算在內的質數定義。

我們想要證明下面的程式碼就是 $y \to y+1$ $$ \begin{aligned} \\& inc \; 0 \to 1 \\& inc \; y \to 2 \cdot inc (\lfloor y/2 \rfloor) \\& \;\;\; where \; y = 1 \pmod{2} \\& inc \; y \to y + 1 \end{aligned} $$ 我的方法是根據每個情況分別證明 ### 簡單的部分 1. $y = 0$ 時 $0 \to 1$ 這個情況

在群中，我們用指數來表達累積的運算，例如 $g \cdot g \cdot g = g^3$。 並且為了符合指數律令 $g^0 = e$ > 指數律是我們想使用這種表示法的主要理由 ### 群元素的階（Order）的定義 任意一個元素 $g$ 的階被寫成 $|g|$。 定義是當 $g^n = e$ 而 $n$ 1. 是個正整數 2. 不存在任何正整數 $n'$ 同時滿足 $n' \le n$ 跟 $g^{n'} = e$ 這時，說 $|g| = n$。 但這個正整數也可能不存在，這時

racket 8.7 這次我比較晚更新，才發現我居然用了快 10 秒才想到下面的 migrate 指令，所以我覺得要把流程紀錄一下。 下載網站就和過去的發佈一樣在 [https://download.racket-lang.org/](https://download.racket-lang.org/)，只要根據自己的電腦選擇合適的版本即可。 ### 設定 environment variable 這邊是跟 executable 有關的設定，下面會為 macOS 特化 ```sh exp

GPG 還蠻麻煩的，所以順手紀錄一下整個流程順便複習自己的知識 ### 列出系統上的 keys 用 `gpg --list-secret-keys --keyid-format=long` 讀出 keys ```sh gpg --list-secret-keys --keyid-format=long ``` #### 生成新的 gpg key 要是你還沒有 key，那麼就需要 `gpg --gen-key` 先生成一把 ```sh gpg --default-new-key-al

最近又看到哈代跟拉馬努金的 1729，所以就寫了一下程式去找能夠被表示成兩種以上立方和的數 ``` 1729 4104 13832 20683 32832 39312 40033 46683 64232 65728 110656 110808 134379 149389 165464 171288 195841 216027 216125 262656 314496 320264 327763 373464 402597 439101 443889 513000 513856 515375

```shell brew install webp cwebp a.png -resize 60 60 -o a.webp ```

```shell brew install optipng optipng -o7 xxx.png ```

最近工作上的開發，對 wasm 的實務又有了更多的掌握，同時發現 wasm 各種資訊的缺乏。 尤其很多技術細節散亂在數十個不同的網頁中，各家編譯器跟 wasm 執行環境又充斥讓人頭痛的小毛病。 所以我決定記錄下各種實用的技巧。 ### Rust 相關的標記屬性 Rust 中的各種標記對編寫能用的 wasm module 置關重要，在其他語言很多 wasm 的特性根本用不出來。 這是目前多家編譯器各自實作 wasm 的碎片問題，不是每個語言都能良好的支援新的 wasm proposal。

### 模仿 1. 要去拆解別人的成果 2. 不能是全然模仿 3. 一點點新奇比全然新奇更容易被接受 4. 接受能力與目標永恆的落差 ### 有效的練習 再來幾乎就是《刻意練習》的重複 ### 知識的詛咒 1. 專家反而不太擅長解說自己的技能 2. 知道答案會改變我們思考的方式 ### 尋求回饋 1. 有效的回饋具有明確性 2. 用請求建議的方式比請求回饋更容易得到好的回饋 3. 來源對象必須能代表目標受眾 ### 用不同角度觀看批評 負面的批評代表改善的機會

layering 的概念其實並不陌生，在不同的程式語言裡面有諸多實現不同類型的限制的方式。 最常見的一種就是 type system，其他像是 eBPF 的 logging 與 process 分開也能算是這樣的工具， 甚至是最簡單的 assertion 也能幫助我們進一步對程式做更多的推斷。 ### Software Design for Flexibility 在這本書的第六章用比較彈性的方式建立了 layering 的統一系統，例如說重力可以寫成 ```scheme (define

在傳統的 ML 或是 Haskell 裡面，有一個型別表現的特別醜陋，就是 data type 表示的 disjoint。 這是因為無論如何，disjoint 就是會需要執行期時有要處理哪個分支的資訊。 因此語言中都設計有 constructor 這麼一個特殊的存在，其中每個 case 都有對應的執行期標籤。 舉例來說， ```ocaml type bool = false | true ``` 這裡 `false` 可能就是 `0`，`true` 就是 `1`。 ```ocaml ty

重複賽局的作法是假設參與者並不只做一次決策，而是必須反覆對某個博奕重複多次。 用不盡完備的說法，一次的勝利並不能長期帶來利益，例如對方可能報復。 而這也更加的符合很多現實世界的情況。 此外隨著階段進行也可能有均衡的變化。

這個方法仰賴 mastodon 的 RSS feeds，假設 1. 站點是 `abc.social` 2. 個人 ID 是 `xxx` 那麼應該會有一個網址是 RSS feeds 的連結，通常叫做 `abc.social/@xxx.rss` 或是 `abc.social/@xxx.atom`。 有了這些接下來不管用什麼方法，只要把需要的資訊轉發出去就結束了。 我個人是採用 ifttt 的服務，不過因為原理很簡單，原則上也可以自己寫程式處理。

有些資料結構可以有效的存取任意元素，但有時候我們需要的只是高效存取最小的元素。 支援這種存取模式的資料結構就叫做 priority queue 或是 heap。 而 heap 經常用 heap-ordered tree 實作。 ### Heap-ordered 所謂 heap-ordered，就是每個節點的元素不大於其子節點的元素。 在這個排序下，樹的最小元素總是在根節點。 ### 左偏樹 左偏樹的定義是滿足 leftist property 又符合 heap-ordered 的二元樹

首先定義型別 $1$ 是只有唯一一個元素的型別，我們不關心這個元素到底叫做什麼。 同理 `Bool` 就會是 $2$，因為它有兩個元素，而其他一樣有兩個元素的型別是同構。 ### 乘法 那麼乘法可以視為 `Pair`，記作 $A \times B$。 可以由檢查 $1 \times A$ 跟 $A \times 1$ 是否跟 $A$ 同構來檢驗這個想法。 #### 檢驗 以下的 Haskell 程式裡，`()` 是 $1$ 型別，小寫的型別則是型別變數，恰巧方便讓兩個定義適用於任何型別

This note will not be very complete, but might become a series. ### Effect as interface The first case, use `maybe` to implement `raise` effect. ```koka fun raise-maybe( action : () -> <raise|e> a ) : e maybe<a> with handler return(x)

Each Wasm module instance is a verified and well scoped object, its memory can be defined and entries are its functions. Thus, the potential of Wasm module instance is they can be the unit in concurrent programming, since we can know how many resour

How to proof a program will stop and give us an answer? This big question leads halting problem, but not the end. Even though we cannot get a result for arbitrary program, get this information for certain kind of program might still useful. However,

- 數學之美 吳軍 - 全知讀者視角 04 - 小書痴的下剋上 第五部 2,3,4 - 冰菓

1. `~/.agda/defaults` ``` standard-library ``` 2. `~/.agda/libraries` ``` ~/.agda/agda-stdlib/standard-library.agda-lib ~/.agda/cubical/cubical.agda-lib ~/.agda/agda-categories/agda-categories.agda-lib ```

記錄一下一個有趣的函數：**joint denial**（又稱為 **Peirce's arrow** 或是 **NOR**）。它的真值表是 | P | Q | P ↓ Q | | ----- | ----- | ----- | | true | true | false | | true | false | false | | false | true | false | | false | false | true | 這個函數好玩的地方是其實我們熟悉的所有邏

## Introduction In the excellent library nanopass, we can define a language via `define-language` and make pattern matching on it by using `define-pass` or `nanopass-case`, the most important thing nanopass given here is the generated code for thes

Two years ago, I have a [post](/blog/2020-05-16-de-bruijn-index) about de Bruijn indices. I don't think de Bruijn indices order is important, it turns out, that's wrong! ## Introduction What's the order of indices? It means we have two choices 1.

## 說明 所謂的使用參考等價性呢，是指在某些語言裡面，兩個物件是否相同是通過參考而非內容決定的。 舉例來說，**racket** 裡寫下一個空結構，然後生成一些實例 ```racket (struct id ()) (define a (id)) (define b (id)) (define c a) ``` 我們可以用一些 `eq?` 運算來檢查 ```racket > (eq? a b) #f > (eq? a c) #t > (eq? c a) #t > (eq? b c)

## 最開始的問題 在解決 sauron 要如何從定義跳轉到使用位置的時候，我讓 maintainer 之間互相通知依賴關係，由依賴方通知被依賴方。 這樣的程式雖然符合直覺，卻因為實作而受到限制。正如以下推文說到的問題 <blockquote class="twitter-tweet"> <p lang="zh" dir="ltr"> no，這個想法的問題是沒有意識到記憶體開銷出在 thread internal channel 上 <br /> thread

This is a brief note about what a type theory should have and the flow. ## Top level A top level of dependent type language should be a modular thing, whatever a module or big `letrec`. In the top level, we should be able to have a list of definit

## Introduction [ee-lib](https://docs.racket-lang.org/ee-lib/) is an amazing library made by **Michael Ballantyne**, it provides a convenience local context let user can record meta information for a macro, but there have some behaviors I want to r

**typed/racket** is huge and seems impossible to understand, so I want to make try about this situation. This article will give you a systematic way to learn how to break down a complex macro system, by showing you a short tracking into typed/racket

In Racket GUI, [`framework/preferences`](https://docs.racket-lang.org/framework/Preferences__Textual.html) is a built-in module that allows you to set and get configuration for your GUI. However, invoking [`preferences:set-default`](https://docs.rac

I want to make this record as a post to ensure I can remember these nice decisions in the future. Let's start with a brief history of the project. A few years ago, I think is 2020 July, I found Racket has no nice IDE for many reasons. Mainly, we onl

In MacOS, we have crontab and periodic can pick, but I didn't find how to set a certain time like 3 pm to run the periodic. Thus, I switch to crontab and it's very easy to use, you can type the command: ```sh crontab -e ``` Or you like to run comm

- 區分工作事項跟一般事項 - 工作時間：工作開始、結束按鈕 - 工作時間時建立的事項都是工作事項 - 工作時間內看不到一般事項，反之亦然 - 事項時間標記 - 事項提醒

The following code records how to convert bytes's encoding in Racket, from MS950(CP950) to UTF-8 ```racket (define-values (result success-length status) (bytes-convert (bytes-open-converter "CP950" "UTF-8") #"A888º£BC")) result

First of all, a resume should reduce the job that HR has to do, [stop ruining your resume](https://zriyansh.medium.com/stop-ruining-your-r%C3%A9sum%C3%A9-c8ca15de5a98) is a good article you should read first if you have no idea why you want to use t

Rename the title of Utterances issues can be helpful when moving site to different URL, the following code is how can we make it. ```shell read -p "current URL of site? " current_site_url read -p "new URL of site? " new_site_url if [ -z ${current_

鑑於[上次的分析](/blog/2022-04-04-mech-analysis-for-mech-arena/)在這幾輪改版之中已經有點變化，這次會針對改變的部分進行說明。 1. Surge 大幅強化 2. 新機甲 Orion ### Surge(24) 強化內容 - 血量增加。比 Killshot 血量高一些，至少不是薄皮脆雞了 www - 速度上升到 Shadow/Killshot 水準 - 技能部分 - 縮短重啟所需的秒數 - 定身範圍增加。但最好不要用 radius

考慮 $F(x) = f(x)g(x)$，求$F(x)'$? 直覺上會因為 $f(x)+g(x)$ 的微分是 $f(x)'+g(x)'$，而認為結果是 $f(x)'g(x)'$。 那我們馬上實驗看看？令 $f(x) = x$ 且 $g(x) = x$，得 $$ (x\cdot x)' = x' \cdot x' = 1 \cdot 1 = 1 $$ 這顯然是荒謬的結論，所以這應該是錯的。 不如回歸本來的定義？ $$ F(x)' = \lim_{t \to 0} \frac{F(x+t)

今天我想介紹一篇論文 [Programming with union, intersection, and negation types\*](https://arxiv.org/pdf/2111.03354.pdf) 其中差集類型的概念，而紀錄下這篇文章。 我們已經很習慣各式各樣的 polymorphism 了。例如 Parametric polymorphism 說我們可以引入型別變數，呼叫函數的時候時實例化一個適當的型別。 此論文不考慮 prenex form 以外的情況，顯然是因為 $

Usually, we have a pattern `E` have to find from a syntax tree, this is a trivial case in nanopass since it defaults on. For example, if we have a small language have symbols, integers, and addition. ```racket (define-language INT (terminals

**Riemann integral** is a good start for learning integral as the first rigorous definition of integral on an interval. ### Definition #### Part 1 Let $f(x)$ be a continuous function on the interval $[a, b]$, we can make a $m$ cut($m \in \mathbb{

Commands ```shell brew install basictex export PATH=$PATH:/usr/local/texlive/2022basic/bin/universal-darwin sudo tlmgr update --self sudo tlmgr install texliveonfly ```

Rhombus is Racket 2(maybe?), an another syntax style choose for Racket's User, one must write `#lang rhombus` to use it. To install, use ```shell raco pkg install --auto rhombus-prototype ``` ### Expression and block form ```racket 1+1 begin:

The Archimedean principle is: If $a$ and $b$ are real numbers with $a > 0$, then there exists a natural number $n$ such that $na > b$. So $n > \frac{b}{a}$, by this we can have a particular example. Let $a = \epsilon$ and $b = 1$, then $n > \frac{

Recently, I'm working on a [theorem prover](https://github.com/racket-tw/k), and implementing implicit parameters. This brings a hard problem for me, and the idea get from [type theory elaboration implementation](https://www.youtube.com/playlist?lis

對至少六星的機甲分析，排序是我對操作難度跟強度的綜合排名。 大致是基於我的經驗跟參考 [Mayer](https://www.youtube.com/channel/UCxA1VejLBvK1tiVjEQPd-tA) 等高等玩家的影片分析來的。 前幾名的差距並不大，基本上都是可以被當主力練的，而後面的只是操作難度高或是需要對地圖有高度的理解等等，除了 Arachnos （沒提到的某台歡迎您直接遺忘它 www）。 - 機甲技能距離都是約 30m（但部分技能實際距離就是 29m，不要問為什麼 w

這篇是我對 HoTT(Homotopy Type Theory)目前的理解與整理，如有錯漏歡迎提出修正。 要理解就要先知道 identity 問題，即 `x ≡ y` 這樣的型別，在 extensional type theory(e.g. MLTT) 裡面是唯一的，即對 `P Q : x ≡ y` 可以證明 `P ≡ Q` ```agda UIP : (X : Set) → ∀{x x' : X} → ∀(r s : x ≡ x') → r ≡ s UIP X {x} {.x} refl

Closure conversion is an important transformation in compilers, especially for functional programming languages. To know why this is important, you should know what closure is. To understand closure, [lambda calculus](/blog/2020-01-01-note-what-is-l

`let/cc`'s type cannot be inferred by typed/racket, but the type of it is always `(-> T Void)` for a function returning `T`, so one should write ```racket (: foo : -> T) (define (foo) (let r : T (r t))) ```

Field is a nonempty set $\mathbb{F}$ with two binary operations 1. addition: $+$ 2. multiplication: $\cdot$ satisfying the following five axioms. 1. Commutative Law: If $a, b \in \mathbb{F}$, then $a + b = b + a$ and $a \cdot b = b \cdot a$ 2. Di

A recursor of $\mathbb{N}$ is like the following $$ \begin{aligned} & R^\mathbb{N} : C \to (C \to C) \to \mathbb{N} \to C \\& R^\mathbb{N} \; z \; s \; 0 :\equiv z \\& R^\mathbb{N} \; z \; s \; (suc \; n) :\equiv s \; (R \; z \; s \; n) \end{aligne

Encode scheme objects in a word(64bits) is fun and important for dynamic language! The idea is using 3 bits for tagging, 61 bits for data. For small types like `integer`, `boolean`, `char`, how to use that 61 bits is clear , but how to handle comple

Boolean algebra can be encoded by indexing, for example, a venn diagram for two sets: $A$ and $B$ divide diagram to four parts: $1, 2, 3, 4$. Thus 1. $A = \{1, 2\}$ 2. $B = \{1, 3\}$ 3. $A \cup B = \{1, 2, 3\}$ 4. $A \cap B = \{1\}$ 5. $(A \cup B)'

With git hook, we can do automation for some common task, this article record how to use `pre-commit` to auto format changed files. The followig example is for JS project. `package.json` ```json { ... "scripts": { "format": "prettier --ign

Control how to print an object is an important thing in any languages. in Racket, `prop:custom-write` is one of many ways for structure, and it works for `typed/racket` this variant. ```racket #lang racket (struct vec3 (x y z) #:property prop:c

macro is all about delay, let give a form control the computation, for example ```factor t 2 3 if ``` The above program is easy to understand once you know the computation of factor is based on stack and concat. Then you know it means if true, ret

All you need are [deallocator](https://docs.racket-lang.org/foreign/Allocation_and_Finalization.html#%28def._%28%28lib._ffi%2Funsafe%2Falloc..rkt%29._deallocator%29%29) and [allocator](https://docs.racket-lang.org/foreign/Allocation_and_Finalization

Since my macOS using arm64, I can't develop x64 apps on my NixOS, at least it's not as simple as on native machine. Thus, I always have a good reason to ssh to my NixOS and work on it, but I never do that since I'm lazy! This is a journey about how

```shell mix phx.new <project name> --no-ecto cd <project name>/assets npm i svelte svelte-loader --save mkdir -p js/svelte ``` 1. install `Sveltex` in `mix.exs` ```elixir def deps do [ {:sveltex, git: "https://github.com/virki

Racket provides Objective-C bindings, so the best part here is that we can use Cocoa in Racket to build a GUI. In fact, `racket/gui` on macOS is based on Cocoa. The following program is relied on some works in [dannypsnl/cocoa](https://github.com/da

The most famous quick sort in the functional world is from Haskell. To simplify the problem, all elements in given list are unique. ```haskell quickSort :: Ord a => [a] -> [a] quickSort [] = [] quickSort (x:xs) = quickSort [y | y <- xs, y < x] ++ [

NOTE: A problem is single digit print with trailing 0 ```asm .global printNumberEntry printNumberEntry: // asked two words on stack sub sp, sp, #16 mov x15, #10 mov x12, x0 // print prepare // fd(x0) = 1(stdout) mov x0, #1 // len(x2

Start ```racket (define (zero f x) x) (define (suc n) (λ (f x) (f (n f x)))) (define (add n1 n2) (λ (f x) (n1 f (n2 f x)))) (define (λnum->number n) (n (λ (k) (add1 k)) 0)) ``` Play with it ```racket (λnum->number (suc zero)) (λnu

Since I finally figure out how to set up these, I record them and provide some convenience common setup. It's all about environment variable: `CHEZSCHEMELIBDIRS`, it's a common shell path list in `<path>:<path>:<path>:...` format. First, create a

A usage of list files, is building existed C libraries, listing all C files is annoying. ```zig var general = std.heap.GeneralPurposeAllocator(.{}){}; defer _ = general.deinit(); const dir = "./src/"; var sources = std.fs.Dir.Iterator{ .dir =

seven segment display is a form of electronic display device for displaying decimal numerals, the following picture shows how to build it up.  Mapping: 1. 1 -> gpio pin 6 2. 2 -> gpio pin 5 3. 3 -> gnd

我們知道 forth 是一個 stack-based 的連接語言，極度簡單的概念讓它非常容易被 port 到各種機器上，並且不需要太多的 runtime 支援。下面我就來介紹怎麼在 arm64(aarch64) 的 macOS 下寫出對應的 forth 指令。 ### Integer 對整數這種字面值，我們只需要推進 stack ```asm mov x0, #<integer value> str x0, [sp] ``` ### arithmetic 對 `+`, `-`, `*

```shell home-manager switch home-manager expire-generations '-10 minutes' nix-collect-garbage ```

TimescaleDB is a postgres compatible DB with time series extension ### Container for development To run up an instance: ```shell docker run --rm --name dev-postgre -e POSTGRES_PASSWORD=postgres -p 5432:5432 -d timescale/timescaledb-postgis:latest

**blink** is like hello world on Arduino, and here I will show how to do it in zig. First, you need to create a zig project: ```shell mkdir zig-arduino && cd zig-arduino zig init-exe ``` ### Blink(programming) You can look the following picture f

在 2021 的最後一天，要為各位介紹偉大的 errlang，顧名思義，就是更會回傳 err 的語言。典型的 errlang 程式如下 ```go _, err := f() ``` 我們有 err，從來也不檢查 ```go v, err := f() switch err.(type) { // ... } ``` err 的型別總是讓人懷疑 ```go v, _ := f() ``` 我們有時會讓 err 接地 ```go v, _ = f() ``` 接多了就會接

One can get `tree` command on macOS by using ```shell brew install tree # or nix-env -i tree ``` A sample is ```shell tree -P 'lang|*.rkt|*.scrbl' -I 'compiled|doc' ``` for racket project. It produces ``` . ├── info.rkt ├── main.rkt ├── scribbl

`MacroTools` 是 Julia 的一個程式庫，可以大幅簡化編寫 macro 的難度。 ```julia using MacroTools expr = :(Expr(A, B)) @capture(expr, T_Symbol(fields__)) ``` 上面的程式裡面寫了 `:(Expr(A, B))`，意思是 `quote Expr(A, B) end` ```julia @capture(expr, T_Symbol(fields__)) ``` 這段會去比對 `ex

數列 $$ a_n = \frac{1}{2} + \frac{1}{4} + \frac{1}{8} + ... + \frac{1}{2^n} = \frac{1}{2} + \frac{1}{2^2} + \frac{1}{2^3} + ... + \frac{1}{2^n} $$ 我們可以知道 $a_n$ 其值等同 $1-\frac{1}{2^n}$。不過這是為什麼呢？乍看之下很難直接得出這個結論，所以我們可以作圖來幫助思考。 $a_1$ 可以視為一個正方形對半之後的左半

在課堂上，矩形的面積公式被寫成 $lw$ 或是 $l \times w$（讓我們假設長為 $l$，寬為 $w$）。當解釋為何如此時，常常告訴學生這是因為矩形可以被拆解成 $lw$ 個單位正方形。但說到底單位正方形的面積也是用同一個公式算出來的，所以我們不應滿足於這樣的解釋，那麼我們又要怎麼推導出我們常用的矩形公式呢？這就是這篇文章想要說明的事情。接下來就讓我們進入直覺的世界。 根據日常經驗，我們可以知道不管面積怎麼定義，都和長寬有關係。我們可以定義出一個函數 $A$（Area），面積可以表述

Idris has a simple FFI, the following code is an example. ```idris %foreign "C:puts,libc" prim__puts : String -> PrimIO Int ``` To avoid duplicate typing, we usually would write ```idris libc : String -> String libc fname = "C:" ++ fname ++ ",lib

`syntax-property` 可以用來把資訊存入 syntax 中，這可以用在各種有趣的 macro 擴展系統之中。一個我比較熟悉的案例是 type-system，比如我們可以寫下 ```racket (define-syntax-parser Nat [_ (syntax-property #''Nat 'type #'Type)]) (define-syntax-parser zero [_ (syntax-property #''zero 'type #'Nat)]) (

`with` 身為一個多條件過濾器，許多人會像下面那樣誤用它。 ```elixir with ["Bearer" <> token] <- get_req_header(conn, "authorization"), {:ok, data} <- Authenicate.verify(token) do %{current_user: get_user(data)} else %{} end ``` 然而正確的寫法應該是下面這樣。 ```elixir with ["Be

For some projects, like Phoenix project, we need a database for testing. Good news is setting it up is simple: ```yaml jobs: build: name: Build and test runs-on: ubuntu-latest services: postgres: image: postgres:11

Phoenix is a great framework, but sometimes we want to use frontend framework like React. In this article, you will learn how to use them together. First, we create a project with the following commands. ```shell mix phx.new <project name> --no-ect

Long time ago, I play Elixir and write down an [article](/blog/2018-03-31-phoenix-run-and-up/) about [Phoenix](https://phoenixframework.org/). Time has passed, now I'm really working with Elixir XD. Today, I want to show how to set up a [GraphQL](ht

The following code shows how to find max subsequence ```racket #lang racket/base (define (max-subsquence lst) (define maxsofar 0) (define maxendinghere 0) (define maxelement -inf.0) (for ([e lst]) (set! maxelement (max maxelement e))

First step, install [remote pack](https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.vscode-remote-extensionpack). Now, at the left-button of your vscode should have a `SSH: ...` button. After clicked it, there will show some optio

This article ports lexer from [Go implementation](/blog/2017-07-08-lexer-explains/) and ports parser from [Rust implementation](https://github.com/dannypsnl/elz/blob/master/src/parser/mod.rs) to Racket. ### Lexer First, we need some structures tha

這篇文章是從我在 Clojure Taiwan 的分享 [clojure isn't lisp enough](https://www.meetup.com/Clojure-tw/events/277419019/) 改編而來的。由於演講與文章的差異，編排會略有不同，但主旨仍然是 macro 系統與開發方式之間的交互影響。 這篇文章前段的兩大主角分別是 Racket 和 Clojure。Clojure 是 2007 年從 Lisp 家族分支出的不可變範式（也有人說函數式，但對我來說函數式僅需

- [css secrets](https://www.oreilly.com/library/view/css-secrets/9781449372736/) 不用大量細節灌爆你的腦袋，卻在一個個可以直接撿來用的案例中教會你怎麼把 css 的技巧套用到真實世界中 - 黑暗元素 這部應該不需要介紹了吧 lol - 非虛構寫作指南（on writing well） 用簡單的文字透徹地傳達寫作的要點，還有仔細的分析各種題材如何蒐集素材，絕對是文字工作者是不可錯過的好書 -

## Why? strictly positive 是 data type 中對 constructor 的一種特殊要求形成的屬性，這是因為如果一個語言可以定義出不是 strictly positive 的 data type，就可以在 type as logic 中定義出任意邏輯，形成不一致系統。 現在我們知道為什麼我們想知道一個 data type 是不是 strictly positive 了！ #### First Example: Not Bad 了解完 strictly p

How to deploy r16 bot on Heroku. ```shell git clone [email protected]:williewillus/r16.git cd r16/ echo 'web: racket -l r16 ./' > Procfile heroku buildpacks:set https://github.com/lexi-lambda/heroku-buildpack-racket heroku config:set RACKET_VERSION=8.

Add the following code helps GitHub Action caches installed packages. ```yaml - name: Cache uses: actions/[email protected] with: path: | ~/.racket key: ${{ runner.os }}-primes ``` If you install packages via command like: ```shell raco

Continuation is the **future** of the program, for example ```racket (+ 3 2 (* 5 (+ 6 1) 8)) ``` What is the continuation of `(+ 6 1)`? We can get the result by replacing `(+ 6 1)` with a hole: ```racket (+ 3 2 (* 5 ?hole

When we say "A is convex", means for any two points in $A$, the line in $A$(each point on the line in $A$). To prove the title "Is the unit sphere convex?", we need to prove for any two vectors $X$, $Y$ 1. their length $\le 1$ 2. their linear comb

首先用 `define/augment` 往 `on-close` 附加一些額外的控制程式碼 ```racket (define open? #f) (define custom-frame% (class frame% (super-new [label "test"] [width 300] [height 300]) (define/augment (on-close) (set! open? #f)) (se

home-manager 會讀取 `.config/nixpkgs/home.nix` 並套用裡面的設定（config），所以我們可以用一個 git repository 管理並用 ```shell ln -s $(pwd)/home.nix ${HOME}/.config/nixpkgs/home.nix ``` 把設定掛到 home-manager 讀取的位置。一個基本的設定檔內容如下： ```nix { config, pkgs, ... }: { programs.home-

先到 [Download Page](https://nixos.org/download.html) 下載 Gnome, 64bit 這個 iso，在 macos 上可以用以下指令找出並把 iso image 弄進 USB ```shell $ diskutil list [..] /dev/diskN (external, physical): #: TYPE NAME SIZE IDEN

- 拿 racket 寫了幾個 nanopass 跟 compiler 的教學 1. [從 frontend(compiler) 到 nanopass](https://racket-tw.org/post/2020-12-26-frontend-to-nanopass.html) 2. [用 nanopass 做簡單的類型檢查](https://racket-taiwan.org/post/2020-12-18-simple-type-check-with-nanopass.htm

# Lean 4(nightly) ```shell curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh elan default leanprover/lean4:nightly ``` ### Editor - [VSCode](https://github.com/leanprover-community/vscode-lean4) # Idris 2 ```shell br

在 dependent type 裡面，我們可以寫下如 ```racket (data Nat [zero : Nat] [suc : (Nat -> Nat)]) (data Bool [true : Bool] [false : Bool]) (define (Nat-or-Bool [x : Bool]) : Type (match x [true => Nat] [false => Bool])) ``` 這樣的

Racket macro is a powerful and great tool to create a new syntax form for existing language. Most of the time it just works as expected, but sometimes we would meet some subtle bugs from it. I would explain a certain case of this situation, then tel

循序式語意對程式初學者而言其實很不自然，最主要的原因就是因為它的常見實作語言是 C 語言家族，而 C 語言的 assign 符號跟數學的等於是同一個符號(都是 `=`)。當然改個符號就能解決辨識問題，事實上另一個曾經的主流循序式語言家族 Pascal 就採用了 `:=` 符號因此沒有任何問題。但接著我們還是遇到了語意上的問題，我們知道數學上等於是永久的，一但我們指定「`i` 是整數 `1`」，它在接下來的討論之中都會一直是 `1`。然而循序式程式語言裡面「`i` 是整數 `1`」是暫定的，它真

- [無限的力量](https://www.flag.com.tw/books/product/F0916) 這本是我最近看過最好的數學科普書籍 XD，題材是無限與微積分，很好的介紹了微積分的發展與未來 - 如果贏者全拿，我們還剩下什麼 這本書是巷口仔社會學的第三部，由多篇文章組成，每個作者都極力呈現從社會學觀點出發剖析而得的經濟現象解釋與可能性 - 窮忙：我們這樣的世代 努力致富是上一代流傳給我們的常見觀念之一，但如果努力沒有用呢？如果貧窮不是因為不努力呢？ - 失控

Overview 1. what is Subtyping? 2. what is Liskov Substitution Principle? 3. what's the problem? 4. how to solve this mistake of type system ### What is Subtyping? A common misunderstanding is OOP must have **subtyping** and **generic** at the sam

- 拿 racket 寫了 [raytracer](https://github.com/dannypsnl/raytracer) - 加了 Version Control Panel 跟 REPL 到 [sauron](https://github.com/racket-tw/sauron) 裡 - [inductive](https://github.com/dannypsnl/inductive) 實驗失敗([incr](https://github.com/dannypsnl/incr

我發現真正重要的內容通常需要長時間修改、反覆拿出來閱讀，所以目前的形式越來越不適合。因此以後 blog 這邊會逐漸廢人化，只有無聊透頂的技術相關或是日常才會發這裡 www。舉例： ```racket (define-syntax-rule (comment ...) (void)) ``` 這在 **racket** 裡定義了一個什麼也不會做的語法，可以充當註釋 ```racket (comment give me money QAQ) ```

First we have UTLC(untyped lambda calculus) to STLC(simply typed lambda calculus), by adding arrow type($\to$): $\lambda x:Nat.x$ ### Lambda cube Lambda cube starts from STLC. #### STLC -> $\lambda 2$ Terms depend on Types: $\lambda (a : *).\lam

scribble is a useful tool to create nice documents, however, with Chinese(any unicode character) it might produce some weird empty box for them. To solve this problem we need to create `style.tex`. ```latex % style.tex \usepackage{fontspec} \setmai

In **Racket**, we know using form(`...` represents ignore) ```racket (define (helper) ...) (define (procedure) (helper) ...) ``` is better than form ```racket (define (procedure) (define (helper) ...) (helper) ...) ``` However, t

Quickly note some Coq. ```coq Theorem plus_0_n : forall n:nat, 0 + n = n. Proof. intros n. simpl. reflexivity. Qed. ``` - `intros` introduces variable from environment, here introduce bound `n` from `forall`. - `simpl` would try to reduce both s

Counting is a useful skill, we count in many places, money, cars, weight. We develop awesome ways to count number by hands, if we mark thumb as t, index as i, middle as m, ring as r, little as l, then in Taiwan people counting as the following mappi

Tape `julia` in shell, after getting into the interactive environment of [Julia](https://julialang.org/), tape `]` to get into pkg mode: ``` _ _ _ _(_)_ | Documentation: https://docs.julialang.org (_) | (_) (_)

Compare with [old implementation](/blog/2020-05-24-hindley-milner-system-incremental-build-and-make-new-language/), this version improves by using s-exp to represent type, therefore, can reduce `unify` size a lot. ```racket (define (lookup/type-of

Just record a bad idea www. ```racket (data Point ; constructor-name type* [Point Int Int] (deriving (Eq, Ord))) (data List (a) [nil] [cons a (List a)]) (cons 1 nil) ; infer get a=Int (= absolute (n) (case (< n 0) [#t (- n)]

[framework](https://docs.racket-lang.org/framework/index.html) based on [racket/gui](https://docs.racket-lang.org/gui/) and provides some helpful components. This note is about `editor`, more precisely [racket:text%](https://docs.racket-lang.org/fra

This article is about how to get a fixed point in lambda calculus(utlc) system, if you didn't familiar with it, you can read [NOTE: what is lambda calculus](/blog/2020-01-01-note-what-is-lambda-calculus/) to get started. What's a fixed point? When a

Why? Always a good question, to understand logic programming, need to realize what we gain from it. Normally, if we want to solve a computational problem, we make a sequential command to get an answer. For example, what is Fibonacci's number at `3`?

- Magma: A set equipped with a single binary operation that must be closed by definition. Definition: a set $M$ matched with an operation $*$. magma or closure axiom: $\forall a, b \in M \implies a * b \in M$ - Semigroup: Magma + associativity

優質國度絕對是精彩的超乎預期的小說，甚至無需過多介紹。來看簡介就知道有多棒： > 優質國度知道你會喜歡這本書 > > 超過 630,000 讀者跟你一樣喜歡這本書 > 22 個國家的讀者覺得這本書的內容很好看 > 歡迎來到「優質國度」，地球上最好的國家。 > 在這裡，只要登錄您的「唇紋」， > 演算法就會幫您處理好生活中的所有大小事。 > > 您將可以使用—— > > 【等級評價系統「RateMe」】 > 依據財產、品味、健康指數等項目劃分使用者的等級。 > 高等級的人可以享有例如把紅燈變成

估算演算法的執行時間對寫出有效率的程式非常重要，而基於兩個假設我們採用了量級作為估算方式： 1. 求精確複雜度很難 2. 係數通常不重要 當可以求精確複雜度時，當然應該用更好的工具，並以實驗佐證。 ### 定義 #### O(big O) 給定複雜度函數 f(n)，O(f(n)) 為複雜度函數 g(n) 構成之集合。其中，對任意 g(n)，必存在正實數 c 與非負整數 N，使所有 n ≥ N，g(n) ≤ c × f(n) 這看似很難理解的定義其實在說一件很簡單的事：g(n) 會在

### 材料(一人份) 沒講數量的是因為亂加就好了 - 高麗菜 $\frac{1}{8}$顆 - 培根 2 片 - 油 - 低筋麵粉 4 匙 - 起司粉 - 黑胡椒 - 雞蛋 1 顆 #### 配料 - 肉鬆 - 美乃滋 - 柴魚 ### 流程 1. 把麵粉、蛋加水和成麵糊，打到沒有結塊即可 2. 切碎高麗菜丟進麵糊攪拌 3. 倒一點油，把麵糊到下鍋。把起司、培根放上去，灑黑胡椒 4. 麵皮可以滑動時翻面，接著培根開始發出吱聲就可以起鍋了 5. 加肉鬆、柴魚跟美乃滋

### $\lambda 2$ (Second order typed lambda calculus) Consider **identity function**: $$ \lambda x : nat.x \\ \lambda x : bool.x \\ \lambda x : (nat \to bool).x $$ There are many **identity function**s, one per type, but their definitions are all

ZFC(Zermelo-Fraenkel set theory with the axiom of choice) is an axiomatic system used to formally define set theory. More precisely, ZFC is a collection of approximately 9 axioms, define the core of mathematics through the usage of set theory. Primi

lambda calculus 有所謂的 substitution，具體來說就是 `((lambda (x) x) y)` 會變成 `y`，但正確實作這個行為到底有多麻煩呢?為什麼我寫這篇廢文: 因為我寫錯了... 一切都由簡單的 macro 開始搞，`utlc` 的目標是簡化 term: ```racket (define (utlc t) (match t [`(λ (,x) ,m) `(λ (,x) ,m)] [`(,f ,a) `(,f ,a

我只是寫 continuation 寫一寫非常不滿意，果然先寫個廢文好了，這篇只是一個把 racket 改成 currying 的 macro 說明： ```racket #lang racket (require (for-syntax syntax/parse)) (define-syntax (curry stx) (syntax-parse stx [`((~literal λ) (p) body) #'(λ (p) body)] [`((~

樸素集合論([Naive set theory](https://en.wikipedia.org/wiki/Naive_set_theory))只有兩條公理： - 外延公理(axiom of extensionality)：給定兩集合 $A, B$，若 $\forall x, x \in A, x \in B$，$A = B$ - 概括公理(axiom of unrestricted comprehension)：對任何描述 $x$ 的 $\varphi (x)$，存在集合 $S$ 使 $

Hindley-Milner (HM) type system is a classical type system for lambda calculus with parametric polymorphism. Its most notable property is it can infer most types of a given program, **without type annotations**! However, this feature sounds cool but

At the beginning of learning PLT, everyone could be confused by program that didn't have a variable! Will, I mean they didn't use `String`, `Text` or something like that to define a variable. A direct mapping definition of **lambda calculus**(a.k.a.

很久以前就曾經想過要不要寫下這種經驗文，這念頭出現到現在轉眼就過了兩年了 XD。期間真的發生了太多事，現在又到了人生的十字路口所以決定記錄一些東西，希望這篇文章或許能夠啟發一些像我一樣迷惘的人。 ### 大學教育 我接觸程式的時間不是特別早，到了大學才第一次"使用"電腦。那時真的蠻好笑的，我選了這裡的原因是因為我覺得這系名好長好有趣就填在指考志願第一個位置(而我當時也沒有試圖弄懂志願序的用途 XD)，亂填的下場就是我爸差點沒氣死。當時幾經考慮，然而最後我還是決定不重考了。因為前進後或許不是

演算法時間複雜度分析：對每個不同的輸入大小，其基本運算所執行的次數 ### 所有情況時間複雜度 $T(n)$ - 有些情況下基本運算執行次數與輸入大小以及輸入皆有關，例如循序搜尋中，目標值位置就會影響實際執行時間：假設目標 $x$ 在第一位，那只需要比較一次；$x$ 不在陣列中就需要比較 $n$ 次 - 但對另一些演算法而言，基本運算執行次數只與輸入大小有關，這時我們稱存在 $T(n)$ ### 最差情況時間複雜度 $W(n)$ 對 $T(n)$ 存在的演算法而言，$W(n) \equ

### 材料 - 筆管麵 - [奶油塊](https://24h.pchome.com.tw/prod/DBAK0Z-A9005Y8J4) - 牛奶 50ml - 鹽 - 開水 - 沙拉油 - 洋蔥 - 蒜 ##### 可選 - 培根 - 蘑菇 ### 流程 #### 1. 備料 1. 切蒜碎 2. 切洋蔥絲 #### 2-1. 麵 1. 開水煮沸後加入 2 匙鹽(或是罐裝轉 6 次) 2. 計時 12 分鐘，放入筆管麵，時間到關火 #### 2-2. 白醬(煮麵時間約剩 6

A long long time ago, we found natural numbers can be useful in our life, and some of them seem special. These numbers' multiplication can be a unique identifier for a certain number. We called them: **prime**. A **prime** has two factors: $1$ and i

Writing parser is a boring and massive job, therefore, people create many ways like parser generators to reduce costs. One of them called parser combinator, parser combinator solves two problems: 1. didn't massive as the hand-crafted parser, 2. didn

在[上一篇](/blog/2019-11-09-abstraction-of-programming-design/)教學裡我們只花費了心思在如何建立核心概念的程式上，然而寫好地程式碼沒有讓人操作的介面也就只是一團垃圾而已，這次我們就來看看怎麼樣逐步開發操作用的介面吧！ **Racket** 本身就提供了相當方便的內建 GUI，而這次我們就是要使用這些 API，首先我們來打造單一帳戶的操作介面 ### 宣告式語言 racket/gui ```racket #lang racket/gui

WARNING: This should no longer work, refer to https://hydra.nixos.org/build/119559243/download/1/manual/#sect-macos-installation Since MacOS Catalina adds some new rules, root path cannot be used by applicatin now, caused Nix package manager cannot

There are some trap when using **class** in C++. One of them is the initialization order of members. This can be annoying, therefore, I want to record this: **Declare order would affect initialization order for C++ class members**. For example: ```

Last time we introduce [Functor](/blog/2019-12-13-from-infinite-type-to-functor/), a [Functor](/blog/2019-12-13-from-infinite-type-to-functor/) is a container which provide a function can help another function operating the [Functor](/blog/2019-12-1

### Seven Bridges of Königsberg The seven bridges of Königsberg is a notable problem in mathematics. The following picture shows the actual layer of the seven bridges.  And we can use a graph vers

大約是在去年 8 月左右我在書店發現了[天防者](https://www1.oeya.com.tw/2ejMI?uid1=blog)第一集，身為布蘭登．山德森的腦粉，怎麼能夠錯過大大的新書呢？ 當下就買了英文版回來閱讀，不過當時公司相當忙碌也就只看了一兩章就放到一旁。過了一陣子「又」看到中文版的出現，看著封面設計這麼讚，當即也買下了它(敗書真的很棒 www)。 過了幾天就出國前往日本(還不知道什麼時候才能再去 QQ)，也在行李中放入了[天防者](https://www1.oeya.com.tw

$$\mathbb{Z}$$ contains positive and negative numbers, but nowdays Computer system based on binary. There only have `0` and `1` can be used. A simple solution is: **put signed symbol at the most significant bit**. For example, use 8 bits can represe

Last time I introduce [lambda calculus](/blog/2020-01-01-note-what-is-lambda-calculus/). Lambda calculus is powerful enough for computation. But it's not good enough for people, compare with below **Church Numerals** $$ add := \lambda m. \lambda n.

A few days ago, I post this [answer](https://dev.to/dannypsnl/comment/ldl8) to respond to a question about Racket's web framework. When researching on which frameworks could be used. I found no frameworks make get values from HTTP request easier. So

一如標題這篇是介紹程式語言的文章，比較特殊的是分類語言的方式主要是以能學到什麼觀念為重點。因此我不會去比較它們的範式(如 OOP, FP)或是語法的差別。另外順序跟重要度無關，每個數字標示的都是我推薦去嘗試看看的語言，而其中如果列出多個則代表擇一即可 我第一個推薦的類型是 Scheme/[Racket](https://racket-lang.org/)，Racket 是 Scheme 的平台跟語言變種，但就我目前所知應該沒什麼差異所以我就歸類為同一個語言了。這門語言的特點是一如所有 Lis

晚上跟老同學出去吃飯之後去買 sim 卡(對方要出國)，我們又想說好像沒試過 goshare 不然試看看啊，於是在捷運上開始弄 app：掃描文件跟臉部完成手續！不試還好，一試就變成現在這篇文章的內容啦 www 一開始的 goshare 地圖偏了一條街，我們找了一陣子才發現畫面上的車在外面大街的對面那一側(還要兩個眼鏡仔發揮視力確認車牌)。好吧，小誤差可以接受。到了車邊一看按鈕超多，還好我同學知道怎麼開車廂，其中一個安全帽不知道是不是上一個使用者不知道怎麼解開，扣環上的繩子直接被拆下來 XD。

Optional type `std::optional<T>` was introduced since C++17, we could include header `<optional>` to have it. I supply a few examples to explain this good abstraction. A little step: ```cpp std::optional<int> i{1}; if (i) { std::cout << i.value(

> Satisfiability Modulo Theories(SMT) problem is a decision problem for logical formulas with respect to combinations of background theories such as arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is an efficient SMT solver with spe

Bounded polymorphism refers to existential quantifiers($$\exists$$), restricted to range over types of bound type. To understand it only needs a few examples. Let's start! Take a look at the following program: ```haskell numSort :: Num a => [a] ->

一如標題這是我最後一次去寫對 Go 的公開抱怨，而這不是因為我終於能夠接受它了，而是對其設計與文化感到徹底的失望。有些人可能知道我對這門語言曾經抱持的過度熱愛，我甚至寫過數個盡情發揮 meta programming 技巧的程式庫與多篇包含模式、concurrency、測試等等的介紹文章。當時我缺乏對語言設計的認識，可以說是抱持對 Google 的憧憬(而這當然也已經不存在了)、對語法與創造者們的宣言而對它抱持信心，在現在來看是可笑的。在這裏我先說結論，我不會再抱怨 Go 並不是拒絕使用它，已

For me, programming was about how to map my mind to the world; from this view, it probably shows why I tend to use statically typed language. A strong model could ensure more people won't misunderstand our purpose. This article was going to show som

For the decade, people like to say TDD can solve problems faster, and I'm going to claim this was not the truth. We could solve the problem was because we knew the solution. TDD was good, but no silver bullet. We could say that TDD helping us find o

- Chapter 20: This Class Is Too Big and I Don’t Want It to Get Any Bigger - Chapter 21: I’m Changing the Same Code All Over the Place - Chapter 22: I Need to Change a Monster Method and I Can’t Write Tests for It - Chapter 23: How Do I Know That I’m

At [ch6-10](/blog/2019-12-07-reflection-on-working-effectively-with-legacy-code-ch-6-10/) we know why adding test is so hard, and how to get over it. As usual, we overview what is going to be mentioned in this article: - Chapter 11: I Need to Make

What is lambda-calculus? Or, more specific, what is untyped/pure lambda-calculus? To answer this, I wrote the note for myself. Lambda-calculus was a formal system invented by Alonzo Church in the 1920s, and we can enrich it in a variety of ways, for

From 1972, **C** became more and more important in the underlying world. Many projects are based on **C**, including the famous operating system: **Linux**; the multi-platform toolkit for creating GUI: GTK; "your friend": Ruby and many others great

This week our company wants to improve one of our projects which is based on Istio, exchanging weight in different checker instances, make the traffic distribution fairer. My co-worker provides a nice idea: We watching Pods by the [label selector](h

Before you start to read, ensure you're using Cabal >= 3.0 to manage your project. For a **Haskell** project, I usually use Cabal, do not have any special reason. In the `xxx.cabal` file, we can define some common dependencies by `common` block: `

At [infinite type](/blog/2019-12-08-infinite-type/) I mention a way(recursive abstract data type) to make we use `Option[T]` just like `T`. However, such modeling is not enough. Consider the following example(with the same pseudo syntax takes from [

First, we can make in cluster config became more evident. ```rust let cfg = Config::InCluster // or let cfg = Config::Path("~/.kube/config") let cluster = kube::attach_cluster(cfg); ``` Then we can mix get/list by providing type parameters: ```ru

**Haskell** resource is a little bit outdated and if you take a look at [https://www.haskell.org/documentation/](https://www.haskell.org/documentation/) you would found there are several tutorials, make choose one be a hard thing. So I decide to mak

Infinite type sounds not good since we have no idea how much space would it take. Consider this: ```haskell Prelude> let x = Nothing Prelude> let x = Just x <interactive>:2:9: error: • Occurs check: cannot construct the infinite type: a ~ Mayb

At [part I](/blog/2019-11-24-reflection-on-working-effectively-with-legacy-code-part-one/) we basically understand why we need to test, how to test legacy code and what tools can we use. Chapter 6 to 10 mentions more practicing issues that would fac

[Mergeable replicated data types](http://kcsrk.info/papers/oopsla19-mrdt.pdf) Kaki et al., OOPSLA’19 First, we need to know the context we need mergeable replicated data types(MRDT). In the introduction the authors mention: > Modern distributed da

Preface author defines: what is legacy code? The code which lack of tests. Keep going on, at chapter 1 author compares reasons we update the code. 1. New Feature 2. Fix Bug 3. Refactor 4. Optimize | | Feature | Bug | Refactor | Opt

I have a long time thought that algebra data type(ADT) is must need. In `Haskell`, ADT looks like this: ```haskell data Term = Variable String | Lambda String Term | Application Term Term ``` And let's see how to do the same thing in `Scala

這是一篇重看 2017 年發的系列文 (這裡是第一篇 [routedan.blogspot.com/2017/02/atm-ps.html](https://routedan.blogspot.com/2017/02/atm-ps.html)) 之後決定重寫的文章 之所以決定重來，是因為以現在我的角度來看，當初寫得太過 Java Spec，並且設計流程相當的缺乏建構領域模型的概念 針對第一點，我決定用 Scheme 作為開發語言，來讓讀者理解程式語言並非重點所在，深入學習語言的特殊技巧確實

So what's wrong with me, write down an article for `.gitignore`. Because this [answer](https://stackoverflow.com/a/58758400/6789898) makes me reconsider how to use `.gitignore`. The answer tell us it have a better name: `.git-do-not-complain-about-

Consider the following program: ```go type AState uint8 const ( S1 AState = iota S2 S3 ) ``` This is quite usual in Go. But we want to make it more expressive. So we have: ```go func (s *AState) ToS1() { *s = S1 } func (s *AState) ToS2() { *s

After compiling DPDK, load module and start our process. A common problem is we have no idea where is the NIC going :). And DPDK actually provides some tools for these operations, one of them is `dpdk-devbind.py`. It located at `$(DPDK_PROJECT)/use

Last week I'm trying to reproduce a bug happened in our customer environment, so we create a minimal example for this: https://github.com/glasnostic/nff_go_test During this, I found an annoying problem and want to record it. I got an error: `EAL:

I believe no one likes a big script, and I don’t like it either. A big script means a buggy script. A big script can cause no one can understand it. For example, a command `apt-get install x` stands for what? When it in a thousand lines script?

This article is created as a record of the feedback of the usage of nix, also stand for learning how to use nix in daily developing life. Remember I would not dig into the implementation or model concept inside of nix but all about how to use it to

Just a record. At most of time, if we want to get into a node of kubernetes cluster, we can just using `ssh`. Or we would have a master node has public IP, then we first access the master than access workers to debug. However, in some environments

This week, I have to upgrade nff-go from v0.7.0 to v0.8.1, so I change the version first. However, I found the whole package `nff-go/low` move to `nff-go/internal/low`, and our code directly based on `low`. After some research, I found all I need is

### Get start This article is the note and thought I get from the conference. I would mention the following topics: - type checker for Ruby(steep) - GC compaction ### type checking for Ruby #### Ruby 3 Basically, I understand what Matz(creator

In my case, I have a trait called `Resource` for deserialize from bytes. Now I want to reuse a struct called `List` for others `Resource` so I write done: ```rust struct List<T> { // ignore others field items: Vec<T>, } impl<T: Resource> R

tcpdump? A command line tool for analyzing network packets. How to get packets? Using `-i` option, `tcpdump -i <device-name>`, you would get the packet through NIC(network interface card) named <device-name>.</device-name> How to get `<device-na

Sample code is quite easy: ```go type Car interface { impl() Car Move() } type Animal interface { impl() Animal Walk() } ``` Now, let’s create a structure type: ```go type Duck struct { Animal } ``` Now, if you add `func (d *Duck) Move()`,

There is a saying: > I never had a slice of bread particularly large and wide that did not fall upon the floor and always on the buttered side Even I already work with Go for almost 3 years, I still made these stupid bugs. But learning from errors

Kubernetes was built to run distributed systems on a cluster of nodes. Understanding the concept of kubernetes networking could help you correctly understanding how to run, monitor and trouble shooting your applications on kubernetes, even more you

## What is Huge Page? When a process using some memory, CPU marking the RAM used by the process. For efficiently, CPU allocate by chunks by 4K bytes(default on many platforms). Those chunks called pages. Since process address space is virtual, CPU

We usually have to transfer files between two computers, such as config, log, image. There are a lot of tools that could do it, but if we only know one approach, we would have trouble quickly, so I'm going to show you five tools relate to the topic.

A few weeks ago, we re-discuss the config setup issue; we found generating a new, valid config is too hard for anyone. You must remember all the field, what we need at this time, some duplicate, some would change by the environment, all the stuff be

> Just a note Hash map is a data structure that helps you associate a key type to a value type. For example, a string map to the boolean value. I choose an easy way to create one, that's an array to a list. The type definition was: ```go type Nod

Seriously, I'm not a big fan of the debugger since I never have a try at before. But this time I take a few hours to work with it and the experience is amazed. The debugger provides a way to peeking all stuff inside the program by different input, a

Back to 2016, I learned [googletest](https://github.com/google/googletest) how improving my C++ project. From that, I always want to know how it. Let's take a look at some basic example of it. ```cpp TEST(Arithmetic, Integer) { ASSERT_EQ(1 + 2,

### 基本前提 所有有理數皆可表示為兩個整數的比值，形如 $\frac{p}{q}$ ，而無理數就是不能的那些，但是這個定義太含糊了，以至於許多年來數學家不願承認無理數是數字 用 $\frac{p}{q}$ 就能輕鬆證明 $\sqrt{2}$ 不是有理數，這裡就不贅述 有理數有兩個性質 - 稠密性(任意兩個有理數之間必然有無窮多個有理數) - 不完備性(任意兩個有理數之間必然有無窮多個無理數，故而不能構成連續性，即不完備) ### 戴德金分割 戴德金分割定義了一種形式，即我們可以在

Whole thing is started from **Ingress** this feature of **Kubernetes**. But today I'm not going to talk too much about it, basically just I have to let **Ingress Controller** will send packets to our **Router** so that we could do the thing we want,

Although the article is for Go, but you still can use concept part for others language. Frist we create a script called `bench_compare.sh`: ```bash if [ "${TRAVIS_PULL_REQUEST_BRANCH:-$TRAVIS_BRANCH}" != "master" ]; then REMOTE_URL="$(git config

A typical problem is someone, maybe your friend, your teacher, your co-worker, tell you that you must learn the freshest, incredible new XXX. Nobody cares what's that. The problem is, what they suggest might not be what you need. So the funny things

## Before you beginning You should already install `kubectl` this command line tool. And knowing what is Kubernetes. Knowing why we need to separate the environment for the different member. ## Config for demo At first, we need to prepare a confi

Recently we are working on a new feature is about filter packets by HTTP header for our router. This is the concept, we read the header by rules, rules are just some key/value pair. If key missing or value isn't matched, then we drop the packet. Wh

What is XDP? XDP is eXpress Data Path, it's a technology about putting a BPF code virtual machine on the NIC(network interface controller) driver before kernel network stack so that we can filter the packet before kernel, it would make processing sp

Just list some testing way in Go. Basically we use `testing` this built-in lib to testing To start your first test with Go is an easy task. Example(we would test the following function under directory `add`) ```go package add func Add(x, y int)

> 欲閱讀本篇文章至少需要知道何為 container，由於範例將採用 Docker 為例，所以也預設讀者已經具備操作 Docker 的能力；且讀過 kubernetes 的[基礎概念](https://kubernetes.io/docs/concepts/)只是還沒開始用而已 Kubernetes 最小部署的單位為 Pod，一個 Pod 是 1 至 N 個 container 的群組，它們共享了網路(Network)和儲存空間(Storage) 這麼設計的好處之一是某些本來就耦合的比較

Basically, the problem is because I use Go binding of LLVM, then it hard to use preinstalled LLVM. This article is about how I solve the problem step by step. First we need to install dependencies by apt-get(travis use ubuntu 14.04 if you do not s

I am going to show you enough knowledge to getting start with Go. Are you ready? ## Variables In Go, we have `const`, `var` & short declaration & definition. In top scope of Go program(out of function) ```go const C = "constant" var V = "var"

Use builtin functionality to test a Go server is a panicful experience. The problem is because we have to handle too many error and get so much thing we aren't always need. Of course, we will create a abstraction to reduce this panic. But if we alr

Mark-Sweep is a classic GC algorithm, it's combined with two parts, `mark` and `sweep`. Mark pseudo code would like: ``` mark(root): if !root.is_marked: root.is_marked = true for obj in root.knowns: mark(obj) ``` And Sweep

What is RPC? RPC means "remote procedure call". The concept is call remote function as local function. Then gRPC? It is a framework that help you create RPC. Traditional RPC has some problem make it hard to use. For example, how do you know, what

I have to create a checker for our DNS server. Our DNS server will return it's config via `TXT`. Code would like: ```go package main import "github.com/miekg/dns" // func main m := dns.Msg{} // `google.com.` is correct format, `.` is required!

Do you know what can Go's package `reflect` do? Whatever you had use it or not. Understanding it is not a bad thing. A well known thing is Go don't have generic, I'm not going to tell you we have generic, I'm going to tell you some basic trick to

A few days ago, I release the redux-go v2.1. The purpose is: create reducer & action then manage relationships between them is pretty hard! Let's start from basic v2 store. ```go // package reducer func Counter(state int, action string) int { s

I think most Gopher had read [error-handling-and-go](https://blog.golang.org/error-handling-and-go). Has anyone had watched [Go Lift](https://www.youtube.com/watch?v=1B71SL6Y0kA)? Let's getting start from **Go Lift**! The point of **Go Lift** is: Er

Rust is a strange language. ## Moving First point is move semantic. ```rust fn main() { let s = "hello".to_string(); let t = s; let u = s; } ``` What do you expect? `t` & `u` is `s`? No! `rustc` says: ``` error[E0382]: use of moved

Redux is a single flow state manager. I porting it from JS to Go at last year. However, there had one thing make me can't familiar with it, that is type of state! In Redux, we have store combined by many reducers. Then we dispatch action into store

Although title contains Ruby, but I won't talk too much on it, because I did not learn it. This conf is my first conf. I learn something at here, and I will write down in following text. The first impress talk is using Elixir & Kafka write a server

> 閱讀此篇之前，我假設讀者已具備 `Go` 知識，一點 CS 常識，和一些讓子彈飛的技巧(師爺？師爺？) 說起 `Go` 的 `channel`，要從[CSP](http://www.usingcsp.com/cspbook.pdf)(Communicating Sequential Process)模型說起 在電腦科學中，CSP 是一種形式語言，描述非同步系統中各種[interaction](https://en.wikipedia.org/wiki/Interaction)的模式

這篇只是隨便紀錄一下好不容易終於弄懂的 Nginx ，首先各個平台安裝方式應該直接上網查詢 [官網下載頁](https://www.nginx.com/resources/wiki/start/topics/tutorials/install/) 最基本的啟動方式通常是 `/usr/bin/nginx` ，不過各平台可能有差異，應以實際位置為主 ## 指令 ```bash $ nginx -s stop # shut down nginx $ nginx -s reload # rel

這幾天好不容易有機會試玩 Elixir 的神奇框架 Phoenix 首先要用 mix 下載 phoenix ```bash $ mix archive.install https://github.com/phoenixframework/archives/raw/master/phx_new.ez ``` 另外也需要 node, npm 等相依 預設使用 postgreSQL 作為資料庫 Phoenix 與 Rails 相同，都是由框架為你產生基礎模板的設計，指令如下： ```b

Go 的測試有一個很討厭的行為，那就是 test caching，它會儲存測試的結果然後導致失敗沒有被發覺 如果你的 Go 版本是 1.9，你可以嘗試用`go test -count=1`命令執行測試 `-count=1`參數會取消 test caching 你還有其他選擇，例如`GOCACHE=off go test`，這也會取消 test caching 期望這個問題可以很快得到解決

說到 Lexer 技術，大家應該都會想到正規表達式，但是為什麼是正規表達式呢？ 所以我們要介紹整個掃描並辨識字詞的技術與原理 最簡單的辨識單字技術是大家都能直接想出來的方法，就是 character-by-character 演算法 其技術原理非常簡潔，如果要辨識 `new`，我們會怎麼做呢？ ```racket (define (new? s) (define cs (string->list s)) (if (< (length cs) 3) #f (

If you had written any concurrency code in Go, I think you could seem `sync.WaitGroup` before. Today's we will focus on create a wait group by channel trick. How? First, you need a channel without buffer. ```go func main() { wait := make(chan

Sort is an operation very often to use. Although a `quick-sort` isn't too long. We still don't want to create it again and again. It also doesn't have the value to copy it. Good news is standard package `sort` provide a lots of sort function. Unlik

## How to implement singleton in Go? It's really a problem at there. And worth to think about it. ### Start Let's consider how to create a singleton? We need a reference can't be change by anyone at all the time except initialize. Is that possibl

`this` scope rule is one of the hardest problem in JS. Let's start it. ```js function print() { console.log(this.data) } let obj = { data: "This is obj", print, } obj.print() // Output: This is obj // It's good. But if we send print to other

## Install(Unix Like system) ### ffmpeg [Download Page](https://www.ffmpeg.org/download.html) ```bash $ ./configure --enable-shared $ make $ sudo make install ``` ### OpenCV [Download Page](https://opencv.org/releases.html) ```bash $ mkdir rel

那麼今天就來介紹說很久但是一直沒有寫的 Erlang 吧! Erlang 是一隻很有趣的語言，它絕對跟你看過的主流語言有巨大的差異，無論是語法上還是思想上皆是如此 首先我們需要安裝環境，請參考官方的 Downloads 接著我們就從 erl 開始吧 ```bash $ erl ``` 輸入指令啟動 Erlang 的互動環境 你可以先嘗試輸入 ```erlang 1> X=0. 0 2> X=1. ** exception error: no match of right hand

Let's start from some code. And seems will be only code in this article. ```cpp // Compile: clang++ main.cc #include <iostream> template <int x, int y> class Matrix { // We don't care how to implement at here public: std::string print() { retu

Use command<br> `$ go get -d llvm.org/llvm/bindings/go/llvm`<br> to get llvm project Then<br> `$ cd $GOPATH/src/llvm.org/llvm/bindings/go/llvm` Then `$ mkdir workdir && cd workdir && mkdir llvm_build` Then go back to dir go/llvm `$ ./build.s

在 Vim 中 找出文字並修改不是一件複雜的事 你只需要 `:Start, Ends/You want to replace/You want to get/g` `:`是進入命令模式 `Start`和`End`都是行號的代號，你可以用數字 1, 2, 3... 也可以是特殊字元，例如\$是最後一行 接著`s///g`是取代命令，`s/你想取代的/你想顯示的新字串/g` 字串使用正規語言進行比對 例如： ```bash [a-zA-Z]+ \".*?\" ```

好吧，上一篇說了這麼多，其實幾乎就只是把屬性定義在類別外罷了，沒什麼啊 這樣並沒有比`class`強到哪裡 所以，讓我們來看看`extension hacks`吧！ ## hack 1: > extension from a temporary protocol ```swift protocol MenuItem {} extension label : MenuItem {} extension button : MenuItem {} var list = [MenuItem

雖然 apple 在 `extension` 的文件中註記了 > NOTE<br> > If you define an extension to add new functionality to an existing type, the new functionality will be available on all existing instances of that type, even if they were created before the extension was

今天我想介紹一個強大有趣的工具--ANTLR 這個工具根據我們定義的文法產生處理原始碼的 parser，當然不只是處理程式語言，你也可以用來處理其他資料 ## 安裝 ```bash cd /usr/local/lib sudo curl -O http://www.antlr.org/download/antlr-4.7-complete.jar export CLASSPATH=".:/usr/local/lib/antlr-4.7-complete.jar:$CLASSPATH" a

因為 Elz 實在是一個遠超我一開始的預想的語言(最開始只是想了解編譯器，乾脆就開始設計新語言了) 打造花了我很多心思，Elz 採用先從原始碼中取得詞素，再分析詞素的設計 這樣一來兩邊都可以降低實作的複雜度 分成`lexer`與`parser`兩大主軸工作之後，考慮到效能，我沒有採用 lex 這種吸引人的作法(其實一開始是有試過，最重要的問題是我覺得學那個好麻煩 XD) 而是手刻這個部分，其中最重要的設計就是利用`Golang`的共時技巧，讓`parser`可以不用等待`lexer`的

### 基本的 thread 建立 標準庫的 thread 非常容易存取 ```cpp #include <thread> #include <iostream> using std::cout; void hello() { cout << "hello" << '\n'; } int main() { std::thread t(hello); t.join(); } ``` 1. 引入`thread`標頭檔 2. 宣告函式 3. 建構一個`thread