JSXよりHaxeがイケてる3つの理由 - みずぴー日記
Javascriptを生成できる言語『JSX』がリリースされました。めでたいですねー。 ただ同じくJavascriptを生成きるHaXeのことが忘れられている気がするので、宣伝します。 ステマじゃないよ! 型推論がイケてる 現時点でJSXには型推論が実装されてないので、関数を定義するには全ての型を書く必要があります。 // JSXだよ! function add(x : number, y : number) : number { return x + y; } これだけなら特に問題ないように見えますが、これが高階関数を定義しようとするとどんどん複雑になっていきます。 // JSXだよ! function f(g: function(:number):number): function(:number):number { return function(x: number): number
VSTTE Competition参加記録 - みずぴー日記
id:yoshihiro503さんに誘われて、VSTTE Competitionというソフトウェア検証コンテストに参加しました。 「検証ツールに特に制限はないぜ」と書かれていたのでCoqを使いました。 競技プログラミンングに初めて参加しましたが、48時間ぶっとうしで同じ課題に取り組むのはとてもエキサイティングで楽しかったです。 参加メンバー [twitter:@yoshihiro503]さん [twitter:@pirapira]さん [twitter:@hirose_golf]さん ボク([twitter:@mzp]) 一日目 開始直前 yoshihiro503さんから"uiro,tebasaki,miso,..."と列挙された謎のメールが届く。 どうやらチーム名の候補だったらしいです。 yoshihiro503さんとSkypeで話しながらbitbucketの準備をしたりする。 0:00
MessagePack for OCamlを公開しました - みずぴー日記
くえにしさん([twitter:@kuenishi]さん)に誘われたのでMessagePackハッカソンに参加してきました。 MessagePack本体のレポジトリにMessagePack for OCamlを取り込んでもらったので、みんな使ってください! MessagePackって? JSONやYAMLと同程度の表現能力をもった省スペースなオブジェクトシリアライザです。対応言語もC/C++/Java/D/Ruby/Haskellなどと非常に多いです。 対応言語言一覧 → http://wiki.msgpack.org/display/MSGPACK/QuickStart 公式Wikiの採用実績によると、かなりメジャーなプロジェクトも採用されているようです。実際、ハッカソンにも仕事で利用されている方が結構来ていました。 実はボクたちの作っているチャットアプリのAsakusaSatellit
名古屋Reject会議で「証明駆動開発のたのしみ」というタイトルで発表してきました - みずぴー日記
証明駆動開発のたのしみ@名古屋reject会議 View more presentations from Hiroki Mizuno
名古屋Reject会議を開催しました - みずぴー日記
名古屋Ruby会議02のとなりで名古屋Reject会議というイベントを開催してきました。 「Rubyという言葉を使ったら負け」みたいな雰囲気のある謎なイベントでした。たのしかった! 当日は[twitter:@maeda_]さんがustream中継を、[twitter:@wof_moriguchi]さんがタイムキーパーをやってくれて、ものすごく助かりました。主催者は笑いながら発表を聞いてただけです、ごめんなさい。 発表資料まとめ 漏れがあったら教えてください。 @bleis『そうだ、bf処理系つくろう！もちろんSQLで！』 @sunflat『Amazon EC2 (Nagoya reject02)』 @yoya『PHP: ZendEngineの話』 @terurou 『名古屋Reject会議でCommonJSの話をしてきました - terurouメモ』 @nari3『GC本スピンオフ』 @m
リストモナドを使ってみる - みずぴー日記
このエントリはScala Advent Calendar jp 2010 : ATNDの25日のものです。 メリークリスマス! クリスマスは楽しくみんなでパズルを解いて遊びましょう。 パズルみたいな探索問題をScalaで解く場合は、リストモナドを使うとキレイに書けます。 例: SEND+MORE=MONEY 例として覆面算を解いてみましょう。 各アルファベットに異なる数字が割り当てれる。その数字は何か? ただし最上位桁が0ではない。 普通にforループを使って解くと、ネストの深さが酷いことになります:)。 // int(1,2,3)を123にする関数 def int(xs : Int*) : Int = xs.foldLeft(0)( _ * 10 + _) // SEND+MORE=MONEYの答えを探索する def solve : (Int,Int,Int) = { for( s <-
NGK忘年会2010でCoqの紹介をしてきました - みずぴー日記
NGK忘年会2010（昼の部） : ATNDという名古屋の全コミュニティ合同の忘年会に参加してきました。 発表したこと NGK忘年会 2010 / CoqからRubyへView more presentations from mzpi.発表動画@Ustream CoqPartyのスライドの使いまわしです。 Coq楽しいよ、盛り上ってるよ、って話をだらだらしてきました。 Coq入門記事 上のスライドでCoqに興味を持ってくれた人が数人いるらしいので、入門記事へのリンクを貼っておきます。 プログラマのための Coq - zyxwvの日記 ガリク先生の講義資料 浅井先生のゼミ資料 あとProofCafeもよろしくお願いします。 懇親会の感想・メモ Scala座でニアミスした[twitter:@PG_kura]さんとやっと話せた [twitter:@fate_fox]がしっかりしすぎててビビる B
lessでPDFを読もう - みずぴー日記
awk-users.jpのhi_saitoさんのポストでlesspipe.shなるものを知った。 これを使うと、lessでPDFとかを読めるらしい。全部確認したわけじゃないけど、以下のファイルをlessで読めるらしい。 PDF File - *.pdf Word Document- *.doc Image Files - *.gif, *.jpg, *.jpeg, *.png TAR Files - *.tar TAR Files with gzip - *.tar.gz Zip Files - *.zip Gzip and Gzip2 Files - *.gz and *.bz2 ISO Files Debian Files - *.deb RPM Files - *.rpm インストール $ sudo port -d lesspipe.sh とかでlesspipe.shをインストールし
F#はじめました - みずぴー日記
30分プログラム、その805。 インストール Redirecting…のインストーラでインストールする。 http://msdn.microsoft.com/en-us/fsharp/cc835251.aspxを$FSHARP_HOMEに展開する 使い方 $ mono $FSHARP_HOME/bin/fsc.exe $ cp $FSHARP_HOME/bin/FSharp.Core.* . $ mono fact.exe 3628800 ソースコード let rec fact n = if n = 0 then 1 else n * (fact (n - 1)) printf "%d\n" (fact 10);; 参考 過去の30分プログラム
今年は名古屋でOCamlMeeting! - みずぴー日記
um2010 - OCaml.jp 去年は東京で開催されたOCamlMeetingですが、今年は名古屋で開催されるそうです。 上記URLでプログラムも公開されていますが、かなり豪華なことになっています。 http://igeta.cocolog-nifty.com/blog/でおなじみのF#のいげ太さん。Windowsユーザかつ関数型プログラマはレアな気がするので、F#の話はなかなか貴重だと思います。 プログラミングの基礎 ((Computer Science Library))の浅井先生。この本は関数型プログラミングの入門書としてだけでなく、プログラミグ一般の入門書としてもすばらしかったので、ステキな話が聞けると思います。 ガリク先生によるOCaml 3.12の話。OCamlの開発者(の一人)から直接、OCaml 3.12の話が聞けるのは相当レアだと思います。しかも日本語で。 id:ca
Coqでラムダ計算を証明してみた - みずぴー日記
前からずっと取り組んでいた「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. 証明した定理 型
Coqのおかげで見つけれたバグ - みずぴー日記
最近、Coqで型付きラムダ計算を定義して、ProgressやPreservationを証明するという遊びにはまっています。とてもおもしろいので、みんなもやるといいと思うよ。 で、最近、substitution lemmaの証明にチャレンジして、もろくも敗れ去りました。よくよく見直してみると、そもそもsubstitutionの定義が間違っていました。このバグはなかなか根が深くて、前に作ったトイ・コンパイラ(scalet)でも同じ間違いをしてました。 というわけで、これはCoqのおかげで見つけれたバグだし、人手は見付けづらいバグと言えないこともないので記録しておきます。 バグを含んだSubstitution まずはバグを含んだSubstitutionです。どこが間違っているか分かりますか? ボクは分かりませんでした。 (* subst *) Inductive Subst : term ->
今日のCoq: 型づけ規則とそれに関する補題 - みずぴー日記
とうとう、型づけ規則の定義ができました。 というわけで、簡単な補題を証明しようとしたところ、string_decがうまく扱えなくて挫折しました。 証明したかった補題はTAPLに載っている「Inversion of the typing relation」という補題です。TAPL曰く、Immediate from the definitionらしいです。 (* typing t tenvは、型環境tenvにおいてtが型づけ可能ならSome type、型がつかないならNoneを返す。 *) Lemma InvTypeRelVar : forall (tenv : list (string * type)) (x : string) (r : type), Some r = typing (Var x) tenv -> In (x,r) tenv. というわけで証明にチャレンジします。 まずは、
今日のCoq: ラムダ式とsubstitute - みずぴー日記
バリアントでラムダ式を作って、その上でsubstituteを定義してみました。目指してるのは単純型付きラムダ計算です。 覚えたこと 全部、末尾に「〜らしいよ」ってつけて読んでくれるとうれしいです。 再帰のあるバリアントはInductiveで定義する 相互再帰のあるバリアントはwithでつなげる andはProp上の演算。andbはbool上の演算 文字列を扱いたいときはRequire Import Stringする よく分かんないこと 文字列上の等価性チェックをどうしたらいいかが分からない。Stringモジュールにあったprefixを使って、 Definition string_eq (xs ys : string) := andb (prefix xs ys) (prefix ys xs). としてるけど、これを評価するとすごいことになる。 Eval cbv delta iota bet
今日の証明: reverse (reverse xs) = xs - みずぴー日記
最近Coqが流行してるので、ボクも流れに乗ってみました。 今回、ボクが証明したかったのは、2回reverseすると元に戻るという性質です。 Theorem RevReflect : forall {A : Type} {xs : list A}, reverse (reverse xs) = xs. そののために、appendを定義したり、Lemmaを証明したりしてます。 状況に応じて、TheoremやLemma、Fact、Remark、Corollary、Propositionを使い分けるのがクールらしいですよ。参考 あとReverseAppendを証明するときは、全部introsしちゃうのじゃなくて、xを残しとくという覚えたてのテクニックを使ってます。引数の順番大事! Require Import List. Fixpoint append {A : Type} (xs : list
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
名古屋Ruby会議で「Coq to Rubyで初める証明駆動開発」というタイトルで発表してきました - みずぴー日記