タグ

型理論に関するDOISHIGERUのブックマーク (3)

  • クラスとは何か - SiroKuro Page

    とりあえず 「クラスは型である」は間違いである - SiroKuro Page を整理してみようと思った。 自分が考える『クラス』という語句を可能な限り明確にするために、色々と参考にして次のように分けて考える。 クラス定義(ソースコードの記述) クラス型 クラス(java.lang.Class のインスタンス) 変数宣言を記述する際のクラス名 前提:「クラス定義」は「クラス型」および「クラス」を定義する これはたぶん正解で問題ない。 命題その1:「クラス定義 != クラス型」 定義と型そのものは厳密には同じではない。たぶん。 命題その2:「クラス定義 != クラス」 定義とクラスそのものは厳密には同じではない。たぶん。 命題その3:「クラス型 != クラス」 これがそもそもの問題。自分のイメージとしては クラス型が表す情報は型に関する情報のみで、実装の詳細は含まれていないだろう クラスが持

    クラスとは何か - SiroKuro Page
  • 型システムの理論の影 - プログラマーの脳みそ

    プログラムにおける型システムってのは数学・論理学の型理論を基盤にしていて、抽象的なもやもやとした代物。この型システムの理論を現実に実装したものとして、多様なプログラム言語が存在するわけだ。 鶏と卵という話だとどっちなんだろう。実装が先でそれを理論としてまとめたって感じなのか、理論がまず考えられてプログラム言語が実装されたのか…。最初のプログラム言語というと1954年に登場したFORTRANで、IBMのジョン・バッカス氏*1によって考案された。FORTRANにはいくつかの数値型がある。この頃に型システムの体系的な理論ができていたとは思えないから多分、実装が先行なんだろうな。 理論としての型、そのJava実装のクラス 型システム(type system)でいう型(type)は型理論に基づくわけで、数学的な抽象概念に近い。例えば僕らが日常生活で数学的概念である1/3という値を厳密に使うことはない

    型システムの理論の影 - プログラマーの脳みそ
    DOISHIGERU
    DOISHIGERU 2011/12/01
    ゆるふわ
  • 型理論 - Wikipedia

    型理論(かたりろん、英: Type theory)とは、プログラミング・数学言語学等に現れる型の概念及びそれらが成す型システムを研究対象とする数学・計算機科学の分野である。特定の型システムのことを型理論と呼ぶこともある。集合論の代替となる数学の基礎として役立てられる型理論(型システム)も存在する。そのような例としてアロンゾ・チャーチの型付きラムダ計算やマルティン・レーフの直観主義型理論が有名である。 20世紀初頭にバートランド・ラッセルが発見した、ラッセルのパラドックスによるフレーゲの素朴集合論の欠陥を説明する中で提起されたtheories of typeが型理論の起源であり[1]、後年にAxiom of reducibilityが付随された型理論は、ホワイトヘッドとラッセルの 『プリンキピア・マテマティカ』に収録されている[2]。 単純階型理論(Simple Theory of Typ

  • 1