Dan's
Blog

Programming Language Theory • System Programming

119 Posts

NOTE: Lambda Cube

1 min read • 2020-09-17

First we have UTLC(untyped lambda calculus) to STLC(simply typed lambda calculus), by adding arrow type(): Lambda cube Lambda cube starts…

NOTE: scribble and xelatex

1 min read • 2020-09-01

scribble is a useful tool to create nice documents, however, with Chinese(any unicode character) it might produce some weird empty box for…

[racket macro] define/where

1 min read • 2020-08-23

In Racket, we know using form( represents ignore) is better than form However, the benefit of defining helper in target procedure can be see…

NOTE: Coq tactics

2 min read • 2020-08-19

Quickly note some Coq. introduces variable from environment, here introduce bound from . would try to reduce both sides of equation, in…

NOTE: how to setup a julia project

1 min read • 2020-08-07

Tape in shell, after getting into the interactive environment of Julia, tape to get into pkg mode: In this mode tape: In the current…

Infinite, how big?

3 min read • 2020-08-07

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…

NOTE: represent type by s-exp when doing inference

1 min read • 2020-08-01

Compare with old implementation, this version improves by using s-exp to represent type, therefore, can reduce size a lot.

NOTE: Bad Idea, put Haskell in S expression?

1 min read • 2020-07-31

Just record a bad idea www. The major challenge would be can be repeated. Therefore, have to record each binding and convert to a pattern…

NOTE: Racket GUI framework and editor component

1 min read • 2020-07-30

framework based on racket/gui and provides some helpful components. This note is about , more precisely racket:text%. Whole GUI system based…

How to find mk fixed point

3 min read • 2020-07-26

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…

Why Logic Programming?

1 min read • 2020-07-15

Why? Always a good question, to understand logic programming, need to realize what we gain from it. Normally, if we want to solve a…

NOTE: Algebra Structure

1 min read • 2020-07-12

Magma: A set equipped with a single binary operation that must be closed by definition. Definition: a set matched with an operation . magma…

小說推薦:優質國度

1 min read • 2020-07-03

優質國度絕對是精彩的超乎預期的小說,甚至無需過多介紹。來看簡介就知道有多棒: 優質國度知道你會喜歡這本書 超過 630,000 讀者跟你一樣喜歡這本書 2…

NOTE: 演算法的量級

2 min read • 2020-06-20

估算演算法的執行時間對寫出有效率的程式非常重要,而基於兩個假設我們採用了量級作為估算方式: 求精確複雜度很難 係數通常不重要 當可以求精確複雜度時,當然應該用更好的工具,並以實驗佐證。 定義 O(big O) 給定複雜度函數 f(n),O(f(n)) 為複雜度函數 g(n…

大阪燒

1 min read • 2020-06-17

材料(一人份) 沒講數量的是因為亂加就好了 高麗菜 顆 培根 2 片 油 低筋麵粉 4 匙 起司粉 黑胡椒 雞蛋…

NOTE: lambda 2

1 min read • 2020-06-12

(Second order typed lambda calculus) Consider identity function: There are many identity functions, one per type, but their definitions are…

NOTE: ZFC

2 min read • 2020-06-11

ZFC(Zermelo-Fraenkel set theory with the axiom of choice) is an axiomatic system used to formally define set theory. More precisely, ZFC is…

正確實作 substitution 有多難

2 min read • 2020-06-04

lambda calculus 有所謂的 substitution,具體來說就是 會變成 ,但正確實作這個行為到底有多麻煩呢?為什麼我寫這篇廢文: 因為我寫錯了... 一切都由簡單的 macro 開始搞, 的目標是簡化 term…

NOTE: 樸素集合論三大悖論

3 min read • 2020-05-31

樸素集合論(Naive set theory)只有兩條公理: 外延公理(axiom of extensionality):給定兩集合 ,若 , 概括公理(axiom of unrestricted comprehension…

Currying

1 min read • 2020-05-31

我只是寫 continuation 寫一寫非常不滿意,果然先寫個廢文好了,這篇只是一個把 racket 改成 currying 的 macro 說明: 先把 macro 寫好,現在來思考一下所謂 currying 到底做了什麼,簡單來說它就是 λ…

Hindley-Milner type system: Incrementally build way & Make new language in Racket

14 min read • 2020-05-24

Hindley-Milner (HM) type system is a classical type system for lambda calculus with parametric polymorphism. Its most notable property is it…

De Bruijn index: why and how

5 min read • 2020-05-16

At the beginning of learning PLT, everyone would likely be confused by some program that didn't have a variable! Will, I mean they didn't…

Programming 生涯回顧

7 min read • 2020-05-13

很久以前就曾經想過要不要寫下這種經驗文,這念頭出現到現在轉眼就過了兩年了 XD…

NOTE: 演算法的各種時間複雜度

2 min read • 2020-05-12

奶油白醬義大利麵

1 min read • 2020-05-10

材料 筆管麵 奶油塊 牛奶 50ml 鹽 開水 沙拉油 洋蔥 蒜 可選 培根 蘑菇 流程 1. 備料 切蒜碎 切洋蔥絲 2-1. 麵 開水煮沸後加入 2 匙鹽(或是罐裝轉 6 次) 計時 12 分鐘,放入筆管麵,時間到關火 2-2. 白醬(煮麵時間約剩…

A beautiful proof: There have infinite primes

1 min read • 2020-05-09

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…

How to parse expression with the parser combinator

3 min read • 2020-05-03

Writing parser is a boring and massive job, therefore, people create many ways like parser generators to reduce costs. One of them called…

程式設計思考(二)操作介面

6 min read • 2020-04-25

在上一篇教學裡我們只花費了心思在如何建立核心概念的程式上,然而寫好地程式碼沒有讓人操作的介面也就只是一團垃圾而已,這次我們就來看看怎麼樣逐步開發操作用的介面吧! Racket 本身就提供了相當方便的內建 GUI,而這次我們就是要使用這些 API…

NOTE: how to install Nix package manager on MacOS Catalina

1 min read • 2020-04-17

Since MacOS Catalina adds some new rules, root path cannot be used by applicatin now, caused Nix package manager cannot work! The problem is…

NOTE: class member initialization order in C++

1 min read • 2020-04-13

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…

From Functor to Applicative

3 min read • 2020-04-11

Last time we introduce Functor, a Functor is a container which provide a function can help another function operating the Functor. This…

NOTE: Seven Bridges of Königsberg and Eulerian graph

1 min read • 2020-04-03

Seven Bridges of Königsberg The seven bridges of Königsberg is a notable problem in mathematics. The following picture shows the actual…

小說推薦:天防者

2 min read • 2020-04-01

大約是在去年 8 月左右我在書店發現了天防者第一集,身為布蘭登.山德森的腦粉,怎麼能夠錯過大大的新書呢? 當下就買了英文版回來閱讀,不過當時公司相當忙碌也就只看了一兩章就放到一旁。過了一陣子「又」看到中文版的出現,看著封面設計這麼讚,當即也買下了它(敗書真的很棒 www…

Binary Encoding of Integer

4 min read • 2020-03-21

contains positive and negative numbers, but nowdays Computer system based on binary. There only have and can be used. A simple solution is…

NOTE: simply typed lambda calculus

2 min read • 2020-03-08

Last time I introduce lambda calculus. Lambda calculus is powerful enough for computation. But it's not good enough for people, compare with…

A Racket macro tutorial -- get HTTP parameters easier

6 min read • 2020-02-16

A few days ago, I post this answer to respond to a question about Racket's web framework. When researching on which frameworks could be used…

一些推薦去嘗試看看的程式語言

3 min read • 2020-02-06

一如標題這篇是介紹程式語言的文章,比較特殊的是分類語言的方式主要是以能學到什麼觀念為重點。因此我不會去比較它們的範式(如 OOP, FP…

不會騎 Gogoro 的兩個鄉巴佬

2 min read • 2020-01-31

晚上跟老同學出去吃飯之後去買 sim 卡(對方要出國),我們又想說好像沒試過 goshare 不然試看看啊,於是在捷運上開始弄 app:掃描文件跟臉部完成手續!不試還好,一試就變成現在這篇文章的內容啦 www 一開始的 goshare…

NOTE: C++ optional

1 min read • 2020-01-26

Optional type was introduced since C++17, we could include header to have it. I supply a few examples to explain this good abstraction. A…

NOTE: a little bit Z3 solver

1 min read • 2020-01-24

Satisfiability Modulo Theories(SMT) problem is a decision problem for logical formulas with respect to combinations of background theories…

NOTE: bounded polymorphism

1 min read • 2020-01-24

Bounded polymorphism refers to existential quantifiers(), restricted to range over types of bound type. To understand it only needs a few…

最後一次抱怨 Go

10 min read • 2020-01-19

一如標題這是我最後一次去寫對 Go 的公開抱怨,而這不是因為我終於能夠接受它了,而是對其設計與文化感到徹底的失望。有些人可能知道我對這門語言曾經抱持的過度熱愛,我甚至寫過數個盡情發揮 meta programming 技巧的程式庫與多篇包含模式、concurrency…

Type as Constraint: Why we need more type?

3 min read • 2020-01-16

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…

TDD is not silver bullet

1 min read • 2020-01-11

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…

Reflection on Working effectively with legacy code --- chapter 20 to 23

2 min read • 2020-01-04

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 2…

Reflection on Working effectively with legacy code --- chapter 11 to 19

4 min read • 2020-01-03

At ch6-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…

NOTE: What is lambda calculus

6 min read • 2020-01-01

What is lambda-calculus? Or, more specific, what is untyped/pure lambda-calculus? To answer this, I wrote the note for myself. Lambda…

Interaction with C in Zig

7 min read • 2019-12-22

From 1972, C became more and more important in the underlying world. Many projects are based on C, including the famous operating system…

NOTE: get labels from Pod

2 min read • 2019-12-20

This week our company wants to improve one of our projects which is based on Istio, exchanging weight in different checker instances, make…

How to test in Haskell: HSpec setup

1 min read • 2019-12-14

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…

NOTE: If we write kubernetes client in Rust

1 min read • 2019-12-13

First, we can make in cluster config became more evident. Then we can mix get/list by providing type parameters:

From Infinite Type to Functor

4 min read • 2019-12-13

At infinite type I mention a way(recursive abstract data type) to make we use just like . However, such modeling is not enough. Consider…

Infinite Type

3 min read • 2019-12-08

Infinite type sounds not good since we have no idea how much space would it take. Consider this: At here, the type of was after the first…

Haskell quick start

6 min read • 2019-12-08

Haskell resource is a little bit outdated and if you take a look at https://www.haskell.org/documentation/ you would found there are several…

Reflection on Working effectively with legacy code --- chapter 6 to 10

8 min read • 2019-12-07

At part I 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…

Mergeable replicated data types

4 min read • 2019-11-30

Mergeable replicated data types Kaki et al., OOPSLA’19 First, we need to know the context we need mergeable replicated data types(MRDT). In…

Reflection on Working effectively with legacy code --- Part I

3 min read • 2019-11-24

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…

Algebra data type vs Class

1 min read • 2019-11-19

I have a long time thought that algebra data type(ADT) is must need. In , ADT looks like this: And let's see how to do the same thing in…

程式設計思考(一)核心領域

7 min read • 2019-11-09

這是一篇重看 2017 年發的系列文 (這裡是第一篇 routedan.blogspot.com/2017/02/atm-ps.html) 之後決定重寫的文章 之所以決定重來,是因為以現在我的角度來看,當初寫得太過 Java Spec…

How to use .gitignore

1 min read • 2019-11-08

So what's wrong with me, write down an article for . Because this answer makes me reconsider how to use . The answer tell us it have a…

Weird behavior in Go: encoding/gob

1 min read • 2019-10-31

Consider the following program: This is quite usual in Go. But we want to make it more expressive. So we have: p.s. Replace and others…

DPDK usertools: devbind

1 min read • 2019-10-19

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…

DPDK -- EAL Input/output error

1 min read • 2019-10-18

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…

Why not a big script

1 min read • 2019-10-05

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…

nix report

4 min read • 2019-09-12

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…

Privileged Pod -- Debug kubernetes node

1 min read • 2019-09-01

Just a record. At most of time, if we want to get into a node of kubernetes cluster, we can just using . Or we would have a master node has…

cgo can be a trouble

2 min read • 2019-08-15

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 move to , and…

Notes: Ruby Conf Taiwan 2019

6 min read • 2019-08-13

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…

How trait with lifetime can be a trouble and how to fix it

2 min read • 2019-07-31

In my case, I have a trait called for deserialize from bytes. Now I want to reuse a struct called for others so I write done: Because…

tcpdump cheat sheet

2 min read • 2019-06-25

tcpdump? A command line tool for analyzing network packets. How to get packets? Using option, , you would get the packet through NIC…

A simple way to ensure interface won't be implemented accidently

1 min read • 2019-06-18

Sample code is quite easy: Now, let’s create a structure type: Now, if you add , you won’t be a car accidently! What if you want to embed…

The Go concurrency bug I made

3 min read • 2019-05-25

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…

Kubernetes Networking: concept and overview from underlying perspective

17 min read • 2019-05-18

Kubernetes was built to run distributed systems on a cluster of nodes. Understanding the concept of kubernetes networking could help you…

HugePages on Kubernetes

3 min read • 2019-05-04

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…

5 tools for file transfer

3 min read • 2019-04-27

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…

gRPC proxy: approach & pain

3 min read • 2019-04-13

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…

Write a hashmap in Go

2 min read • 2019-04-04

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…

Introduction of LLDB

3 min read • 2019-03-17

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…

Make googletest-like test framework from scratch

5 min read • 2019-03-03

Back to 2016, I learned googletest how improving my C++ project. From that, I always want to know how it. Let's take a look at some basic…

戴德金分割與1為何等於0.9...(無限循環)

3 min read • 2019-03-01

基本前提 所有有理數皆可表示為兩個整數的比值,形如 ,而無理數就是不能的那些,但是這個定義太含糊了,以至於許多年來數學家不願承認無理數是數字 用 就能輕鬆證明 √…

Tracing source code of Kubernetes client-go

8 min read • 2019-01-25

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…

How to compare Go benchmark in TravisCI

1 min read • 2018-12-28

Although the article is for Go, but you still can use concept part for others language. Frist we create a script called : Then I usually…

Should I learn?

2 min read • 2018-12-22

A typical problem is someone, maybe your friend, your teacher, your co-worker, tell you that you must learn the freshest, incredible new XXX…

Kubernetes context

4 min read • 2018-12-09

Before you beginning You should already install this command line tool. And knowing what is Kubernetes. Knowing why we need to separate the…

XDP some note

3 min read • 2018-11-30

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…

fun networking: tcp close

1 min read • 2018-11-30

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…

Testing in Go

4 min read • 2018-11-17

Just list some testing way in Go. Basically we use this built-in lib to testing To start your first test with Go is an easy task. Example…

Kubernetes 從 Pod 開始

5 min read • 2018-10-27

欲閱讀本篇文章至少需要知道何為 container,由於範例將採用 Docker 為例,所以也預設讀者已經具備操作 Docker 的能力;且讀過 kubernetes 的基礎概念只是還沒開始用而已 Kubernetes 最小部署的單位為 Pod,一個 Pod 是 1 至 N…

Test LLVM Go binding in travis

2 min read • 2018-10-06

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…

Go quick start

4 min read • 2018-09-23

I am going to show you enough knowledge to getting start with Go. Are you ready? Variables In Go, we have , & short declaration…

Use httpexpect to test server

1 min read • 2018-09-16

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…

Mark Sweep GC

1 min read • 2018-09-03

Mark-Sweep is a classic GC algorithm, it's combined with two parts, and . Mark pseudo code would like: And Sweep pseudo code would like…

gRPC quick start in Go

2 min read • 2018-08-16

What is RPC? RPC means "remote procedure call". The concept is call remote function as local function. Then gRPC? It is a framework that…

Practical issue about DNS -- EDNS0

2 min read • 2018-08-07

I have to create a checker for our DNS server. Our DNS server will return it's config via . Code would like: But our config stream is too…

Reflection in Go: create a stack[T]

2 min read • 2018-07-22

Do you know what can Go's package do? Whatever you had use it or not. Understanding it is not a bad thing. A well known thing is Go don't…

Magic in redux-go v2.1: package rematch

7 min read • 2018-07-04

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…

Error is Value

3 min read • 2018-06-22

I think most of Gopher had read error-handling-and-go Has anyone had watched Go Lift? Let's getting start from Go Lift! The point of Go Lift…

How to getting start with Rust

3 min read • 2018-05-26

Rust is a strange language. Let's start! Moving First point is move semantic. What do you expect? & is ? No! says: These error tell you…

Design of Redux-go v2

4 min read • 2018-05-17

Redux is a single flow state manager. I porting it from JS to Go at last year. But there had one thing make me can't familiar with it, that…

Some thinking from Elixir X Ruby Conf

2 min read • 2018-05-01

Hi everyone, I am Danny. Although title contains Ruby, but I won't talk too much on it. Because I did not learn it. This conf is my first…

Go Channels 入門

5 min read • 2018-04-23

閱讀此篇之前,我假設讀者已具備 知識,一點 CS 常識,和一些讓子彈飛的技巧(師爺?師爺?) 說起 的 ,要從CSP(Communicating Sequential Process)模型說起 在電腦科學中,CSP 是一種形式語言,描述非同步系統中各種interaction…

Nginx 安裝與啟動

1 min read • 2018-04-02

這篇只是隨便紀錄一下好不容易終於弄懂的 Nginx ,首先各個平台安裝方式應該直接上網查詢 官網下載頁 最基本的啟動方式通常是 ,不過各平台可能有差異,應以實際位置為主 指令 設定流程 把設定檔放在 下,請根據系統到 Nginx 的設定檔目錄中尋找這個目錄 p.s…

Phoneix 安裝與啟動

1 min read • 2018-03-31

這幾天好不容易有機會試玩 Elixir 的神奇框架 Phoenix 首先要用 mix 下載 phoenix 另外也需要 node, npm 等相依 預設使用 postgreSQL 作為資料庫 Phoenix 與 Rails…

How to disable Go test caching

1 min read • 2018-03-17

Go 的測試有一個很討厭的行為,那就是 test caching,它會儲存測試的結果然後導致失敗沒有被發覺 如果你的 Go 版本是 1.9,你可以嘗試用命令執行測試 參數會取消 test caching 你還有其他選擇,例如,這也會取消 test caching…

Introduction Of Char Recognizing -- Lexer Tech

4 min read • 2018-02-25

此篇使用 Rust 作為演示實際程式碼的語言 說到 Lexer 技術,大家應該都會想到正規表達式,但是為什麼是正規表達式呢? 所以我們要介紹整個掃描並辨識字詞的技術與原理 最簡單的辨識單字技術是大家都能直接想出來的方法,就是 character-by-character…

Create a WaitGroup by yourself

2 min read • 2018-02-15

If you had wrote any concurrency code in Go. I think you could seems before. And today point is focus on create a wait group by channel…

Sort by interface in Go

2 min read • 2018-02-14

Sort is an operation very often to use. Although a isn't too long. We still don't want to create it again and again. It also don't have the…

The best practice of Singleton in Golang

1 min read • 2018-02-12

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…

You should know about `this`

4 min read • 2018-02-09

scope rule is one of hardest problem in JS. Let's start it. Ok! Now we know the true: is dynamic. But! We still need to send us function to…

OpenCV introduction

1 min read • 2018-02-08

Install(Unix Like system) ffmpeg Download Page OpenCV Download Page Introduction Show Image Compile & Run it.

Erlang Quick Start

4 min read • 2018-01-05

那麼今天就來介紹說很久但是一直沒有寫的 Erlang 吧! Erlang 是一隻很有趣的語言,它絕對跟你看過的主流語言有巨大的差異,無論是語法上還是思想上皆是如此 首先我們需要安裝環境,請參考官方的 Downloads 接著我們就從 erl 開始吧 輸入指令啟動 Erlang…

Type driven development in C++

1 min read • 2017-12-23

Let's start from some code. And seems will be only code in this article. Ok, some code be there, why I want to talk about these code? Few…

llvm Go bindings

1 min read • 2017-12-04

Use command to get llvm project Then Then Then go back to dir go/llvm I had installed Ninja, then build script use it to build system. I…

Vim replace

1 min read • 2017-10-24

在 Vim 中 找出文字並修改不是一件複雜的事 你只需要 是進入命令模式 和都是行號的代號,你可以用數字 1, 2,…

Extension hack

4 min read • 2017-09-29

好吧,上一篇說了這麼多,其實幾乎就只是把屬性定義在類別外罷了,沒什麼啊 這樣並沒有比強到哪裡 所以,讓我們來看看吧! hack 1: extension from a temporary protocol…

Swift --extension概念入門

3 min read • 2017-09-29

雖然 apple 在的文件中註記了 NOTE If you define an extension to add new functionality to an existing type, the new functionality will be available on…

ANTLR v4--introduction

3 min read • 2017-09-03

今天我想介紹一個強大有趣的工具--ANTLR 這個工具根據我們定義的文法產生處理原始碼的 parser,當然不只是處理程式語言,你也可以用來處理其他資料 安裝 之後會用到的通常是這支程式 因為它用來產生 parser 開始 我們需要建立一個檔案叫,而裡頭的 grammar…

lexer 原理解釋

3 min read • 2017-07-08

因為 Elz 實在是一個遠超我一開始的預想的語言(最開始只是想了解編譯器,乾脆就開始設計新語言了) 打造花了我很多心思,Elz 採用先從原始碼中取得詞素,再分析詞素的設計 這樣一來兩邊都可以降低實作的複雜度 分成與兩大主軸工作之後,考慮到效能,我沒有採用 lex…

C++ thread 基礎

4 min read • 2017-06-26

使用標準庫的 thread 非常容易 1.引入標頭檔 2.宣告函式 3.建構一個物件…

©2020 dannypsnl(林子篆)