あまりわかってないけど、とりあえずいくつか適当な関数を書いたのでメモ。依存型うける(気がする)。 agda2 の emacs モードが使いこなせないのと関数を実行する方法がわからんのが問題である。 module NList where data Nat : Set where zero : Nat succ : …

今 Agda 的な論文を読んでて、Agda はなかなかおもしろそうだなと思った。Coq よりは情報系の人に優しい気がするし(僕は情報系ですらないという噂も。Oops!)。というわけで日記に Agda タグを作ってみた。依存型とかうけるし。

某T研究所のインターンシップ的なものに応募したんですが、見事に落ちました。残念すぎる。せっかくモデル検査の話があったので食いついてみんたんですが…。 だがしかし、こういうときこそ前向きにいかんとね。

pdfminer という pdf をあーだこーだするスクリプトが面白いので遊んでいる。pdf をそれなりな svg に変換するのが当面の目的だが、どうも一部の文字の位置がずれてしまう。 ソースを読む時間はさすがにないのでわからないが、ぱっと見だと太字の部分があや…

いいお勉強サイトはどこー。

そういえば知らなかった(!)のでメモ。yyでコピー、pでペースト。

気がついたら全然書いてなかった。特に忙しかったわけでもないんだけど。 前に研究室で emacs のキーボードマクロ(?)を簡単に説明したらみんなの食いつきがすごかったので、それを紹介。あと vim でも同じことをやる方法を調べたので、それも紹介。ただし vi…

最近 ocaml-nagoya で、id:yoshihiro503 さんと交代で圏論の発表をしている。 難しいけど、焦らずに地道にやっていきたい。そのうち圏論勉強会名古屋支部を名乗れるようになるといいなと思います。笑

今年の4年生も勉強会(SICP 読書会?)をやるらしい。素晴らしいことです。長く続けばいいんだけど。 で、講師をする schemer の id:athos がちょっとすごいので、彼の日記にあった限定継続版ジェネレータを普通の継続で書き直してみた。最初は楽勝だろーと思っ…

今まで気がつかなかったんだけど… <person> <name>...</name> <mail>...</mail> <mail>...</mail> ... </person> みたいに、 のあとに が任意回続くようなやつってよろしくないのですか？ お遊びで xslt 変換しようとして気がついたんですけども。少なくとも xslt じゃうまく処理できないですよね？ DTD も書けない気…

参加してます。ただのスタッフですが。PPL で見たことがある人もちらほら。 こういうところにいると、おもしろいけど自信をなくすから困るね。

普段の自分にもっとも必要な言葉はこれだな。さぼってはいけない。

うーん、SVG ってなかなかおもしろいですね。あんな簡単に絵が描けるとは思わなんだ。ただ残念な事に Safari だとアニメーション系がうまく動かない模様。

モデル検査のための抽象化の話。超書きっぱなし。 かの Dams さんは、もともとの実装を完璧に真似たモデルを concrete transition model, 適当に抽象化したものを abstract transition model と呼ぶらしい。で、そのモデルの間の関係を考える。抽象化を行っ…

まわりではやっているようなので勝手に便乗。結構短くかけた。 import List nums = [[08,02,22,97,38,15,00,40,00,75,04,05,07,78,52,12,50,77,91,08] ,[49,49,99,40,17,81,18,57,60,87,17,40,98,43,69,48,04,56,62,00] ,[81,49,31,73,55,79,14,29,93,71,40,…

C か C++ で BigNum を実装したいとか思ったけど、どうしたらいいかわからない。というかそもそも C++ の書き方がわからない。

図書館に行く用事があったので、ついでにいくつか本を借りてきた。Scheme 入門とかプログラミング Ruby とか。読みこむつもりは全然ないんだけど、これくらい知っとかないと馬鹿にされるかなとか思って。そんでまず Scheme 入門を飛ばし飛ばし読む。マクロと…

プログラミング Ruby を読む。巷で噂のブロックってのがでてきた。特に感想はないけど。まだ最初のほうしか読んでないんだけど、最後のほうをちらりと見たら、「型なんてあってもそんなに嬉しくないし、動的型付けなほうが生産性があがるんですよ」というよ…

id:msakaiさんが、sized-list の appendで長さ付きのリストを扱う方法を解説してくれている。すばらしい。 しかし型関数なんていうかっちょいいものがあったのかー。型関数の意味とか能力はさっぱりわからんけど、こんな風にかけてしまうとはおどろきである…

今日まで3日間、PPL2008 に参加してきた。先輩の id:syd_syd さんや指導教官のY先生をはじめ、ocaml-nagoya の人達や id:msakai さんなどがいらっしゃったので、あまりアウェイな感じはしなくて楽しかった。自分の発表は、ポスタに書いたプロパティに致命的…

諸事情からwindowsでmobility workbenchを動かさないといけなくなった．smlnjのwindowsバイナリをからサイトしてきて，READMEの通りにやったらうまくいかなかったのでメモ． まずTextIO.inputLineの戻り値がoptionな感じになってるのでそれを全部修正(case文…

Haskell でネットワークしてみよう，ということで．id:syd_syd さんの http://haskell.g.hatena.ne.jp/syd_syd/20061019/p1 とかのあたりも参考にすればいいと思う！ 研究室で定期的に投げられるお知らせメールを自動化しようということで，Python,Ruby,Java…

ラムダ計算はまったくわからんのですが，一応コードを書いたのでメモ．かけ算よりむしろ足し算のほうが難しかった． and と or はちょいと考えたけどわからなかったので wikipedia で調べた．足し算かけ算に比べるとなんとなく感動が薄い．笑 ラムダ計算での…

前に作ったやつが Safari で動かなくて悲しかったので， JSONP 的なものを使って動くようにしてみた． JSONP では script タグを使ってどっかのサーバに置いてある javascript を読みにいくことで，サーバをまたがった通信ができます． GreaseMonkey は scri…

研究室の隣の席の T さんに，JSON というのを教えてもらった．これを使えば GM_ な関数がなくてもなんとかなるらしい．時間を見つけて調べてみることにしよう．それと T さんに協力してもらって見た目よくした．やっぱりスタイルシートって難しい．てかさっ…

最近は何にもコードを書いてなかったので，id:suer さんから全面的なバックアップを受けつつ卒論から逃避しつつ Greasemonkey スクリプトを書いてみた．これで del.ico.us のブックマークにアクセスしやすくなったぜ！みたいな． Firefox の Greasemonkey で…

wxWidgets 2.8 と ghc6.6.1 でコンパイルに成功したという報告が． けど ghc6.6.1 が入らないので無理です…．バイナリすらも動かん．VM 上の適当な Linux でやってみるか…．

GHC 6.8.2 をバイナリから入れてみた． ghci がうまく動いてない様子だが，とりあえずほっといて wxHaskell の最新版を他のマシンの darcs で持ってきてコンパイル．wxcore は入ったのでサンプルを動かしてみるも， LSOpenFromURLSpec() failed with error -…

(たぶん)インストールできません。 ghc darcs subversion -> もとから入ってるっぽい ghc と darcs が結構致命的。 Leopard への乗り換えを検討されている方はご注意。

普通の MacBook を買いました．十分に満足しております． ただ， Macports で GHC が入らない点が不満．あと emacs も入らないみたい． このへんはなんとかしないと卒論が書けないな…．