Records for 4-5 and 4-6

Dancing disco at the cementry.

About Mathematica

Mathematica 11 could not be started after a freetype upgrade.

When run in command line, it emits an error like this.

According to the gentoo forum site. Mathematica has its own libraries, and it calls the system library of freetype.

Forcing Mathematica to use the system library by removing and in ${TopDirectory}/SystemFiles/Libraries/Linux-x86-64 could solve the problem.

About R

To do a linear fit by this:

x <- c(...)
y <- c(...)
fit <- lm(y ~ x)

The one who wrote this article fell asleep halfway…

Rec 4.8

Computing Method

If f(x) satisfies:

  1. $f(x) \in [a, b], x \in [a, b]$

  2. $f’$ is Lipschitz continuous with some $K < 1$.

Then there exists a unique fixed point of f in $[a, b]$.

Existence: intermediate value theorem.

Uniqueness: reductio ad absurdum.

Newton’s method:

To find $X$ s.t. $F(X) = 0$.

First $X=X_0$

$$\Delta X_0 = \left(\left.\frac{\partial F}{\partial X}\right|_{X=X_0}\right)^{’}F(X_0)$$

$$X_1=X_0+\Delta X_0$$


$X_2=X_1+\Delta X_1$

Where $\frac{\partial F}{\partial X}$ is the Jacobian matrix of $F$.

Facts about Mozilla

  • It developed Thunderbird, a program for emails, feeds, and IM and so on. And now Thunderbird is abandoned.


It is said starting firefox with env MOZ_USE_XINPUT2=1 firefox enables scrolling with a finger. Not working now.

The bugzilla page suggests there should be a --enable-default-toolkit=cairo-gtk3 in the configure options shown in about:buildconfig.

Works now after upgrading GTK. Why.

Firefox OS

Another abandoned project is Firefox OS. Refer to this post.

  • Starting point: Boot to Gecko(B2G), push the envelop of the web

    • Architecture:
      • Gonk: Open Linux kernel and drivers
      • Gecko: Web runtime with open Web APIs
      • Gaia: User interface with HTML5-based Web content
  • Firefox OS 1.0

    • Imitate what already existed
    • Invented a lot of APIs to talk to hardware of a smartphone from Javascript(that wouldn’t come into standards)
    • Introduced packaged apps to Gecko to achieve both the offline(run apps without Internet connection) and security requirements(to secure privileged functions like calling and texting messages).
      • Packaged apps got no URLs and have to be signed by a central authority to say they are safe. -> Against the web.
  • Firefox OS 1.x

    • Just chasing the coat tails of Android
  • Differentiation

    • Affordable phones -> 1.3t
      • $25 smartphone: mostly done by Taipei office
    • Web -> 2.0
      • Haida: blur the line between apps and websites
      • Overshadowed by feature requests from venders
  • 3.0 -> 2.5 Come to stall and dead in the end.

Rec 4.9

Computer Architecture

Refer to Computer Architecture: A Quantitative Approach

Optimization of Cache Performance

  1. Nonblocking Caches to Increase Cache Bandwidth

Pipelined computers that allow out-of-order execution will benefit from this kind of cache which can supply cache hits even during a miss.

  1. Multibanked Cache
Bank 1 Bank 2 Bank 3 Bank 4
0 1 2 3
4 5 6 7
8 9 10 11
12 13 14 15

Increase bandwidth.

  1. Compiler

  2. Prefetching

Programming Languages

Still, refer to Standford’s cs242.

Existential types

Interface: specify what a type should be able to do, regardless of the implementation

Implementation: concretize the interface by showing how a type can implement the interface

It has two kinds of operations: pack and unpack.

Packing is the introduction of an implementation(see More monads in OCaml).

For example, this is an example of a monad interface:

module type M = sig
type _ t
val pure : 'a -> 'a t
val bind : ('a -> 'b t) -> 'a t -> 'b t

And an implementation of it:

module Option:M = struct
type 'a t = Nothing | Just of 'a
let pure x = Just x
let bind f x = match x with
| Just y -> f y
| Nothing -> Nothing

It’s an ugly example, but the point is, the detail about Option.t is erased, with only the interface(pure, bind) left.

utop # Option.pure 3;;
- : int Option.t = <abstr>

The implementation, Just 3 is not available here, and we cannot use Just to create a Option.t as well. Wait … shit.

Forget about monads, let’s go with another example:

module type Stack = sig
type _ t
val create : unit -> 'a t
val push : 'a t -> 'a -> 'a t
val pop : 'a t -> 'a t * 'a option
val empty : 'a t -> bool

And an implementation by list here:

module LStack : Stack = struct
type 'a t = 'a list
let create = fun () -> []
let push s x = x::s
let pop x = match x with
|x::xs -> xs, Some x
|[] -> [], None
let empty x = match x with
|x::xs -> false
|[] -> true

Everything works fine without the knowledge that LStack uses list for the stack. Say you create a new stack using LStack.create, there is no way for you to use it as a list, though it is one.

utop # let mystack = LStack.create ();;
val mystack : '_a LStack.t = <abstr>
utop # assert(mystack=[]);;
Error: This expression has type 'a list but an expression was expected of type
'b LStack.t

That’s abstraction in a nutshell.

The existential type is like this: ${*S, t} : {\exists X, T}$ means that type t, coupled with implementation S, makes a package that have an abstract type X with signature T. For the LStack, the analogy would be:

$$ *list \sim *S\ {create = \cdots, push = \cdots, pop = \cdots} \sim t\ {create : \forall a.unit \rightarrow X[a],\ push : \forall a.X[a] \rightarrow a \rightarrow X[a],\ pop : \forall a.X[a] \rightarrow X[a] * option[a]}\sim T $$

And there is the pack operation, which erases one or more types and introduces an implementation: $$\frac{\Gamma \vdash t : [X\rightarrow U]T}{\Gamma \vdash {*U, t}\ as\ {\exists X, T} : {\exists X, T}}$$


愛されたくて偽って もっともっと自然に笑えばいいかな

Comment and share

Facts about Bash/Dash/sh

  • Arch Linux uses Bash(Bourne Again Shell) for POSIX shell (/bin/sh)
  • When Bash is called with sh, it tries to emulate the POSIX shell
  • Dash is POSIX compatible, making it Bash incompatible.

Facts about of V-Table

In C++, the virtual table pointer is located in the head of the class instance.

The virtual table is a table of pointer to virtual(overridden or not) functions.

Therefore, to invoked these virtual methods, a mechanism called thunk(a jocular form of think) is needed. It means doing something before the actual function is called. And functional language relies largely on this mechanism.

Fact about Zeromq

  • It is a distributed communication library.
  • It sits on top of the TCP/IP layer, means the possibility is huge that it sends message by syscalls like send.

Facts about lttng

  • Means Linux Tracing Tool, next generation
  • In Artful repo, for older Ubuntu versions, go to ppa:lttng
  • Can be used to trace syscall, or even user application(need to write code into the program)
  • babeltrace could be used to translate the file.

Facts about Ubuntu

  • The life span of Zesty(17.04) has ended in Jan. 2018. Artful will meets its end in Jul. 2018.
  • The life span of non-LTS versions is 9 months.
  • 18.04 is called Bionic, will upgrade later

Facts about Opam

The package manager of OCaml. Not a kind of mineral.

Facts about type algebra

Refer to this page.

The type could be expressed in an algebra-like manner:

0: None type, there is 0 way to construct an empty type object

1: Singleton

2: Two ways to construct the type, boolean type is an example

$+$: Sum type, the object of type $a+b$ could be either type a or type b, but not both, there are exactly $a+b$ ways to construct the object. Injection is used to construct an instance, if it is called an instance.

$\times$: Product type, the object of type $a\times b$ is a combination of an object of type a and one of type b. OCaml adopts this notation, an constructor applied to type $a\times b$ is written as Foo of a*b.

And as a surprising yet unsurprising coincidence, the sum and product obey the rules:

Communicative: $a+b=b+a$

Associative: $a+(b+c)=(a+b)+c$

Distributive: $a\times(b+c)=a\times b+a\times c$

For recursive types like the tree, which is

data Tree a = Leaf a | Branch (Tree a) (Tree a)

The formula is:

$T = a + T^2$

Therefore, we have:

$$T^2-T+a=0 $$

$$T = \frac{1-\sqrt{1-4a}}{2}$$ (Why choose the minus sign?)

Use Taylor series, we could obtain:

$$T=1 + a + a^2 + 2 a^3 + 5 a^4 + 14 a^5 + 42 a^6 \cdots$$

And the coefficients of a are Catalan numbers.

Zippers means we could turn the pocket inside out and focus on one element in a data structure, in a way that updating the focused element , as well as moving the focus around, takes $O(1)$ time.

And we can focus on the holes of a type.

$a\times b$ has one hole of a

$a+a$ has two holes of a, that is data _, a and data a, _

It is likened to partial differentiation, for example:

$$\frac{\partial (u \times v)}{\partial a} = \frac{\partial u}{\partial a} \times v + \frac{\partial v}{\partial a} \times u$$

If $\frac{\partial t}{\partial a}$ means the hole numbers of a in t, and let the g of constant be zero, and g of other variables be one, then magic!

It can be applied to the list type:

data List a = [] | Cons a (List a)

$$L=1+aL$$, take both sides’ derivative of a, we got:

$$\frac{\partial L}{\partial a} = L + \frac{\partial L}{\partial a} \times a$$

$$\frac{\partial L}{\partial a}=\frac{L}{1-a}$$ and$\frac{\partial L}{\partial a}=L^2$. Bravo! That is the zipper type, one pointing to left and the other right.

Added 3/29:

But the same thing could not be perfectly applied to the binary tree type.

Recall, we have the binary tree type:

data Tree a = Leaf | Branch a (Tree a) (Tree a)

Then the formula is:


The best I could get is about:

$\frac{\partial T}{\partial a}=T^2L$, and the $L$ is a list of type $2aT$.

According to LYAHFGG, the zipper of a binary tree should be something like this:

data Crumbs a = LeftCrumb a (Tree a) | RightCrumb a (Tree a)
type BreadCrumbs a = [Crumbs a]
type Zipper a = (Tree a, Breadcrumbs a)

It is easy to see that Crumbs a has a type of $2aT$ and BreadCrumbs a has a type of $\frac{1}{1-2aT}$.

But wait! That gives $T$ rather than a $T^2$ in the numerator.

Maybe we’ve just started wrong, like, we took the wrong differentiation.

That would be left for future investigation.


PEBKAC (Problem Exists Between Keyboard And Chair) is the word that describes user error.

Comment and share

  • page 1 of 1
Author's picture


A progamer.

(click me to see some )