Time for some acknowledgements. First and foremost, I thank Mr. Xie for the interview and various discussions. I thank Mr. Bai for job recommendation. I thank Ms. Chen for the PS. I thank Mr. Han for job recommendation. I thank Mr. Hou for the post which gave me the first job. I thank Mr. Huang for the present. I thank Mr. Li for job recommendation. I thank Mr. Liu for the appreciation and career advice. I thank Mr. Luo for the friendly interview. I thank Ma for teaching me many life tips, among them how to cook. I thank Mr. Qiao for job recommendation. I thank Ms. Qu for job recommendation. I thank Mr. Yang for answering my navie questions. I thank Mr. Zhang for career advice. I thank Ms. Zhang for not beating me to death after all. I thank Mr. Zhu for the treat. I thank various HRs for the arrangement. I thank interviewers for making me believe I am valuable. I thank many other people from whom I sought solace and comfort.

The saddest thing in life is wasted talent, and the choices that you make will shape your life forever. -- A Bronx Tale

Almost finished (TM) reading

Some books are to be tasted, others to be swallowed, and some few to be chewed and digested. -- Bacon

Real World Haskell

This book is bad because it has too few exercises and it is much less fun to walk through. Learn You a Haskell for Great Good! seems to be better-suited for newcomer. I think walking through Typeclassopedia and doing H-99: Ninety-Nine Haskell Problems are much more effective. Though you will not have as comprehensive knowledge on haskell.


I read most of the papers, but didn’t do the projects yet (TM). I want to contribute to some distributed system project like spark, etcd, kubernetes, cassandra and zookeeper. I have spark on my mind as I choose the lesser of 3 evils. Scala is the best among all the rubbishes and spark seems to be cooler.

Reading Distributed Systems by Maarten van Steen is a total waste of time, Designing Data-Intensive Applications seems to be better.

Type-driven development with idris

This book is quite simple if you’re familiar with Haskell. Not because Idris is heavily inspired by Haskell, just because it is simple in itself. Idris has quite a few improvements over Haskell, e.g. first-class types, dependent types, views. But, the best thing of Idris for me is interactive programming (à la proof-assistants?).

Often times, solving a problem is given the signature and some existing functions implementing a function. The relationship of the function to be implemented and the existing functions could be opaque. For example, implement foldMap in terms of foldRight or foldLeft and vice versa. Extra flexibility is added when we can curry and uncurry existing functions. Moreover, I sometimes find it hard to understand what an “abstract” function tries to do. It is especially so when there are too many one-letter symbols whose meanings are not immediately obvious to me, and we do not have different type face for different kinds of data. It is a common practice that Haskellers use the same symbol to denote both type and type elements, sometimes even better, they use the same symbol for a type and an element from different type.

Functional programming gurus can chase diagrams by heart. We mortals deserve better tools like Idris. The case-spliting, goal-like lifting and type inspection can help mortals think clearly, as there ain’t such thing as thinking when it is the only way out.

Introduction to Automata Theory, Languages, and Computation

Best book on computation? This book could be tedious for passive digestors like me. People “in a hurry” should at least try to substitute the theorem constructions with the before-mentioned examples, or it will be hard to follow this book. I did the exercises in early chapters, and failed to be up to par in later chapters.

Structure and Interpretation of Computer Programs.

This book is a tour de force. Seasoned programmers can still learn a lot from this book. It is a pity that I did not finish it in the best of my youth. It could be such an ecstasy. I finished every exercises in chapter 1 a long time ago. Recently I managed to skim through this book in the subway. I find so many recurring themes of computer science in this book. I image a younger me could have learned many things in this book, e.g. standard algorithm tricks like divide-and-conquer, dynamic programming, coding economically with higher order functions like map filter reduce, what Alan Kay meant by object-oriented programming are really just message-passing, evaluation strategies, lazy lists, concurrent programming techniques like lock and channels, event sourcing, how to Program from ground up, an alternative description of how computer works, writing a domain-specific language for database querying, how to simulate nondeterministic Turing machine with deterministic Turing machine.

I am genuinely curious about how the authors think of purely functional programming languages like Haskell, what’s the authors’ opinion on transactional memory.

Failed Attempts

Books I really wanted to finish reading in one shot, but do not have much progress as of today.

  • Lectures on the Curry-Howard Isomorphism
  • Certified Programming with Dependent Types
  • Computer Complexity: A Modern Approach
  • A Graduate Course in Applied Cryptography

Augmented wishlist


  • Homotopy Type Theory: Univalent Foundations of Mathematics

I only have a vague impression of HoTT. These also seem to be decent materials. An introduction to univalent foundations for mathematicians. Introduction to Univalent Foundations of Mathematics with Agda.

  • Type theory

Currently there seems to be no satisfactory type theory book.

  • The Software Foundations series
  • Spark in Action
  • Kubernetes in Action
  • Cassandra: The Definitive Guide
  • A Second Course in Formal Languages and Automata Theory
  • On Concurrent Programming (Texts in Computer Science)
  • Programming Languages: Applications and Interpretation
  • The Implementation of Functional Programming Languages
  • Essentials of Programming Languages


  • zurihac

enrolled, and will not be able to go because of the ill timing, just cancelled the schedule

  • munihac

too late to enroll, currently on the wait list, don’t think I will be able to go as it would be too later when the waillist is shortened



They are several tricks to pipe all traffic through a socks5 proxy. redsocks leverages iptables to redirect traffic, which requires root permission. proxychains uses the LD_PRELOAD for dynamically linked programs. I’d like to use linux namespace and something like tun2socks to transparently redirect traffic for specific programs. This can be done with the help of something like tun2socks. Unfortunately, tun2socks is strongly coupled to other components of badvpn. I want to implement this from ground up with userspace tcp/ip stack like smoltcp.

Classification of Poems

I want to do something like Automatic Mood Classification of Punjabi Poems Using Supervised Approach, and create a tag cloud for all poems.

I can think of several practical usage of such system. First it can be used in naming. A good name with a great connotation for a baby is something what Chinese parents would call a head start in life. Moreover, to baptize a product after poems can make the product stand out. Together with tag cloud, trademark registration status querying and username availiability check (e.g. namecheckr), it can be of tremendous importance for startups to build a solid brand. It would also be every writers’ dream thesaurus. Image you have a thesaurus for poem stanzas instead of just for individual words and phrases. This is actually my inspiration for such project. Another related usage is comparative literature study. I can haz a much more comprehensive 管锥编?


You know, I am a cooker myself, albeit not a dexterous one with many recipes. I actually have a treasure trove. I tried to open it with pandas. To my frustration, dreadful OOM popped up. I want to build a service so that I can query all the recipes which could be done with the materials in my fridge and within 15 minutes.

Onward to …

Many years ago, I saw an article from a magazine in which a high school student abroad described his experience as a lonely stranger in a strange land. When asked why he decided to go abroad all alone after all, he answered he envies the American teenagers who have their deposit box in their school.

What a compelling (or you may think, unconvincing) reason! I have harbored many similar reasons. But I’d rather not to name them. Man wants one thing and one thing only, freedom or death. It’s fucking disgusting. Hell will be a better place for me if I was still under the grip of the Zhao King in 4 June 2024.

I can haz a choice?

Publié le par v dans «misc». Mots-clés: haskell, idris, hott, type-theory, distributed-systems