Rubyにはウンザリ！動的型付け、副作用、およびオブジェクト指向プログラミング全般からの考察 | POSTD
この記事を書き上げるには、相当長い時間がかかりました。本来は今年の年明け、 Rubyの死 やデイヴィッド・ハイネマイヤー・ハンソンの TDDは死んだ がアップされて騒ぎになる前に投稿するつもりだったのです。昨年末に書いたツイートを見てください。 > Rubyにはもう飽き飽きした。理由はいろいろあるが、特にその副作用と、ステータスが可変なせいで大量のユニットテストを書かされるのにはウンザリだ。 @abevoelker Rubyの開発に関しては、大勢の人が心のどこかで何かおかしい、何かが欠けていると思っているようですが、たいていの人は責める対象を間違っています。Rubyで書いたアプリがとんでもない代物になったって？ それはあなたがきちんとテストコードを書かなかったか、テスト駆動開発（TDD）の指針に則って開発しなかったからです。もしくは、正しいデザインパターンに切り分けるための知識が不足してい
Haskell/カリー=ハワード同型 - Wikibooks
カリー=ハワード同型(Curry-Howard isomorphism)は数学の一見無関係に思えるふたつの領域、型理論と構造論理を結びつける実に驚くべき関係である。 導入[編集] これよりカリー=ハワード同型は単に C-H と表記する。C-H が示しているのは、定理の本質を反映するような型を構築し、それからその型を持つ値を見つけさえすれば、どんな数学的定理をも証明することができる、ということだ。これは最初は極めて不思議に思える。型と定理にどんな関係があるというのだろうか？しかしながら、以下に述べるように、このふたつは非常に近しい関係にあるのである。はじめる前に簡単に注意しておくが、導入の章では error や undefinedのような 表示的意味論 が ⊥ である式の存在は無視する。これらはとても重要な役割を果たすのだが、これらについては後ほど別に考えることにする。また、unsafeCo
Haskell/Denotational semantics - Wikibooks
導入[編集] この章ではHaskellプログラムの意味がどのように形式化されるかという表示的意味論(denotational semantics)を説明します。「square x = x*x というプログラムの意味は、数をその平方数に写す数学の平方関数だ」ということを形式的に規定することはつまらないことにみえるかもしれませんが、それでは f x = f (x+1) のような無限ループするプログラムの意味はどうでしょうか？ 以下ではまずこの疑問に対するScottとStracheyのアプローチを例示し、概して関数プログラムの、特に再帰的な定義の正しさについて論じる基盤を得ることにしましょう。もちろん、これらのトピックではHaskellプログラムを理解するために必要なものに集中します。[1] この章の他の狙いは、ある関数がその引数を評価する必要があるかどうかというアイディアを捉えた正格と遅延の概
みんなのAgda Wiki
2014/07/17 講義記録 2014/07/10 第12回講義 2014/07/03 第11回講義 2014/06/26 第10回講義 2014/06/19 第9回講義 2014/06/12 第8回講義 トップページ test 第７回講義 2014/05/29 第6回講義 2014/05/28 第３回講義 第２回講義 2014/05/27 第５回講義 2014/05/15 インストール 第４回講義 2014/05/02 コマンド一覧 2014/04/24 記号 第１回講義 2014/04/20 メニュー 2014/04/17 編集用テンプレート
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
