No Such Blog or Diary

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 の型の項なのでエラー」という意味のわかるエラーを吐いてくれるようになった．

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

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

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

1998年～1999年 Slackware．最初に Linux をいじった時にはカーネルのバージョンはまだ 2.0.X だった．PJE で Wnn を突っ込んだりとかしていたような気がする．この頃に比べると最近はものすごく便利になったもんだ．

1999年～2000年 Turbo Linux．ここらで Slackware で環境整えるのが面倒になって Turbo Linux に手を出してひよった．研究室のマシンは FreeBSD だったっけな．まだまだ Linux は趣味の世界だった頃？

2000年～2005年 Red Hat＆Fedora Core．ひよるのにお金かけるのもあれだからとフリーにもどる．しばらくは Red Hat 系で安定．

2005年～2006年 Gentoo．後輩が使っているのを見て使い始めた気がする．結局，色々と面倒になったのとコンパイルしまくるのは環境によろしくないのとで１年くらいしか使わなかった気がする．

2006年～2008年 Debian．ここらは使うディストリビューションを色々試しつつ Fedora より Debian のほうが使いやすいかなぁとか考えていた気がする．

2008年～2012年 Ubuntu．お仕事用のメインマシンを Linux にして生活しようと決めて，色々と楽な Ubuntu に移ったのが 2008年の頭だったはず．ここから基本的に Ubuntu しか使ってない．

うん，よくわからんが普通な変遷だ．

あー，彼岸花の時期は終わったかぁ．コスモスもそろそろ微妙かぁ？　紅葉前線はどこだぁ？

閑話休題．

モン・サン・ミッシェル行きのツアーが７月から９月の期間限定だった orz　楽しようと思ったけど失敗．ちゃんと計画を練るか．

閑話休題．

1年前に書いた下記の Haskell コードが読めなくなっている．修行が足らん．

fib((-1+)->n@((-1+)->m))|m<0=1|((,,fib n)m->(fib->x,_,y))<-()=x+y

閑話休題．

国際電話のタイムラグを体験．やっぱ微妙に遅れるね．

今日は満月だったのか？　とか考えつつ６時半頃に近場のトラムの駅へてくてく．

７時過ぎに LES AUBRAIS 駅に到着．パリ行の Intercites の切符を買って７時半ちょっと前に電車出発．

８時１５分くらいにオステルリッツ駅到着→メトロ５でバスティーユ駅に→メトロ１でルーブル美術館．残念ながら駅から地下に抜ける通路の扉が閉まっていたので8:45くらいに地上からピラミッドに並んだ．最初の折れ曲がりの手前には並べたけれど前回よりも前に並んでいる人の数がだいぶ多い．Intercites があと20分くらい早いといいのだけど，一本前は一時間以上前なので微妙．

そしてまたニケへ直行．でも既に人が……　スタートダッシュが足りなかった．

混んでるところを遠巻きに見るシリーズ：

なんとなく朝日の入り具合的に室内が金色に輝いてるように見えたのだけどうまく撮れない罠．あれこれしているうちに団体に占拠されてチャンスを逃した……

よくわからない工事中？　

お帰りは地下からで．セキュリティチェックがボトルネックだよね……　そのあとのチケット購入は自動券売機が意外と空いている印象．

人が多すぎてやる気なくしたので今回は２時間半ほど見て回って終了．久々にアジア系の人を沢山見た気がする．つか，列に並んでた前のグループ日本人だったし．

閑話休題．

せっかくパリに出てきたし＆レンズの焦点距離が足らんしということで，Eマウントの望遠レンズを見に Chatelet - Les Halles 駅のところのショッピングセンターにある Fnac に行ってみたんだけど……　Sony E 55-210mm F4.5-6.3 の値段が 349ユーロとかで kakaku.com の 30010円よりだいぶ高いという結果．悩ましいので購入は見送った．もうちょっと旅程が単純だったらレンズも沢山持ってこれたんだけどなぁ．

閑話休題．

今日の予算：ルーブル美術館入館料 11ユーロ，パリ・オルレアン往復 19.50ユーロx2，パリ市内のメトロ移動 1.7ユーロx3，合計で 55.1ユーロ（オルレアンのトラムは去年の10回券のあまり2回分を使ったのでカウント無し）．まあ，ユーロ安くなったしリーズナブルなお値段で遊んできた気分．