タグ

ブックマーク / kazu-yamamoto.hatenablog.jp (12)

  • コンパイルは(テストではなく)証明である - あどけない話

    「プログラムのテストはバグの存在を示すことにかけてはとても効率的な方法ですが、バグの不在を示すことにかけては絶望的なほどに不適切です。プログラムの信頼性を顕著に向上させる唯一の方法は、その正当性に対して説得力のある証明を与えることです」 -- Edsger W. Dijkstra 静的型付き言語では、コンパイル時に型が検査される。この型検査に関連して型推論という機能を持つ言語がある。型推論は、大きく分けて2つの意味で使われているようだ。 命令型言語の多くに見られる型推論:型検査の過程で、省略された型を補うこと 関数型言語の多くに見られる型推論:未知の型を変数として方程式を立て、方程式を解いて未知の型を求めること。型推論自体が型検査の役割を果たす この記事では、後者の型推論を話題にする。 静的型付き関数型言語の利点として、よく「コンパイルはテストである」という説明がなされる。プログラムは式で

    コンパイルは(テストではなく)証明である - あどけない話
    tanakaBox
    tanakaBox 2013/03/16
    ふむふむ。
  • GHC でスタックトレース - あどけない話

    これまで GHC では、スタックトレースを取ることが有効なデバッグ方法ではなかった。 なぜなら遅延評価では、(再帰であってもなくても)末尾呼び出しは単なるジャンプになるから、スタックを使わないのである。スタックに戻る場所を積むのは、case と of の中で評価される式だけだ。(つまり、ここは正格に評価される。) この問題を解決するために GHC 7.4.2 から、わざわざスタックにログを残して、スタックトレースが取れるようになった。すなわち、最新の Haskell Platform をインストールしていれば、この機能を使えるということだ。 例として、以下のプログラムを考えよう。 module Main where main :: IO () main = print $ foo 3 + 1 foo :: Int -> Int foo x = x * 2 + bar x bar :: In

    GHC でスタックトレース - あどけない話
    tanakaBox
    tanakaBox 2013/02/07
    これは便利そう。
  • 名詞の王国 - あどけない話

    「君のプログラミング言語で、これ、できる?」で紹介されていた「Execution in the Kingdom of Nouns」を訳してみました。英語よりも、つたない日語訳の方がよい方は、どうぞ。 おかしな訳があれば、教えて下さい。適宜、訂正します。 「C の関数はファーストクラスじゃないよ」などの突っ込みは、原文の著者へどうぞ。 名詞の王国での実行 彼らには気分ってものがある。ものによるが...特に動詞がそうだ。誇り高いことったらない...形容詞相手ならなんとでもできるが、動詞はどうしようもない...じゃが、このわしにかかれば皆思いのまま! -- ハンプティ・ダンプティ 世界のみなさん、こんにちは!今日は、邪悪な王 Java の物語と国中の動詞を滅ぼした彼の冒険について語ろう。 警告:この物語は幸福な結末を迎えない。心臓の弱い人や批判家向けではない。もし、あなたが怒りっぽい性格である

    名詞の王国 - あどけない話
    tanakaBox
    tanakaBox 2010/02/05
    面白い読み物。
  • jemalloc() ~ Firefox 3.0 爆速の理由 ~

    今日、IIJ 技術研究所で jemalloc() について簡単に説明しました。その資料を公開します。 jemalloc() 〜 Firefox 3.0 爆速の理由 〜

    jemalloc() ~ Firefox 3.0 爆速の理由 ~
    tanakaBox
    tanakaBox 2010/02/05
    mallocいろいろ
  • シカクいアタマをマルクする - あどけない話

    日能研の中刷り広告に中学入試の問題が載っていて、興味を引かれました。要約するとこうです。 6桁の数字がある。それぞれの桁の数字は異なる。 これを abcdef と表す。 この数字に 3 を掛けると bcdefa となる。 この数字に7を掛けると6桁の数字になる。 この数字に2を掛けた数字を答えなさい。 当に小学生が解く問題かと目を疑いました。 もちろん大人が解けば簡単です。以降を読む人は、ここで問題を解いてみて下さい。 この問題のおシャレなところ abcedf は 142857 です。 この問題がシャレているところは、 「この数字に 3 を掛けると bcdefa となる」の部分で 3 を選んでいるところ abcedf が答えではなく、わざわざ 2 倍して答えさせるところ 「この数字に7を掛けると6桁の数字になる」という条件は、「5を掛けても」と書く方が厳密で分かりやすいのに、わざわざ 7

    シカクいアタマをマルクする - あどけない話
    tanakaBox
    tanakaBox 2010/02/05
    面白かった。
  • cabalコマンドの使い方 - あどけない話

    Cabal は Haskell のパッケージ管理システムです。枠組みとしての Cabal と、コマンドの cabal があり、間違いやすいです。 Cabal は、パッケージをコンパイルし、インストールする枠組みです configure, make, make install に相当 cabal は、パッケージの依存関係を調べ、必要なパッケージをダウンロードして、インストールするためのコマンドです cabal-install と呼ばれることもあります ここでは、コマンド cabal の使い方を説明します。 インストール 各 OS のパッケージ管理システムを使って cabal をインストールしましょう。GHC を扱っているパッケージ管理システムであれば、cabal にも対応しているはずです。 MacPorts では、以下のようにします。 % sudo port install hs-cabal

    cabalコマンドの使い方 - あどけない話
  • 制約プログラミングのススメ - あどけない話

    IIJ 社内でやったチュートリアル 純粋関数型言語Haskellの紹介 〜制約プログラミングのススメ〜 の資料を公開しました。

    制約プログラミングのススメ - あどけない話
    tanakaBox
    tanakaBox 2010/02/05
    新たな発見の多かった資料。
  • プログラマの壁 - あどけない話

    プログラマに向いている人と向いていない人がいるそうです。 Jeff Atwood さんの「どうしてプログラマに・・・プログラムが書けないのか?」: プログラムを書ける者とプログラムを書けない者の間にある大きな溝についてはよく知られているが、プログラマの職に応募してくる人間は、すでにこの溝を飛び越えているものだとばかり思っていた。明らかにこれは妥当な仮定ではないらしい。プログラムを書けないプログラマの面接で時間を無駄にしないために、FizzBuzzスタイルのふるい分けが必要ということだ。 どんなことでも向き不向きはあるでしょうから、これには納得いきます。しかし、プログラマになれる人の中にも、溝があるようです。 Joel Spolsk さんの「Javaスクールの危険」: 私のささやかな経験から言わせてもらうと、伝統的に大学のコンピュータサイエンスのカリキュラムで教えられているもので、多くの人が

    プログラマの壁 - あどけない話
    tanakaBox
    tanakaBox 2010/02/03
    いっぱい壁を乗り越えないとな。壁だらけ。
  • 素数判定 - あどけない話

    要約:素数判定に使われるミラーラビン法を解説しながら、Haskell で実装してみる。 フェルマーテスト 大きな数を確実に素数だと判定するには、大変時間がかかるので、実用的には「ほぼ素数だ」と確率的に判定する。確率的な素数判定の代表格がフェルマーテストである。 フェルマーテストには、以下に示すフェルマーの小定理を利用する。 a^p ≡ a (mod p) a は任意の整数。p は素数である。法 p の下で a を p 乗したものは、a と合同であると言う意味だ。a には制限はないが、特に a を p より小さい整数、0 ≦ a ≦ p - 1 とすれば、a を p 乗して、p で割ると a に戻るとも解釈できる。 最初に見たときは、だからどうしたと思われるかもしれない。しかし、有名なフェルマーの大定理が実用上何の役にも立たないのに対し、フェルマーの小定理はいろんな場面で活躍する。 実際に計

    素数判定 - あどけない話
    tanakaBox
    tanakaBox 2010/02/03
    フェルマーテストとか
  • Haskell とモナド - あどけない話

    今日までに理解した Haskell とモナドについて、まとめてみます。間違っているところもあると思いますので、コメントを期待しています。(_ _) Haskell の特徴 純粋関数型言語です。 参照透過性 変数は初期化できますが、一旦決まった値は変更できません。関数の返す結果は、引数の値だけで決まります。 遅延評価 データの処理は、当にデータが必要になったときに実行されます。UNIX のパイプみたいなものだと考えるといいでしょう。 Haskell にも副作用はあります。 よい Lisper は、副作用のある関数とない関数を分けて実装します。しかし、そうでない Lisper が分けてくれるとは限りません。 Haskell を使うと、副作用のある部分とない部分を必然的に分けて書くことになります。 変数の値は変更できない たとえば、有名な quicksort を例にとりましょう。 quicks

    Haskell とモナド - あどけない話
    tanakaBox
    tanakaBox 2010/01/24
    return,=>>,>>,Maybe,IOについて。
  • Haskellと副作用 - あどけない話

    よく、Haskellには副作用がないと言われるが、それは間違いだ。確かに、Haskell には状態の変化(あるいは再代入)という副作用はない。しかし、入出力という副作用はある。この記事では、Haskell の副作用に対して、命令型プログラマーにすっきりと理解できる説明を試みたいと思う。 間違った方向への第一歩 Haskell の副作用に関する典型的な説明は、こんな感じだ。 Haskell にはあらゆるレベルで副作用がない。そのため、遅延評価が可能になる。遅延評価では、コードが記述順に実行/評価されるとは限らないので、入出力と相性が悪い。そこで、IO モナドが導入されている。IO モナドのおかげで、入出力に関するコードは記述順に実行され、外界に作用できる。 この説明を聞いて理解しろという方が無理である。説明が苦しい最大の理由は、Haskell にはあらゆるレベルで副作用がないと、間違った一歩

    Haskellと副作用 - あどけない話
    tanakaBox
    tanakaBox 2009/12/18
    副作用のお話からIOへ。 >IO がファーストクラスであることを理解する方が、よほど大切である。
  • 遅延評価と末尾再帰と余再帰 - あどけない話

    遅延評価では再帰の効率はどうなるかという問題です。Real World Haskell で、末尾再帰は重要だと言った後に、遅延評価では末尾再帰なんて気にするなとちゃぶ台を返しています。ようやく haskell-cafeで答えを見つけたので、Luke Palmer さんの許可を得て訳を公開します。 Luke Palmer さんの説明 私が Haskell でプログラミングするときは、通常関数を末尾再帰にはしません。(Int や Bool など)正格な値へ畳み込む場合、末尾再帰を使うのはよいことです。しかし帰納的な遅延構造を作成する場合、関係する用語は(私の記憶が正しければ)「余再帰」(corecursion)であり(訳注:mapは再帰かつ余再帰だそうですが、専門的すぎるので普通の再帰でいいと思います)、末尾再帰とはまったく異なります。 リストに対し末尾再帰で map する関数を例として考えま

    遅延評価と末尾再帰と余再帰 - あどけない話
    tanakaBox
    tanakaBox 2009/12/15
    余再帰(corecursion)
  • 1