書評「型システム入門」 - 純粋関数空間
追記：Amazonのリンクを張っていますが、オーム社のサイト http://estore.ohmsha.co.jp/titles/978427406911P からも購入できます。 AmazonのKindle版はまだ出ていないようですが、 こちらからは今現在でDRMなしのPDFも購入できます。 Kindle版リリースの際にも、 フローレイアウトになる予定はないそうですので、 Amazonにこだわりがあるのでなければ、 電子版で読みたいという方は、こちらから購入されるのが良いかと思います。 あらかじめお断りしておきますと、 この記事は書評ではなく、宣伝です。 数年前に原著を読んだ時から、 本書は私の中では間違いなく良書ということになっておりますので、 私がいまさら内容の善し悪しを語ることには、 はじめから意味がないと思っております。 なのでここでは、この本の魅力、読んで欲しい人、どういう風に読
関係データベースの第1正規形はナンセンス - 檜山正幸のキマイラ飼育記 (はてなBlog)
一昨日の「主キー／外部キーなんてドーデモイイ」と昨日の「絵で分かる！ 主キー／外部キーのアホらしさ」において、主キー／外部キーというのは、いわばメモリ番地とポインターのような、仕掛け・手段が露出しているだけのものだ、と説明しました。仕掛けが露出している結果、概念的には単純なもの（例えば単なる写像）の実現が複雑でしかも恣意的になっています。 今日は正規形、なかでも一番基本的な第1正規形の話です。控えめなデイヴィッド君に代わって、ジイサマ（檜山）が批判的に検討しましょう。 アトミックって何ですかぁ？ 圏論を使えばどうなる スピヴァックは型システムとデータベースシステムの統合を目指す アトミックって何ですかぁ？ 関係データベースである限り、かならず第1正規形になっていることが要求されます。で、第1正規形って何？ カラムの値がアトミックであることだと定義されます。アトミック？ それ何？ まーともか
型システム入門 サポートページ
TAPL 型システム入門 サポートページ Benjamin C. Pierce 著 住井英二郎 監訳 遠藤侑介・酒井政裕・今井敬吾・黒木裕介・今井宜洋・才川隆文・今井健男 共訳 ISBN 978-4-274-06911-6 Benjamin C. Pierce "Types and Programming Languages" の日本語版サポートサイトです。 ご質問・議論 書籍『型システム入門』（TAPL日本語版）の技術的内容や、型システム全般に関する、日本語での質問と議論は GitHub issues にお願いします（2023年9月以前の議論は Google グループ "taplkatasystem" を参照）。 正誤表 第1刷（第2刷で修正済） 定理15.3.5 の証明（p. 148）の「T-Subの場合」における結論の「Γ ⊢ t : T」は、正しくは「Γ ⊢ t' : T」です（原
型推論について - soutaroブログ
暇をみつけては python の型推論をやっている (やろうとしている)。でも、いまだに本当にこれが「原理的に可能」なのかどうか疑問だ…。 http://www.unixuser.org/~euske/offline/memo/cur/cur.html#180812 「原理的に可能」とかについて． まず「原理的に可能」の意味を考える必要がある．「可能」ってなに?なにができたら「可能」なの? 型推論とかのプログラム解析の技術を評価する場合，二つの性質が重要になる．「健全性」と「完全性」．「型推論が健全性を持っている」というのは，「型が推論できたら，そのプログラムは正しい」ということ*1．「型推論が完全性を持っている」というのは，「正しいプログラムは必ず型が推論できる」ということ．MLなんかの型推論は，完全かつ健全である．非常に良くできた型推論アルゴリズムと言える．ただし，型推論アルゴリズムと
オブジェクト指向から理解する型クラス - think and error
Haskell Advent Calendar2011 2日目です。 もう42時になってしまいました...さすがに遅いですね。 Haskellと言えば型クラス オブジェクト指向のクラスとHaskellの型クラスは違いますよ的な説明は見ますがどう違うか比べた情報が無い オブジェクト指向知っている人からの理解を簡単にすればHaskell理解する人が増えますね！ という目論見の元にスライドを作りましたが、ユーザ視点が足りずに混乱させてしまったかも知れません。 Programming haskell chapter10 View more presentations from Ruicc Rail Haskell Advent Calendar明日はid:melponさんです。
行政学における機能概念 - たけみたの脱社会学日記
ルーマン私訳一覧へ戻る Niklas Luhmann, Der Funktionsbegriff in der Verwaltungswissenschaft, Verwaltungsarchiv 49 (1958), S. 97-105. 概念というのは、正しいか正しくないかを論じるものではない。概念について論じることに何か意義があるとしたら、それは、その概念の使い方をちゃんと決めることであり、そうやって決めた使い方を貫いていくとどうなるかを明らかにすることである。その概念が出てきたときに、誰にでもすぐにその意味がわかるためには、論理的に正しく制御できる使用法というのが必要なのであって、そのためにはまずその使用法を決めておかなければならない。 さて、そこで機能［関数］（Funktion）概念であるが、この概念には、論理学や数学で使われているのを除けば、上で述べたような意味での明確さがまっ
次元+次元・解析 -- 現象と量の型チェック機構 - 檜山正幸のキマイラ飼育記 (はてなBlog)
「なんとかならないのか!? ベクトル解析：用語法の無茶苦茶」で次のように言いました： （物理的な意味での）次元解析をちゃんとすべし それで、次元解析（みたいなこと）の話をしたいのですが、「次元」という言葉は注意が必要です。「次元」の2つの意味・用法と、それら2つの次元を両方とも同時に計算・解析する方法について述べます。 内容： 幾何次元と物理次元 量の空間の演算 直積と外積 無次元量 実例：熱流束密度と熱伝導度 L3/(L3∧L3) の分析 強い型付けとしての次元解析 ●幾何次元と物理次元 「次元」は多義語なので、代表的な2つの用法を「幾何次元」と「物理次元」と分けて呼びましょう。 幾何次元は、「直線が1次元で平面なら2次元」といった使い方をする「次元」です。要するに、「空間がいくつの方向に広がっているか」ですね。あるいは、空間の位置を数値の組（座標）で表すとき、「いくつの数を必要とするか
ヒビルテ(2008-09-21)
λ. Sets in types, types in sets Sets in types, types in sets by Benjamin Werner, in Proceedings of TACS'97 We present two mutual encodings, respectively of the Calculus of Inductive Constructions in Zermelo-Fraenkel set theory and the opposite way. More precisely, we actually construct two families of encodings, relating the number of universes in the type theory with the number of inaccessible ca
型推論と型検査、静的な型つけと動的な型つけ、強い型つけと弱い型つけ - sumiiのブログ
ついでに追加。 型推論：変数や式の型をプログラマが宣言しなくても、言語処理系が文脈から推論してくれる機構。MLとかHaskellとか。 型検査：変数や式の型が合っていることを言語処理系が（普通は静的に）チェックしてくれる機構。CとかJavaとか、MLやHaskellも。 静的な型つけ：プログラムの実行前に型を検査する機構。MLとかHaskellとかCとかJavaとか。 動的な型つけ：プログラムの実行中に型を検査する機構。LispとかSchemeとかPerlとか。 強い型つけ：検査を通れば、安全さ(safety)が保証される、という（普通は静的な）型つけ。MLとかHaskellとかJavaとか。Javaはバグがあったりしたので少し怪しいですが。 弱い型つけ：検査を通っても、安全さ(safety)は保証されない、という型つけ。CとかPascalとか。 安全さ(safety)：プログラムが言語仕
論文ファイブ - d.y.d.
16:40 09/01/28 インドコンテスト おとといのを読み返してて、 全体として並列並行系多いなーといっておきながら、 個別紹介に１個もそれ系のがなくて面白いなあと思いました。 と、それはともかく、今年もインド発プログラミングコンテストのお知らせが来てました。 ICPCやTopCoder系の問題の出る CodeCraft、 Project Euler系の問題の出る MathematiKa、 あと今年はなんだか縛り付きプログラミング（ゴルフとか）系の Time Limit Exceeded というのがあるらしい。毎年恒例行事にするつもりなのかな。 去年のはわりと面白かったので、今年も参加してみるつもり。 23:10 09/01/26 POPL 2009 行ってきました。MS Research 多いなーというのと、 まあ当たり前ですが並列並行系多いなーというのが全体的な感想。 以下印象に
はてなブログ | 無料ブログを作成しよう
うまくいかない日に仕込むラペ 「あぁ、今日のわたしダメダメだ…」 そういう日は何かで取り返したくなる。長々と夜更かしして本を読んだり、刺繍をしたり…日中の自分のミスを取り戻すが如く、意味のあることをしたくなるのです。 うまくいかなかった日のわたしの最近のリベンジ方法。美味しいラペを…
リネームとサブタイプと置換原則 - 檜山正幸のキマイラ飼育記 (はてなBlog)
みずしまさんから、一言ではこたえにくいご質問・ご意見をいただいたので、この機会に新しいエントリーを書きます。自分用メモも兼ねており、以前書いたエントリーへのリンクをたくさん含んでいます。 「なんで多重継承はそんなに嫌われるのか？ ちょっくら分析してみるか」において、リスコフの置換原則を引き合いに出しました。リスコフの置換原則については、「クラス継承、リスコフの置換原則、部分集合の型」でも述べています。しかし僕は、リスコフ女史が本来どういう意図と表現で、どのような言明をしたかを正確には知りません。間接伝聞で誤解しているかも。 ですが、「本来」の詮索はおいといて、「リネームとサブタイプと置換原則」にまつわる状況を実例付きで説明することにします。「インスティチューション」という言葉を表だっては出しませんが、僕の気持ちとしては、インスティチューション入門も意図しています。「もっと型理論」の続きみた
今風の型理論入門（本編） - 檜山正幸のキマイラ飼育記 (はてなBlog)
前ふりは「型→代数→…それから：型理論入門（の前半）」にあります。これは本編（後半）。1回読み切り（長いけど）で、比較的新しい*1型理論を紹介します。「入門（門に入る）」というよりは門の外から中を覗いてみる程度。 説明用コードはJavaの構文を使います。ただし、パッケージ宣言は書かないし、publicはなるべく省略。 内容： インターフェースなんて、所詮こんなもの 心理的効果とか、人間-人間コミュニケーションとかは、別問題 わけわからんインターフェースに制約を付加する もっと制約を足してみる 謎のインターフェースに意図されたもの で、それが型理論にどうつながるの？ インターフェースなんて、所詮こんなもの まず、次のインターフェースを見てください。 interface AB { int a(); void b(); } これスゴイでしょ。何がスゴイって、これを見てもなんのことやらサッパリわか
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
数理科学的バグ撲滅方法論のすすめ---目次 | 日経 xTECH（クロステック）
型理論-4- | CiNii Research
型理論-3- | CiNii Research
型理論-2- | CiNii Research
型理論-1- | CiNii Research