http://madscientist.jp/~ikegami/diary/ IKEGAMI Daisuke Copyright 2011 IKEGAMI Daisuke <ikegami(at)madscientist.jp>, copyright of comments by respective authors http://madscientist.jp/~ikegami/diary/20111029.html#p01 2011-10-29T12:41:42+09:00 IKEGAMI Daisuke まとまった文章書く気力がなかなか出ないのと、ついつい Twitter で言いたいことつぶやいて、何も残らない現象起きています。FaceBook もあるし Google+ もあるし、使い分け難しいね。 そこで、下書き.. http://madscientist.jp/~ikegami/diary/20110912.html#p02 2011-09-12T17:31:35+09:00 IKEGAMI Daisuke バグを踏むのを恐れずに先端のソフトウエアを使いたい人向けに、開発版のインストールの方法も説明する。 Agda は ghc (Glasgow Haskell Compiler) と haskell-mode と Agda それ自身(ghc の Agda ライブラリと Emacs の agda2-mode.el)、および Agda 標準ライブラリに依存するソフトウエアである。したがって、この 4 種類をインストールする必要がある。開発版をインストールするために、分散バージョン管理ツール darcs をインストールする。 ghc のインストールは、Haskell Platform を導入するのが楽である。 haskell-mode は Linux .. http://madscientist.jp/~ikegami/diary/20110912.html#p01 2011-09-12T17:31:35+09:00 IKEGAMI Daisuke 現在の Agda のインストールの方法を解説する。今後の開発状況によって、やり方は大きく変わる可能性があるので注意すること。Agda Wiki に最新の方法が記述されるはずである。 Linux については、いくつかのプラットフォーム Agda on.. http://madscientist.jp/~ikegami/diary/20110910.html#p01 2011-09-10T02:31:13+09:00 IKEGAMI Daisuke 旧 Agda で書かれた Hoare 論理のライブラリを Agda2 に翻訳した件について。 Separation 論理が Hoare triple で書かれているので、それを Agda にもちこむにはどうしたらよいのだろうかという妄想から、移植プロジェクトが始まった。Separation 論理は巨大なサイズの Coq ライブラリとして実現されている。それを Agda でどうこうするのは大変だろうなという想像はつくが、どれだけ大変なのかを身をもって知りたかった。 移植の方針は、1) 実直に翻訳 2) Agda 標準ライブラリをできるだけ使う 3) 足したり引いたりしない、の以上3点で行.. http://madscientist.jp/~ikegami/diary/20110807.html#p01 2011-08-08T07:57:59+09:00 IKEGAMI Daisuke 関西でのプログラマの発表/雑談会、前々回、前回に続いて３回目を行いました。参加してくださった皆様ありがとうございます。 発表は以下の通りでした: 理想のキーリマップとは : 天狼の紹介 by @kozo2 さん Kinect でなんかやる by @zophos さん 『プログラミング言語の基礎概念』と演習システム紹介 by @zick_mionh さん カーネルから見るAndroidのセキュリティ by @hiromu1996 さん Haskell モナド入門 by わたし ConsoleKit/PolicyKit by @naota344 さん 順番にまとめます。一件目のキーリマップについて。キーボードのキーの効果をア.. http://madscientist.jp/~ikegami/diary/20110620.html#p01 2011-06-20T21:57:00+09:00 IKEGAMI Daisuke 関西でのプログラマの発表/雑談会、前回に引き続いて二回目を行いました。これまた、あっという間の２時間でした。参加者のみなさん、ありがとう。今回はプロジェクタを用いた発表形式でした。 まず、自己紹介で大宮さんの話がおもしろかったのですが書けません。 竹岡さんのtemoral prolog.. http://madscientist.jp/~ikegami/diary/20110415.html#p04 2011-04-15T10:11:17+09:00 IKEGAMI Daisuke ソースコードはここにあります。 safii さんの GLUT のサンプルでは、カメラが 3D 座標に置かれているのですが、Gloss は 2D しか取り扱うことができません。 そこで、立体的なアニメーションはあきらめて、2D に射影したグラフィクスを描きます。 Haskell で乱数をとりあつかうには、標準の System.Random を利用するのが簡単です。 つまづきやすい点として、乱数の関数は IO モナドからつくられるということがあります。 関数というのは、ふつう、同じ入力からは同じ出力しかでてきません。 この性質が Haskell のコード.. http://madscientist.jp/~ikegami/diary/20110415.html#p03 2011-04-15T10:11:17+09:00 IKEGAMI Daisuke safii さんの GLUT のサンプル では、四角形が回転し、下矢印キーを押すと回転方向が逆向きになります。 キーやマウスのイベントを利用するには、 さきほどの四角形を回した関数 animationInWindow ではなく、 別.. http://madscientist.jp/~ikegami/diary/20110415.html#p02 2011-04-15T10:11:17+09:00 IKEGAMI Daisuke ソースコードはここにあります。 safii さんの GLUT のサンプルと比べると、ずいぶんコードが減りましたがこれは Gloss .. http://madscientist.jp/~ikegami/diary/20110415.html#p01 2011-04-15T10:11:17+09:00 IKEGAMI Daisuke Haskell の 2D グラフィックスライブラリ Gloss の入門記事です。 Haskell で 2D グラフィックスするのはどうすんの : Stack Overflowで紹介されていたので試してみました。あと、前回の関西Codersで、流体シミュレーションを Java で、というのを見せてもら.. http://madscientist.jp/~ikegami/diary/20110412.html#p07 2011-04-13T13:38:44+09:00 IKEGAMI Daisuke その場ではお見せできなかったので、宿題にまわしたものがあり.. http://madscientist.jp/~ikegami/diary/20110412.html#p06 2011-04-13T13:38:44+09:00 IKEGAMI Daisuke RushCheck.. http://madscientist.jp/~ikegami/diary/20110412.html#p05 2011-04-13T13:38:44+09:00 IKEGAMI Daisuke BrainF**k で日本.. http://madscientist.jp/~ikegami/diary/20110412.html#p04 2011-04-13T13:38:44+09:00 IKEGAMI Daisuke Java で流体シミュ.. http://madscientist.jp/~ikegami/diary/20110412.html#p03 2011-04-13T13:38:44+09:00 IKEGAMI Daisuke Prolog で型推論器を書..