はじめに
「『型なし』と『動的型』って同じ？違う？」「ピピーッ！JavaScriptやRubyを『型なし言語』と呼ぶのは間違いです！」
ツイッターを見ていると、このように「型」という言葉の用法に混乱がみられるので、私見で整理してみたいと思います。
まず、「型」という言葉の用法には、大きく分けて2つあります：
- 変数や関数についての静的にわかる性質
- 静的型言語では「型」と言ったら主にこちらを指します。
- 値の種類を区別するための実行時のタグ付け（型タグ）
- 「動的型言語」と言った場合の「型」はこちらです。
- 静的型言語でも「実行時型情報」という名前で、値にタグがついている場合があります。
前者の立場では、「動的型言語」は「型がない」ように見えて、後者の立場では、「動的型言語」にも「型がある」ように見えます。
「静的型 vs 動的型」（あるいは「型あり vs 型なし」）の議論をする際は、「型」という言葉をどちらの意味で使っているのか、意識しておくと良いでしょう。
この文書の残りの部分については、静的な型の特徴や意義、静的な型と実行時の型タグの関係などを見ていきます。以後、単に「型」と言った場合は、静的な型を指します。
静的な立場から見た動的型言語
「静的な立場からすると動的型言語には型がない」と言いました。あえて静的な立場から動的型言語を解釈するなら、動的型言語というのは、ただ1種類の型「Any」を持つように見えます。
Any 型は万能で、どういう使い方（数値演算、関数としての呼び出し、メソッド呼び出し）をしても静的な型検査をパスします（という風に思えます）。
静的な型が1種類しかないということは、静的に得られる情報量がゼロということですから、「（静的な）型がない」と称されるのもやむを得ないわけです。
Gradual Typing について
このような「静的にチェックされない、万能の型」 Any と、通常の（静的チェックされる）型を共存させるのが、最近流行りの gradual typing です。
ただ、 Any 型と他の型の組み合わせ方には要注意です。素直に T ≤ Any, Any ≤ T という風に Any 型と他の型を互換にしてしまうと、全く異なる型 S と T についても Any を介することによって S と T が互換となり、つまり静的な型の体系が「潰れて」しまいます。
静的な型の体系を潰さないようにしつつ、「万能な型」 Any を入れるというのが gradual typing のポイントです。
もっと知りたい方は、 gradual typing の考案者 J. Siek による記事
も読むと良いでしょう。
静的な型と動的な型タグの関係
静的な型システムを持つ言語であっても、実行時に型タグをテストして、静的な型を変換（キャスト）できる場合があります。
このような操作としては C++ の dynamic_cast が代表的でしょう。
Java では instanceof 演算子、 C# では is 演算子によって型タグのテストができます。
Haskell では Data.Typeable の型クラスと関数によって、型タグをテストしたり、キャストしたりすることができます。
通常は、型タグを使用した型の変換（キャスト）には、明示的な操作が必要です。Gradual Typing の Any 型の場合は、このような型の変換が暗黙に起こります（実装によっては型タグのテストが行われなかったりしますが）。
静的な型のメリットとデメリット
メリット
静的な型を持つことの利点は、いくつか考えられます：
- 実行時エラーの排除（プログラムの性質を保証する）
- 効率的なコード生成
- IDE など、開発支援ツールでの利用（入力支援など）
- ソースコードに対する簡易的なドキュメント（型注釈を明示的に書く場合）
注意して欲しいのは、これらのメリットを生かすかどうかは言語および処理系次第であって、必ずしも「静的な型がついているから高速化する」「静的な型がついているのに実行時にぬるぽが起こる言語はフェイク野郎」というわけではありません。
例えば、 TypeScript の場合は JavaScript コードを生成する際に型注釈をはぎ取ってしまうため、いくら型を書いても実行時の高速化には寄与しません。（これはどちらかというと処理系の問題で、同じような言語であっても AssemblyScript のような処理系であれば型によって効率的なコードが生成できるでしょう）
あるいは、発展途上の言語では IDE 等の開発支援ツールのサポートが貧弱で静的型を活かせないかもしれませんが、だからと言ってその言語の静的型が全く無意味ということにはならないでしょう。
「実行時エラーの排除」にも度合いがあって、型システムによって排除できるエラーとそうでないエラーがあります。
例えば、多くの言語では、ゼロ除算や配列の範囲外アクセスを静的に排除できません。あるいは、 Java の場合は NullPointerException を静的に排除できません。
これらのエラーを静的に排除したければ、よりきめ細かい型をつけ、プログラムの書き方をより制約していくことになるでしょう（時にはプログラマーに証明を書かせることになるかもしれません）。
デメリット
静的な型を持つことによるデメリットもいくつか考えられます。
- 「正しい」プログラムに型がつかない
- （体系によっては）型注釈が必要
- 言語の設計者に対する要求レベルが上がる
1番目については、「より強力な」型システムを搭載することによって緩和できます。
例えば、多相型のない単純な型システムでは、次のプログラムに型をつけられません：
function identity(x) {
return x;
}
identity(123); // identity を number => number 型として使っている
identity("hello"); // identity は number => number 型だったはず…。エラー！
しかし、多相型を持つ型システムでは、同じプログラムに型をつけることができます：
function identity<T>(x: T) {
return x;
}
identity(123); // T=number として、 identity を number => number 型として使っている
identity("hello"); // T=string として、 identity を string => string 型として使っている
別の例として、 Haskell ではYコンビネーター λf. (λx. f (x x)) (λx. f (x x)) に型をつけられません
> y = \f -> (\x -> f (x x)) (\x -> f (x x))
<interactive>:2:23: error:
• Occurs check: cannot construct the infinite type: t0 ~ t0 -> t
Expected type: t0 -> t
Actual type: (t0 -> t) -> t
が、再帰型のある体系ではYコンビネーター（やその他の不動点コンビネーター）に型がつきます。（筆者が以前書いた TypeScriptで不動点コンビネータに型をつける - Qiita も見てください）
2番目（型注釈）については、型推論によって型注釈を省略できる場合があります。しかし、どんな体系でも型推論ができるという訳ではありません。
なお、完全な型推論が可能な言語であっても、明示的に型注釈を書くことが「良い習慣」とされる場合があります（Haskell など）。理由としては
- 書く人にとっては、型注釈が関数の設計図となる
- 読む人にとっては、型注釈が簡易的なドキュメントとなる
- 処理系にとっては、プログラムの誤りに対してより良いエラーメッセージを出す助けとなる（ので書く人に優しい）
などがあるでしょう（Haskell の場合は他の理由もありますが）。
3番目、言語の設計者にとっては、型システムを設計するという仕事が増えます。型の表現力、型推論、既存のエコシステムとの兼ね合いなど、両立しづらい複数の要素を考慮して落とし所を見つける必要があります。また、「型システム入門」で扱っていないような発展的な機能が必要なら、ガンガン論文を漁っていくことになるでしょう。
型推論と型注釈
（ここで言う「型推論」は、「関数の仮引数の型を書かなくても推論してくれる」機能あるいは「型引数を補う」機能のことであり、「初期化子付きの変数宣言において右辺の型から変数の型を決める」機能のことではありません。）
型推論の神を信じる民は禁欲的で、型システムにあまり多くを求めすぎない。あまりに強力な型システムを作ると、型推論の神の怒りを買うと信じられているのだ。 — @mod_poppo, 2018
ML 系言語や Haskell では完全な型推論1ができますが、このような言語は、通常は言語を設計する段階で「型推論の邪魔になる機能を持たないように」配慮されています。具体的には、部分型付けや非可述多相があると型推論が困難になる（あるいは、不可能になる）ようです。
逆に、新しく言語を設計する場合でも、あえて完全な型推論を捨てて既存のエコシステムとの互換性を優先する場合が見受けられます。
- Scala は完全な型推論よりも Java との互換性（部分型付け、メソッドのオーバーロード等）を優先したようです。
- F# はドットネットのオブジェクト指向的な概念が絡むと型推論できない場合があるようです。
- TypeScript の型システムが既存の JavaScript コードに配慮しているのは言うまでもないでしょう。
そのような「完全な型推論を諦めた」言語であっても、文脈から関数の型がわかる場合（コールバック関数など）には関数の引数の型を推論できることがあります（局所型推論; local type inference）。
ここ数年 Ruby 界隈の偉い人が「型推論させるから型注釈はいらない」的なことを言っているようですが、既存のエコシステムを捨てない限りは「完全な型推論」は不可能でしょう。方針転換して何らかの型注釈の文法の導入するのか、それとも静的に実行できない何かを「型推論」と呼んで2用語の混乱に拍車をかけるのか、要注目です。（Feature #9999: Type Annotations (Static Type Checking) - Ruby trunk - Ruby Issue Tracking System）
型とセマンティクス： Curry スタイル vs Church スタイル
「静的な型のメリットとデメリット」のセクションでは、あたかも「型がなくても一応プログラムは動くけど、型があるとこんないいことがあるよ」という語り方（Curry スタイル）をしました。
TypeScript が典型例で、 TypeScript の型注釈を剥ぎ取ってもプログラムは（ほぼ）JavaScript として動作するし、もっというと、型エラーが発見されても tsc は JavaScript コードを出力します（noEmitOnError なしの場合）。
一方で、「静的な型がプログラムの本質的な一部分」で「型がないと（型検査が通らないと）そもそもプログラムの意味を考えられない」という見方（Church スタイル）もあります。
例えば C++ には関数や演算子のオーバーロードができ、静的な型によって呼び出される関数が選択されます：
void foo(int x);
void foo(std::string x);
void bar() {
foo(123); // foo(int) が呼ばれる
foo("Hello world!"); // foo(std::string) が呼ばれる
}
これは、静的な型に基づいてプログラムの意味が定まっていると言えるでしょう。
なお、動的型言語でも、実行時に型タグを検査すればこの程度の関数のオーバーロードはできるでしょう：
function foo(x) {
if (typeof x === "number") {
// 数値が渡された場合の処理
} else if (typeof x === "string") {
// 文字列が渡された場合の処理
}
}
foo(123);
foo("Hello world!");
今書いた関数 foo の例では、静的型と動的型の違いは、処理の分岐がコンパイル時に行われるか、実行時に行われるか程度の違いしかないように見えるかもしれません。
では、 Haskell の fromInteger の例はどうでしょうか：
data T = T
instance Num T where fromInteger _ = T
instance Show T where show _ = "Hello world!"
main = do
print (fromInteger 123 :: Int)
print (fromInteger 123 :: T)
fromInteger は Num a => Integer -> a という型を持ち、返り値の型のみによってオーバーロードが解決されます。これはプログラムが静的な型によって意味づけされるからこそ可能なことで、動的型言語では不可能3なことかと思います。
（というか、このような例では型注釈がないと「型が曖昧」になって、プログラムの意味が定まりません。この fromInteger の例では型注釈がないと default 規則によって Integer となりますが、例えば read を使う場合は型注釈がないと曖昧さによってエラーとなることもしばしばあります。）
何が言いたかったかというと、「型はプログラムの安全性の保証や高速化のためにある」という立場、「そもそも型がないとプログラムの意味が定まらない／プログラムに意味を与えるために型を使う」という立場の、両方がありうるということです。
終わりに
平均的なプログラマーに「型について語る前に『型システム入門』を読め」というのは酷かもしれませんが、この記事に書いたような「型」という語の多義性については意識してください。
偉そうにこんな記事を書いている筆者もまだまだ勉強中の身で見識が足りていないので、「型」について一家言あるという人は是非、ブログでも Qiita でも書いてください（ツイッターは用語の意味の確認から始めるような議論に向かないので、ダメです）。
【3月2日 追記】「完全な型推論」「型とセマンティクス」のところにそれぞれ注釈をつけた。