[過去ﾛｸﾞ] 次世代言語12 Go Rust Swift Kotlin TypeScript (1002ﾚｽ)
上下前次1-新
抽出解除 必死ﾁｪｯｶｰ(本家) (べ) 自ID ﾚｽ栞 あぼーん
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
108(2): デフォルトの名無しさん [sage] 2018/07/09(月) 13:40:36.06 ID:XHrPXSC2(1/2) AAS
>>103103(2): デフォルトの名無しさん [sage] 2018/07/09(月) 11:44:42.26 ID:KFrfmR/A(1/4) AAS
依存型がある言語はML族もしくはF#の軽量構文みたいなのが多いのはなんでなの？
C系のシンタックスだと何か不都合でもあるの？
> 依存型がある言語はML族もしくはF#の軽量構文みたいなのが多いのはなんでなの？
> C系のシンタックスだと何か不都合でもあるの？
依存型や本来の多相型(polymorphism)［†］などは型理論の体系つまり高階の型付λ計算に関する論理体系に基づくので
プログラミング言語の型システムとして組み込む場合には同じくλ計算に基づくと関数プログラミング言語の枠組みとは親和性が良いが
Cなどのように変数の値を書き換える代入文や代入演算を有する命令的プログラミング言語とは馴染まない。［‡］
だからそれらの型システムを導入した言語は既存の関数プログラミング言語の構文を流用するケースが多いのだろう。
なおStandard ML/CAML/OCaml/F#などeager evaluationを評価ルールとするいわゆるML系の関数プログラミング言語の一群は
ref型のように代入可能な変数を許すが、本格的な型理論に基づく型システムを組み込む場合はref型の類は除いたsublanguageに対して
行うのが普通。
［†］：本来の多相型とはGirardが竹内の基本予想に関する学位論文で最初に発見（あるいは発明）し
Reynoldsが独立に再発見した型の全称化・抽象化やMilnerが発見したlet-polymorphismなどを指す。
オブジェクト指向での継承に伴って使われるようになった“polymorphism”は
定義が不明確で勝手な拡大解釈が多いので「本来の」という修飾句の対象範囲からは除く。
［‡］：代入操作（代入文と代入演算の総称）を含む命令的プログラミング言語
（Ｃなどの手続き的プログラミング言語やオブジェクト指向プログラミング言語を纏めてこう呼ぶ）に
例えば多相型が馴染まない理由は代入操作可能な変数の型として多相型を許すことは
その変数について動的な型付けを許すことに他ならなくなる。
例で少し説明するが既知なら許してくれ。最も基本的な多相型 ∀t.t （どんな型でもＯＫ）と宣言された変数 x を考える、つまり
∀t.t x;
この変数はどんな型の変数としても使えるので、これにint型の値 1 は代入できる、
x = 1;
この後で式の中でこの変数の値を参照すると int型の値 1 が許される文脈以外ではエラーになる。
即ち、型理論における本来の多相型つまり静的な型付けでの多相型の概念は代入可能な変数では失われるということだ。
119: デフォルトの名無しさん [sage] 2018/07/09(月) 20:54:48.10 ID:XHrPXSC2(2/2) AAS
>>114> ALGOL舐めてるわけ?
AlgolとくにAlgol 60は実用性はともかく言語設計の観点からは非常に優れた言語だったが、命令的言語であるがゆえに型理論には馴染まない部分がある
今回の君のような内容ゼロの一言レスしてる暇があったら、ReynoldsやTennentの教科書・論文ぐらいは読んで勉強したらどうよ
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.026s