No Such Blog or Diary

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

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

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

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

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

閑話休題．

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