[解決済み] アカデミックなCSの世界では、「untyped」は「dynamically typed」の意味もあるのか？

質問

あるスライドデッキを読んでいたら、「JavaScriptは型付けされていない」と書いてありました。

の回答はすべて JavaScriptは非定型言語ですか？ は、JavaScriptが ではない 型付けされない、静的、動的、強い、弱い型付けの様々な形式の例を提示しており、私はそれに慣れていて満足しているのですが、その方法はありませんでした。

そこで、JavaScriptの生みの親であるBrendan Eichに尋ねてみました。

学術的な型は "untyped" を使って "no static types" を意味する。彼らは値が型を持つことを理解できるほど賢い（当たり前か！）。

学術的なコンピューターサイエンスの人々は、"untyped" を"dynamically typed" の同義語として使っていますか（そしてこれは有効ですか）、それとも私が見逃している何か深いものがあるのでしょうか？私はBrendanと同じように文脈が重要であることに同意しますが、私が現在読んでいる本がこのトピックに対応していないため、説明の引用があれば助かります。

また、ウィキペディアにもこのような使い方は載っていません。もし私が間違っていた場合、その用語の使用や疑問のどちらかを台無しにしたくありません:-)

(一流のSmalltalkerがSmalltalkは"untyped"と言っているのも見たことがあるので、この探求を始めたのは一回限りではないのです) :-))

解決するには？

そう、これは学術的な文献では標準的なやり方なんだ。これを理解するには、quot;type"の概念が1930年代にラムダ計算の文脈で（実際はもっと前に集合論の文脈で）発明されたことを知るのに役立ちます。それ以来、計算論理学の一分野として、型理論（quot;type theory"）と呼ばれるものが生まれました。プログラミング言語の理論も、これらの基礎の上に成り立っている。そして、これらすべての数学的文脈において、quot;type"は特定の、確立された意味を持っているのである。

動的型付け（dynamic typing）という用語は、ずっと後になって考案されたもので、数学的に一般的な型という言葉の使い方とは矛盾しています。

例えば、Benjamin Pierceが彼の標準的な教科書で使っている「quot;型システム」の定義は次のとおりである。 型とプログラミング言語 :

型システムとは、型がないことを証明するための扱いやすい構文的手法である。 によってフレーズを分類することによって、特定のプログラム動作の を計算する。

と発言している。

静的」という言葉は、時に明示的に付け加えられます。 例えば、「静的型付けされたプログラミング言語」と区別するために ここで考えているようなコンパイル時解析と Scheme などの言語で見られる動的または潜在的な型付け (Sussman とSteele, 1975; Kelsey, Clinger, and Rees, 1998; Dybvig, 1996)があります。 ここで、実行時の型タグは、異なる種類のものを区別するために使用されます。 ヒープ内の構造体 動的型付け "などの用語は、間違いなく というのは誤用で、おそらく「動的にチェックされる」と置き換えるべきでしょう。 しかし、この使い方は標準的なものである。

この点については、現場で働く人の多くが共感しているようです。

ただし、これは ではなく これはquot;untyped"とquot;dynamically typed"が同義語であることを意味します。むしろ、後者は前者の特定のケースに対する（技術的に誤解を招く）名前であるということです。

PS: ちなみに、私は型システムの学術的な研究者と、JavaScriptの非学術的な実装者の両方であるため、シスマと共存しなければなりません。）