サクサク読めて、アプリ限定の機能も多数!
トップへ戻る
ブックレビュー
www.tom.sfc.keio.ac.jp/~sakai
λ. Closed Freyd- and kappa-categories, John Power and Hayo Thielecke を読んだ。この論文はArrowについて書かれたわけではないのだけど、これでArrowについては大体分かった。Monad が Kleisli category で「計算」を扱うのに対して、Arrowはsymmetric pre-monoidal category で「計算」を扱う。Haskell のデータ型と関数のなすカテゴリからこのカテゴリへの関手を加えた構造を Freyd-category と呼ぶ。で、Freyd-categoryはκ-calculusのモデルの一般化であるκ-categoryと等しくて…… いやー、面白いなぁ。
λ. 『抽象によるソフトウェア設計』がついに出版されます 先日、レビュワーを募集していた "Software Abstractions"の翻訳本ですが、ついに来週『抽象によるソフトウェア設計』として出版されることになりました。 2009年のFLTVで告知してから二年も経ってしまいましたが、ついに出版されることになったかと思うと非常に感慨深いです。これは訳者の贔屓目ですが、それだけの時間に見合う素晴らしい仕上がりの本になっていると思います。 抽象によるソフトウェア設計−Alloyではじめる形式手法−(Daniel Jackson/中島 震/今井 健男/酒井 政裕/遠藤 侑介/片岡 欣夫) この本はAlloyという言語・ツールを用いた形式手法の教科書です。 Alloyというのは、モデル発見器と呼ばれているツールの一つで、条件を与えるとその条件を満たす具体例を探してくれます。モデルというのは、条
λ. Cleanの定関数と定グラフ <URL:http://d.hatena.ne.jp/lethevert/20060601/p1> より。 Haskellはグラフ書き換えによる意味論を言語仕様に採用していないので、言語仕様上はCleanの定関数や定グラフのような概念は存在しない。というか、そもそもHaskellの言語仕様は実行メカニズムをほとんど規定していない。では実際の処理系ではどうかというと、例えばGHCでは(ある種の最適化後に)ラムダ抽象以外の形をしている定義は、すべてCleanでいうところの定グラフとしてコンパイルされる。 full laziness transformation また、full laziness transformation (full laziness optimisation, let-floating) によって、局所的な定義が大域的な定義に引き上げられ
www.tom.sfc.keio.ac.jp
λ. Whyでバブルソートの正当性を示す 計算機言語で定理証明 (Proof Party.JP)のときには、Jahobというツールを使って色々やってみたが、最近Whyという似たツールを知ったので、こっちでも同じようなことをやってみる。 まずは、Jahobでも試したバブルソートの例*1。 BubbleSort.java これを gwhy BubbleSort.java としてgwhyを起動すると、Proof Obligation が抽出されて一覧されるので、あとはメニューから「Proof」「Prove all obligations」とかを選べば定理証明器などが走って証明をしてくれる。 定理照明器としては、Alt-Ergoしかインストールしていなかったけれど、この例ではあっさり全 Proof Obligation が証明された。 以下が結果の画面。 gwhyのこのインターフェースはテストツー
λ. STモナドとSTRefをHaskell上で実装する [FAQ]Haskellには副作用があるのか、ないのか の話。 kazu-yamamotoさんはSTモナドを、「処理系の力を借りないといけないモナド」で、副作用や参照透明性の観点からはStateモナドと本質的に違うものだと主張している。 だけど、STモナドが処理系に組み込まれている理由は効率のためであって、意味的にはStateモナドと大差ないし、効率とあと細かい点を気にしなければHaskellレベルでも実装できるはず。 というわけで書いてみたのが以下のコード。 {-# LANGUAGE Rank2Types, ExistentialQuantification #-} import Control.Monad.State import qualified Data.IntMap as IntMap import Unsafe.Coe
λ. 関数型プログラマにとっての副作用 「Haskell に副作用なんて、あるわけないじゃん。大げさだなぁ」(死亡フラグ)と思っていたけれど、HAMA#3の話をみて自分の考え方を整理できた気がするので、ちょっと書いてみる。 入出力は副作用? 命令型プログラマに説明するときの便法としては、kazuさんの説明は確かに効率が良いとは思うものの、自分がこの説明をするのには結構抵抗がある。 どこに抵抗があるのかというと、その背後にある「入出力するなら副作用がある、Haskellは入出力する、だからHaskellには副作用がある。」というような考え方。 この考え方では、言語がどのようなものであろうと、最終的に実行時に計算機上の現象として入出力が発生すれば、副作用が存在するということになってしまう。 しかし、関数型プログラマにとって、副作用とはあくまでも言語や式の性質であって、実行時に計算機上で発生する
λ. iPhoneのSMSのバックアップ iTunesがバックアップしているファイルが、Windowsならば c:/Users/ユーザ名/AppData/Roaming/Apple Computer/MobileSync/Backup/iPhoneのID?/3d0d7e5fb2ce288813306e4d4636395e047a3d28.mddata とかにあるので、このファイルをバックアップしておけばよい。 このファイルはSQLiteのファイルなので、sqlite3 -csv -separator ',' 3d0d7e5fb2ce288813306e4d4636395e047a3d28.mddata "select * from message;" > output.csv でCSVに変換できる。
λ. “Referential transparency, definiteness and unfoldability” by Harald Søndergaard and Peter Sestoft Chatonのhaskell-jpルームで2009-07-03と2009-07-04にあった、参照透明性と副作用の定義に関わる話で出てきた論文。積読論文の中にあったので読んでみた。 参照透明性(referential transparency)はQuineによって考えられた概念で、LandinとStracheyによってプログラミング言語の性質として使われるようになった。が、その定義・使われ方は変化しており、それらは同値ではないという話。 それらを、この論文での呼び方で呼ぶと以下のような感じ。 確定性 (definiteness) 変数がそのスコープの中で単一の値を持つこと。xを変数とすると
日々の流転 最近、携帯を変えました。MNPを使わなかったので番号が変わります。新しい番号は前の番号(090〜)から、電卓で1003227378をマイナスしたものです。また、メールアドレスはgmailのものを使っています。
λ. 帰りに泳いできた 今日は帰りに久しぶりに泳いできた。 先週と先々週は調子が悪かったのと病み上がりで泳ぎに行かなかったので、3週間ぶり。 使ってなかった筋肉を久しぶりに使ってる感があった。 1kmを25分くらいで。 λ. 『数理論理学』 (古川康一, 向井国昭) 半年くらい前に出た古川先生と向井先生の本をざっと読んだ。 「問題を論理を使って表現して、推論によって問題解決する」という古きよき視点から、命題論理、一階述語論理、論理プログラミング、発想論理プログラム、帰納論理プログラムについて入門者向けに解説した本で、この視点からは良く纏まっている。 厚くないので読みやすいのではないかと思う。 また、個人的には一般論理プログラムの安定モデルによる意味論などをちゃんと説明しているのは、ちょっと好印象。 ただ、論理と計算のしくみ(萩谷 昌己/西崎 真也)などと違って、計算機科学・情報
From: Jun Mukai <mukai@j...> Date: Wed, 23 Jan 2008 22:27:22 -0800 Subject: [haskell-jp:157] Re: Stateモナドを使った実例コーディングは? 向井といいます。 State モナドは名前が混乱の原因だと思います。 これは私見ですが、まずは Writer モナドと Reader モナドを理解すると State モナドは理解しやすいと思っています。さらに、その前段階として Identity モナドも踏まえていると見通しがはっきりします。 以下、ちょっと長くなりますが、どういう意味か説明してみます(わかりにくかっ たらごめんなさい)。 Identity モナドというのは、関数合成のことだと思うことができます。細かい 型を気にしなければ、 return x >>= f >>= g は g (f x
λ. SmallCheck and Lazy SmallCheck: automatic exhaustive testing for small values SmallCheck and Lazy SmallCheck: automatic exhaustive testing for small values. Colin Runciman, Matthew Naylor and Fredrik Lindblad. in Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell を読んだ。 QuickCheck がランダムテストなのに対して、SmallCheck は指定した上限までの範囲の網羅的な検査を行う*1。 QuickCheckでは値が適切に分散するように値の生成機を書くのは簡単ではないが、Sm
日々の流転 最近、携帯を変えました。MNPを使わなかったので番号が変わります。新しい番号は前の番号(090〜)から、電卓で1003227378をマイナスしたものです。また、メールアドレスはgmailのものを使っています。 λ. 「型の型」問題 LL Future のスタッフ&発表者の打ち上げ*1で「型の型」についての話が出たらしい。 あろはさんのTwitterの<URL:http://twitter.com/alohakun/statuses/904102768>や、東京行ってきた - 黎明日記とそのコメント欄で、その辺りの話が出ていたので、ちょっと簡単な説明を書いてみる。 HaskellとかCCの場合 まず、Haskellの場合。 Haskellでは型の型は「種(kind)」と呼ばれていて普通の型とはレベルの異なるものになっている。つまり、型の型は普通の型ではない。 種について簡単に説明
λ. HaskellのMonad Haskellのモナドの話になって、原さんは「私にわからんのは(Haskellが)おかしい」と言っていた。原さんにわからないなら、私にわかるわけがないな。 原さんがわからないってのは、ちょっと信じられないです。Monadの数学的定義を知っているならば、Haskellのは単に「各種の計算体系のモデルを、適当な strong monad の Kleisli category として作れる」ということに過ぎないと思うので。 例えば、Computational lambda-calculus and monadsにも載っている例をいくつか取り上げると…… (例1) 非決定性計算 T: C→C T(X)=℘(X) (℘はべき集合関手) ηA: A→℘(A) ηA(x) = {x} μA: P2(A)→℘(A) μA(S) = ⋃S で定義される Monad (
日々の流転 トラックバックスパムを大量に喰らったので、トラックバックを一時的に無効にしています。 λ. “A functional quantum programming language” by Thorsten Altenkirch and Jonathan Grattage We introduce the language QML, a functional language for quantum computations on finite types. Its design is guided by its categorical semantics: QML programs are interpreted by morphisms in the category FQC of finite quantum computations, which provides a co
From: shelarcy <shelarcy@g...> Date: Wed, 18 Jun 2008 13:10:54 +0900 Subject: [haskell-jp:218] GHC 6.8.3 リリース こんにちは。 GHC 6.8.3 がリリースされました。 http://www.haskell.org/ghc/download_ghc_683.html 今回も主にバグ修正を目的としたリリースです。前の 6.8.2 のような大幅な 機能追加はありませんが、いくつか気の利いた変更が加わっています。 * -prof オプションと -threaded オプションの併用が可能に マルチスレッド環境でプロファイラが正常に動かないことから意図的に -prof オプションと -threaded オプションを併用できないようにしていましたが、 これに起因するビルド失敗が多く報告され
λ. OCamlでランクn多相 レコードでもliftしたい - みずぴー日記 のコメントに関する補足。 関数を受け取って、レコードの型の異なる複数のフィールドに対して適用する高階関数を書きたいという話。 型の異なるフィールドに対して適用するには、受け取る関数は [Int]→[Int]→[Int] のような型の単相的な関数ではなく、∀a. [a]→[a]→[a] のような型の多相的な関数である必要がある。で、多相的な関数を受け取る高階関数の (∀a. [a]→[a]→[a])→Record→Record→Record のような型は、二階ラムダ計算の言葉でいうと、ランク2の型になっている。 ランクの正確な定義は Type reconstruction in finite-rank fragments of the polymorphic λ-calculus (c.f. The “Curry
次のページ
このページを最初にブックマークしてみませんか?
『www.tom.sfc.keio.ac.jp』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く