天泣記

2020-06-30 (Tue)

#1 xkb

思い立って、xkb の説明を読んでみた

2020-05-30 (Sat)

#1 湾曲ディスプレイ

ふと、湾曲ディスプレイと平面ディスプレイで みかけの大きさがどう対応しているか気になった

湾曲ディスプレイの曲率は 1000R とか 4000R とかで表されて、 1000R なら、半径1000mm の円 (の一部である弧) の曲線という意味である

検索したところ、現時点では、1000R というのがいちばん曲率が高いようだ また、画面サイズはだいたい 24, 27, 32, 34inch あたりが多くて, 縦横比は 16:9 と 21:9 が多いようだ。 とりあえず 16:9 とすると、 24inch なら長辺の長さは 24 * 16/hypot(16,9) [inch] = 20.9[inch] = 531[mm] 、 32inch なら長辺の長さは 32 * 16/hypot(16,9) [inch] = 27.9[inch] = 708[mm] などとなる

(湾曲ディスプレイのサイズは、湾曲している画面にそった長さとしよう。それが正しいかどうかはわからないけど)

ユーザとディスプレイの距離は通常 1000mm よりは近いと思う

その場合、湾曲ディスプレイ (の弧の長さ) と同じ横幅の平面ディスプレイで、 ユーザから見た画角を比較すると、湾曲ディスプレイのほうが大きくなるはずである。

ユーザが平面ディスプレイを正面から x[mm] 離れた点から見るとして、 ディスプレイの横幅が w[mm] であれば、 画角は、2 * atan((w/2)/x) [rad] = 360 * atan(w/(2x)) / pi [度] となる

ユーザが曲率 r[mm] の湾曲ディスプレイを正面から x[mm] 離れた点から見るとして、 ディスプレイの横幅 (弧の長さ) が w[mm] であるとする。 このとき、正面から r[mm] 離れたところからみると、 ディスプレイの画角は w / r [rad] であり、 弧の横幅は 2 * r * sin(w / (2*r)) [mm] であり、 弧の奥行は r - r * cos(w / (2*r)) [mm] となる。 ユーザはこの弧を x[mm] 離れたところから見るので、 画角は、2 * atan(r * sin(w / (2*r)) / (x - (r - r * cos(w / (2*r))))) [rad] = 360 * atan((r * sin(w / (2*r))) / (x - (r - r * cos(w / (2*r))))) / pi [度] となる

とりあえず、1500R (r=1500) で 32inch (w=708) としてプロットしてみると

curved-display.png

curved-display.gp:

r=1500.0
w=708.0
plot [0:1000] 360 * atan2(w,(2*x)) / pi, 360 * atan2((r * sin(w / (2*r))), (x - (r - r * cos(w / (2*r))))) / pi

ふむ、600mm くらい離れたところから見たときで、違いは 10度に満たない感じか

ユーザの距離を 300mm から 800mm でプロットしてみる

curved-display-300-800.png

curved-display-300-800.gp:

r=1500.0
w=708.0
plot [300:800] 360 * atan2(w,(2*x)) / pi, 360 * atan2((r * sin(w / (2*r))), (x - (r - r * cos(w / (2*r))))) / pi

2020-04-30 (Thu)

#1 Compiling with continuations のその後

Compiling with continuations (1991) という書籍があって、 CPS (Continuation Passing Style) をコンパイラで使うという話なのだが、 CPS を使うのが良いかどうかというのは、いろいろと議論がある。

1993年に The essence of compiling with continuations という論文があって、 これは A-normal form の提案でかなり有名なので前から知っていたのだが、 その後も、いくつかあからさまなタイトルの論文が出ているようだ

2020-03-30 (Mon)

#1 OCaml での tail recursive な map (逆順にもならず、無駄にメモリを確保しないやつ)

OCaml でリストの map を書くと、素朴には以下のようになるだろう。

let rec map f s =
  match s with
  | [] -> []
  | v :: s' -> f v :: map f s'

標準ライブラリの List.map も、書き方はちょっと違うが、同じようなものである。

<URL:https://github.com/ocaml/ocaml/blob/4.10.0/stdlib/list.ml#L90-L92>

let rec map f = function
    [] -> []
  | a::l -> let r = f a in r :: map f l

ただ、この実装は、tail recursive ではない。 これはマニュアルにも Not tail-recursive. と明記されている。

tail recursive ではないので、リストの長さに比例してスタックを消費する。 なので、とても長いリストに使うと、おそらく不幸なことになる。

では、tail recursive に書こうと思って単純に累積引数を使うと、 リストが逆順になってしまう。 これを実装したものは標準ライブラリの List.rev_map にある。

<URL:https://github.com/ocaml/ocaml/blob/4.10.0/stdlib/list.ml#L100-L105>

let rev_map f l =
  let rec rmap_f accu = function
    | [] -> accu
    | a::l -> rmap_f (f a :: accu) l
  in
  rmap_f [] l

では、tail recursive で、かつ、逆順にならないように、というなら、 List.rev は tail recursive なので、 List.rev_map と List.rev を組み合わせればいい。 しかし、そうすると、List.rev_map で生成したリストをすぐに捨てることになるので、 メモリの無駄である。(無駄に GC 頻度が上昇する、というほうが正確かも)

では、tail recursive で、逆順にならず、無駄にメモリを確保しない map というのは実装できるか?

少し考えると、リストというのは構造上、先頭から末尾に向かってしか調べられず、 また、リストは末尾から先頭に向かって構築せざるを得ない、 ということから、そういう map は無理っぽいと思える。

しかし、最近、Coq の実装内部に、そういう map の実装が存在することを発見した。

<URL:https://github.com/coq/coq/blob/V8.11.0/clib/cList.ml#L403-L415>

let rec map_loop f p = function
  | [] -> ()
  | x :: l ->
    let c = { head = f x; tail = [] } in
    p.tail <- cast c;
    map_loop f c l

let map f = function
  | [] -> []
  | x :: l ->
    let c = { head = f x; tail = [] } in
    map_loop f c l;
    cast c

ここで、head と tail というフィールドをもつレコードと、cast という関数を使っているが、これらは以下のように定義されている。

<URL:https://github.com/coq/coq/blob/V8.11.0/clib/cList.ml#L143-L151>

(** Tail-rec implementation of usual functions. This is a well-known trick used
    in, for instance, ExtLib and Batteries. *)

type 'a cell = {
  head : 'a;
  mutable tail : 'a list;
}

external cast : 'a cell -> 'a list = "%identity"

コメントによれば、これは Coq 独自のアイデアではないようだ。

なにをしているのかというと、コンスセルの tail (cdr) を破壊的に書き換えている。 もちろん OCaml の list 型では書き換えられないのだが、 cell 型では (mutable tail としているので) 書き換えることが可能で、 そうやって書き換えたものを cast 関数で無理やり list 型に変えてしまっている。

この cast 関数というのは、Obj.magic とだいたい同じもののようある。 Obj.magic は以下のように定義されていて、任意の型から任意の型に変えられるが、 cast は cell 型から list 型へ変換するだけにしか使えないようにされている。

<URL:https://github.com/ocaml/ocaml/blob/4.10.0/stdlib/obj.ml#L22>

external magic : 'a -> 'b = "%identity"

OCaml 内部のメモリ表現を知っていれば、cell 型と list 型 (の (::) コンストラクタで作られるデータ) が同じ構造になることは わかるので、こうやって型を変えれば、tail を破壊的に書き換えられる。 tail を破壊的に書き換えられれば、map をうまく実装できる、つまり tail recursive で、逆順にならず、無駄にメモリを確保しない、という実装が可能になる。

つまり「リストは末尾から先頭に向かって構築せざるを得ない」という前提を取り除き、 先頭から末尾に向かって構築することにより、こういう map の実装が可能になる。 まぁ、Lisp や C でリストを扱うなら、 こうやって tail を破壊的に書き換える実装をするのは珍しくないと思うのだが、 OCaml でやっちゃうというのが驚くところである。

なお、ExtLib だとどうなっているか調べると、以下のようになっている。

<URL:https://github.com/ygrek/ocaml-extlib/blob/1.7.6/src/extList.ml#L31-L36>

(* Thanks to Jacques Garrigue for suggesting the following structure *)
type 'a mut_list =  {
  hd: 'a;
  mutable tl: 'a list
}
external inj : 'a mut_list -> 'a list = "%identity"

あー、なるほど、誰が言い出したのかわかったかもしれないですね。

追記: Garrigue先生に教えてもらったのをもとに調べたところ、 以下のような流れのようだ

ExtLib で以下のように入った

他のプロジェクトでも使われる

それはそれとして、言語自体に仕掛けをいれて、ユーザが破壊的変更を記述せず、 最初に書いたような素朴な関数でも定数サイズのスタックで済むようにしようという話がある

2020-02-27 (Thu)

#1 coq issue #11690

GitHub coq/coq#11690: CoqIDE menu item 'View -> Display raw matching expressions'

2020-01-28 (Tue)

#1 TCP_INFO の使い方

そういえば、GNU/Linux では、getsockopt の TCP_INFO で TCP の state を見れる。

ある端末で以下のように TCP のサーバを動かす

% nc -v -l -p 9999
Listening on [0.0.0.0] (family 2, port 9999)

で、次のようにして接続して getsockopt(TCP_INFO) すると、state=ESTABLISHED ということで、TCP state は ESTABLISHED であることがわかる。 (行は長いので改行してある)

% ruby -rsocket -e 'Socket.tcp("127.0.0.1", 9999) {|s|
  p s.getsockopt(Socket::IPPROTO_TCP, Socket::TCP_INFO)
}'
#<Socket::Option: INET TCP INFO state=ESTABLISHED
  ca_state=Open retransmits=0 probes=0 backoff=0
  options=TIMESTAMPS,SACK,WSCALE rto=0.204000s ato=0.000000s snd_mss=21845
  rcv_mss=536 unacked=0 sacked=0 lost=0 retrans=0 fackets=0
  last_data_sent=0.000s last_ack_sent=0.000s last_data_recv=0.000s
  last_ack_recv=0.000s pmtu=65535 rcv_ssthresh=43690
  rtt=0.000022s rttvar=0.000011s snd_ssthresh=2147483647 snd_cwnd=10
  advmss=65483 reordering=3 rcv_rtt=0.000000s rcv_space=43690
  total_retrans=0 (120 bytes too long)>

2020-01-18 (Sat)

#1 ounit issue

GitHub ounit/issues/11: symlinked files outside of temporary directory is removed



田中哲