No Such Blog or Diary

大学で明日の発表の準備．Expression Templates 使ったライブラリの技術的な話を期待さられているらしいのだけど，実装されたものを紹介しても複雑すぎるので簡易版を作って説明しなければならない．

ということで，朝からガリガリとC++のテンプレートなコードを書きつつスライド作成．ひと通り作ってから整理したら何故か２話分のスライドが出来上がっていた．

閑話休題．

休日の防犯巡回か何かの人たちがやってきて何かを語りかけられたのだけど，ぶっちゃけ何言ってるかわからんかった．ジェスチャー的に鍵をちゃんとかけろってことだと思うのだけど，正確なところはわからない．つか，フランス語分かりませんって言うフランス語を喋れるようになるべきだな．英語で言っても通じない．

「日本語食べれません」って言えば大抵の人は引き下がるよ，とかいうことを言っていた留学生を思い出した（「喋れません」すら言えないと認識されて無罪放免になるという論理）．

さくらのVPS以外も試してみようと思って，L2TP/IPsec な VPN が簡単に作れるかどうか幾つかの安い VPS で試した．つか，VPS と VPN って紛らわしい．

とりあえず月490円のお安い DTI の ServersMan @VPS Enrty を最初に試したが，使えるUbuntu のバージョンが古い（10.10 amd64, 10.04 x86）ってのと，カーネル周りがどうやって弄ったものかわからないのとで使いにくい．カーネルモジュール全然ないし……　モジュールを作りなおすとか嫌すぎるし……　そもそもカーネルいじれるのか？　Ubuntu でカーネル変えると起動しませんとか書いてあるドキュメントもあったり……　とかいう感じで即解約．そもそも Ubuntu のインストーラを自分で操作してインストールするタイプでないので色々と面倒．

次に，月840円のカゴヤの VPS タイプA を試すも基本的に ServerMan のと同じでカーネル周りの自由度が……　という感想で即解約．こちらはインスタンスを１日30円で簡単に増やせるのでその点は便利な気がする．

最後に月940円のお名前.com のVPS1GBプラン．これは普通に Ubunru 12.04 を Ubuntu のインストーラを使ってインストールできるのでさくらのVPSと同様に使いやすい（さらには自前のISOをマウントして起動できるのか？）．んで，通常のインストーラで入れるのでカーネル周りも普通で L2TP/IPsec な VPN の構築も何の問題もなく終わった．さくらの VPS と比べてコントロールパネルの出来がよろしい（初心者向けな）気がする．

とうことで，結論：お名前.com の VPS は使いやすいっぽい．計算機性能はどうだかしらんけど．

閑話休題．

お名前.com でサービスを使うには電話認証が必要だったりして微妙に躓いた．申請完了通知のメールに書いてあるURLのページに行ってそこにあるボタンを押すと，申請時に書いた電話番号に電話がかかってくるので，そのページにある認証コードを電話で入れてくださいと．……出張中にもかかわらず自宅の電話番号で申し込みをすると電話認証ができず残念なコトに．とりあえず，ユーザ情報の変更で携帯の電話番号に変更した上でもう一つインスタンスを申し込んで認証をするとかいう対処をした．つか，普通に電話番号間違って登録することもあるだろうから何処かに真っ当な対処法が有る気もする．

Haskell と違って型以外の項もパラメータにとれるので色々と遊べる．自動でプログラムを変換させてみたりとか（基本となる関数の変換方法をインスタンスとして置いといて，それらの基本関数を適当に合成したものの変換結果を計算させるとか）．

とりあえず基本的なギミックは理解したので来週はもうちょい応用にチャレンジしよう．

閑話休題．

自明だけど証明が面倒（というか tactic の使い方に慣れてない）なので admit が大活躍してたりする今日この頃．慣れている人が証明してくれることを願いつつリポジトリに投げる．

Coq の Module の Inline ディレクティブに関連して理解不能なエラーにハマった．下のコードがハマった部分を抜き出したもの．

Module Type A. End A.
Module Type B  (a : A). 
  Parameter t : Type.
End B.
Module Type Bi (a : A). 
  Parameter Inline(10) t : Type.
End Bi.
Module C  (b : B).  End C.
Module Ci (b : Bi). End Ci.
 
Module CX (b : B) (bi : Bi).
  (* These two work well.*)
  Module Cb := C b.
  Module Cbi := C bi. 
  (* These two work well too, using `!' to ignore the Inline directive. "*)  
  Module Cib := !Ci b.
  Module Cibi := !Ci bi.
  (* This fails with saying "Error: The field t is missing in Top.b."*)  
  Module Cib2 := Ci b.
  (* This fails with saying "Error: The field t is missing in Top.bi."*)  
  Module Cibi2 := Ci bi.
End CX.

ファンクタ B と Bi は Print Module Type で見ても名前以外は同じ．ファンクタ C と Ci はファンクタ B と Bi をとる．んで，この C と Ci に B と Bi の型の b と bi を適用してみると，Inline を付けた定義の Bi を受け取るという定義の Ci に関してよくわからんエラーが出る．b も bi も t というフィールドを持っているのにそれが無いとか言われ……　

とりあえず ! 付けて Inline を無視させればエラーでないということは学習した．でも Inline の意味はよくわからん．

Coq に「Hoge a b c の項が期待されるのに Hoge a b c の型の項なのでエラー」と言われた．このメッセージだけを見ていても何も悪いことしてないようにしか思えない．

んで，Set Printing All. と叫んでみたら implicit なパラメータ部分で微妙にずれていたという罠で，「@Hoge X a b c の項が期待されるのに @Hoge Y a b c の型の項なのでエラー」という意味のわかるエラーを吐いてくれるようになった．

……見えている型が同じだったら隠れている部分も自動で表示してくれればいいのに．

いい場所にキッチン付きのホテル（アパートメントホテル）を見つけたので移動．目の前に大学直通のトラムの駅がある．まぁ，３０分強かかるけど．

とりあえずキッチンが使えるのはいいことだ．