はてなブックマーク

CoqUn2010View more presentations from mzpi. 強者の集うCoq庵 : ATNDで無謀にも発表してきました http://www.ustream.tv/recorded/9222006に動画もあるらしいです。怖くて確認できてないですけど。

大名古屋ことGoogle グループの宿題で「Hadoopを動かしてみること」というのがあったので、試してみました。Javaを使う気にはならないので、Scalaで。 コード Hadoopの2章のコードを素直に写経する。一ファイル一クラスの制限がないのはいいね。 import java.util.Iterator import org.apache.hadoop.fs.Path import org.apache.hadoop.io._ import org.apache.hadoop.mapred._ class MapExample extends MapReduceBase with Mapper[LongWritable,Text,Text,IntWritable] { def map(key : LongWritable, value : Text, output : OutputC

30分プログラム、その207。iTunesでの文字化けを解消するために、ID3Tagの文字コード変換プログラムを作ってみた。 結局はこれでは解決せずに、http://ipod-life.org/archives/2004/12/itunes_aaaaeaa_1.phpに書いてある方法で解決した。もしかして文字コードが原因じゃないんだろうか? 使い方 $ ./id3tag.rb foo.mp3 bar.mp3 ソースコード #! /opt/local/bin/ruby -w # -*- mode:ruby; coding:utf-8 -*- # # id3tag.rb - # # Copyright(C) 2007 by mzp # Author: MIZUNO Hiroki / mzpppp at gmail dot com # http://howdyworld.org # # Time

発端 TDDブートキャンプで「テストを書くのはつらい。Bob Martinもacts_as_professionalと刻んだグリーンバンドを身につけて、自分を戒めてるんだ」というエピソードが紹介される ボクも欲しい! http://mixbuzz.com/wristbands.htmlで20個から作ってもらえるらしい さっそく賛同者を募ったところ30個、希望者が集まる よし、注文しよう! 進捗状況 2010-07-11: http://mixbuzz.com/wristbands.htmlに見積りを出しました。Mサイズで30個。色はJUnitのグリーンの色(rgb(0,188,65), ■)です。 2010-07-12: 「RGB指定は200個からです」と言われました。ネオングリーン■で再見積りを出しました。ついでに個数を40個に増やしました。 2010-07-13: 上記の設定で見積りが

明日は、TDD Bootcamp名古屋です。 というわけで、自分のoUnit + omakeでTDDな環境を晒してみます。もっとクールな方法があったら教えてください><。 ちなみに、構築したサンプルはGitHub - mzp/ounit-example-1: OUnit exampleに置いてあります。 ディレクトリ構造 ディレクトリ構造はこんな感じで、本番コード(./src)とテストコード(./test)が別ディレクトリに分かれています。 . |-- OMakefile |-- OMakeroot |-- src | |-- OMakefile | |-- fact.ml | `-- main.ml `-- test |-- OMakefile `-- fact_test.ml ルートのOMakefile ルートのOMakefileではサブディレクトリを認識させます。ついでにocamlf

これ何? irssiというIRCクライアントのプラグインです。 入力した文字数を表示するので、tig.rbのようなTwitterとIRCをつなぐゲートウェイと併用すると便利です。 使い方 word_count.pl · GitHubをダウンロードして、~/.irssi/scriptsに置いてください。 あとはirssiから /script load word_count.pl /statusbar window add word_countで文字数をカウントするステータスバーが追加されます。 ソースコード #! /usr/bin/perl # -*- mode:perl; coding:utf-8 -*- # # char_count.pl - # # Copyright(C) 2010 by mzp # Author: MIZUNO Hiroki / mzpppp at gmail do

これからはTwitterクライアントもOAuthに対応してかないといけないらしいですよ。参考: Twitter APIのBASIC認証は2010年6月に「廃止予定」（→8月まで延長）（→廃止された模様） - 頭ん中。 というわけで、tig.rbをOAuthに対応させてみました。 使い方 (1) OAuth対応版のtig.rbを入手 OAuthに対応させたtig.rbはGitHub - mzp/net-irc at oauthにあります。 gitコマンドの使える人は、以下のように取得できます。 $ git clone git://github.com/mzp/net-irc.git -b oauthgitコマンドの無い人は、tarballをどうぞ。 (2) 認証用のURLを取得する tig.rbを--oauthオプションをつけて起動します。 $ ruby examples/tig.rb --

body{ font-size:10.5pt; } のようにやると、Webページのポイント単位でフォントサイズを指定する事ができる。 しかし、ここは body{ font-size:36px; } のようにpxを使いピクセル単位で指定するべきだ。 ポイントは、70ポイント=1インチ=2.54cmと定義された物理的な値。そのため、それが実際に何ピクセルになるかは、モニタやOSなどの環境によって変化する。 だから、ある環境で10.5ポイントのフォントの高さが40ピクセルの画像と同じ高さであっても、他の環境で同じである保証はない。 というわけで、一貫性をもったデザインを作りたい場合はピクセル単位で指定するべきだし、一貫性が必要ないならそもそも指定する必要がないでしょ？ 参考 CSS完全ガイド 第2版

git diffをすると、前回コミットしたときからのdiffを出してくれます。 で、各差分(ハンク)ごとに、変更範囲も教えてくれます。でも、正直なところ、n行目周辺が変更されたと言われてもよく分かりませんよね。 そこで、.gitattributesに *.tex diff=texと書いてやって、*.texにはtex用のdiffを使うことを教えてあげます。 すると、git diffが、どのセクションが変更されたかを表示してくれます。 参考 入門Git 作者: 濱野純(Junio C Hamano)出版社/メーカー: 秀和システム発売日: 2009/09/24メディア: 単行本購入: 31人 クリック: 736回この商品を含むブログ (155件) を見る

30分プログラム、その705。前にcursesみたいにターミナルの任意の位置にテキストを出す関数 - みずぴー日記でcursesを使わずに端末の好きな位置に文字を出せるようになったので、slを作ってみました。 Perlで使っていた\eがPythonでは使えなかったので、hi_saitoさんが使っていた\033を使っています。 で、作ってから気がついたんですが、本物のslと違って煙がでません。まあ、クリーンなSLということで。 使い方 $ python sl.py ________ __________ _______/ \__I_I_____===__|_________ | H\________/ | | =|___ ___| ________________ | H | | | | ||_| |_|| _| \_____ | H |__--------------------| [__

前からずっと取り組んでいた「Coqで単純型付きラムダ計算を証明してみよう」が一段落しました。 動機 let多相の実装はしたから、次は証明だろ 最近、流行っているCoqを覚えたい 扱えるラムダ式 型は、Bool型と関数型のみ。 Inductive type : Set := | BoolT : type | FunT : type -> type -> type. 式は、変数参照、真偽値、ラムダ(関数抽象)、関数適用、if式。 Inductive term : Set := Var : string -> term | Bool : bool -> term | Lambda : string -> type -> term -> term | Apply : term -> term -> term | If : term -> term -> term -> term. 証明した定理 型

30分プログラム、その691。HOASによるラムダ式。 id:keigoiさんに、HOAS(Higher order abstract syntax)なるものを教えてもらいました。 詳しいことは、http://homepages.inf.ed.ac.uk/ratkey/unembedding.pdfに書いてあるらしいです。 今のところの理解は、 Haskellのラムダ式で、ターゲット言語のラムダ式を表現する アルファ変換とか変数補足とかを考えなくてすむ といった感じです。 さっぱり分からないので、上記の論文にのっている例を実装してみました。 使い方 *Main> eval (lambda (\x->x) `apply` (int 42)) 42 ソースコード {-# OPTIONS_GHC -fglasgow-exts #-} import Text.Printf class Lambda

F# at Microsoft Research - Microsoft ResearchについてきたTutorial.fsを読みながら、F#とOCamlの違いついてメモしてみます。 拡張子が.fs OCamlは.mlだけど、F#は.fs。 コメントが// OCamlのコメントは(* ... *)だけど、F#は//。 範囲 let oneToTen = [1..10] 内包表記 /// The squares of the first 10 integers let squaresOfOneToTen = [ for x in 0..10 -> x*x ] ディクショナリ let lookupTable = dict [ (1, "One"); (2, "Two") ] let oneString = lookupTable.[1] パイプライン 2008-11-12の+>と同じですね。

30分プログラム、その650。http://gauc.no-ip.org/awk-users-jp/blis.cgi/DoukakuAWK_206にインスパイアされました。 上記ページからリンクされているパソコンなら演算が得意なのは理解出来ますが､現在100円クラス... - Yahoo!知恵袋に平方根の計算方法が紹介されていました。 ＴＶで言っていた話なのですが その数字を１から順に奇数を引いていき、０になるまで計算（マイナスになったときはそ の一つ前） ４＝1+3 ９＝1+3+5 ２５＝1+3+5+7+9 で、その奇数の数を何個足したかでルートが算出される。 割り切れない数字の場合もこの応用で計算していて、電卓のルート計算はこの方法を元に 制作しているそうです。 なんだ、これは?! なんで計算できるのかも、奇数の理由もよく分からないし、割り切れない数にどうやって応用したらいいのかも分か

最近、Scalaで遊んでるけれども、MacのScalaは起動が遅すぎる。 VMware FusionにいれたUbuntuで開発してもいいけど、端末しか使わないのにGNOMEを立ち上げるのはメモリがもったいない。それほど、メモリが潤沢にあるマシンでもないし。 というわけで、DebianをXなしでインストールして、Macからsshでつないで使うことにする。WindowsのcoLinuxのイメージ。 Debianのインストールイメージの取得 Debian -- Debian-Installerから好きなのを選ぶ。 ボクは、testingのnetinst CD イメージにしました。 VMware Fusionの設定 VMware Fusionの設定はこんな感じ。あとは、インストール時に「デスクトップ環境」のチェックをはずすようにすればいい。 必要なソフトのインストール まずは、openssh-se

id:mzp:20070214:1171465153の続き。RubyのNet::HTTPでのクッキーの扱い方。 クッキーの受信 クッキは、Set-Cookie:というフィールドに書かれている。 ただし、複数のSet-Cookieフィールドが存在することが普通なので、Net::HTTP#get_fieldsを使って配列の形で取得する。 require 'net/http' Net::HTTP.start('www.tohoho-web.com'){|http| response, = http.get '/cgi/wwwcook.cgi' p response.get_fields('Set-Cookie') } 実行例: ["KAISUU=2; expires=Tue, 1-Jan-2030 00:00:00 GMT;", "HIZUKE=2007%2F02%2F16%2021%3A46%

30分プログラム、その362。http://www.haskell.org/ghc/docs/latest/html/libraries/network/Network-Socket.htmlを使って、簡易HTTPサーバを書いてみた。 これだけ、IO aが多いとHaskell使ってる意味がほとんどない気がするけどね。 使い方 *Main> httpServerとしたあと、http://localhost:8080にアクセスする。 ソースコード import Network.Socket server action = do sock <- socket AF_INET Stream 0 addr <- inet_addr "127.0.0.1" bindSocket sock $ SockAddrInet 8080 addr listen sock 1 sequence_ $ repeat

いまだに継承を使うタイミングが分からない。もうちょっと正確にいうと実装継承を使うべきタイミングが分からない。 インタフェースを継承するのは理解できるよ。型をそろえたり、同一視したいんでしょ。 よくあるコードだとこんな感じ。ちゃんと動くかどうかは知らない。 interface Foo { ... } class Bar implements Foo { ... } class Baz implements Foo { ... } List<Foo> foo = new List<Foo>(); foo.push(new Bar()); foo.push(new Baz()); でも、クラスを継承するのがよく分かんない。メソッドとかを再利用したいんなら、委譲を使ったほうが安心じゃん。不用意なメソッドを公開したりしないし。 class Foo { public void f() { ... }

30分プログラム、その622。RubyにHaskell風のリスト操作を移植しました。 Rubyでコードを書いてるときに、take_whileとかが欲しくなることが何度かあったので、実装してみました。 メソッド内部で副作用を使っているのが何個かありますが、外から見たらちゃんとFunctionalなので許してください。 使い方 p (1..4).take(2) p (1..4).drop(2) ソースコード #! /opt/local/bin/ruby -w # -*- mode:ruby; coding:utf-8 -*- # # prelude.rb - # # Copyright(C) 2009 by mzp # Author: MIZUNO Hiroki / mzpppp at gmail dot com # http://howdyworld.org # # Timestamp: 2