下の記事の続き。 hintは意外に私の欲しい機能がなく、たとえば「あるレコード型のフィールド名をすべて取得」みたいなことができない。Template Haskell の reify 関数なら、任意の識別子について reify が使えるののに… というわけで、 ややアクロバティッ…

GHC API のラッパー hint を使えばHaskellでも手軽にリフレクションっぽいことができる。例えば動的にHaskellのソースをロードして関数を呼び出す、といったことが数行で書ける。 ところでリフレクション周りで色々やろうとすると、すぐに関数の型を解析した…

参考：http://d.hatena.ne.jp/yoshihiro503/20100119#p1証明すげー。 あと、幅優先探索で見つけたパスを無限ストリームで並べているのを見てこれは面白いと思った。枝刈り付きBFSとゴールの発見手続きを独立に書けているのか。なるほど！ ストリームを使った…

無限ストリームの型はCoInductiveという構文で宣言された余帰納的な型である。 無限ストリームはCoFixpointという余帰納的な関数(?)を作る構文で定義する。Fixpointは最小不動点(Coqなら「いつか必ず止まる」)だがCoFixpointは最大不動点(止まらない、無限?)…

Windows Server 2003 を使っているのですが、 ドメインメンバーだからか コントロールパネルの「日付と時刻」では NTPクライアントのタブがなく、GUIで設定できなくなっていました。 次のコマンドラインで、NTPクライアントを設定しました： w32tm /config /…

fixタクティックについて。 ふつう、Coqの証明モードで構造帰納法を回したい場合は inductionタクティックを使いますが、 fix は、帰納法のためのよりプリミティブなタクティックのようです(項の場合分けをやらない)． This tactic is a primitive tactic to…