【TypeScriptよりいいもの】未だ応用されきっていない、型システム本来の力の簡単紹介【読み物】
これはなに？
型システム（静的型付けのシステム [1]）のオタクによる、ものすごく簡単な説明。
型システムには多くの機能が存在するため、必ずしも単純な強弱で語れないものの、基本的に上から下に行くほど、型システムがリッチになっていくことを意図している。
C・C++
intやcharなどの値が区別できるが、いつの間にかそれぞれが紛れ込んでいたりする。
これは型チェックエラーにならない:
#include <iostream>
int main() {
int age = 25;
char grade = 'A';
// intとcharには暗黙変換があるのでコンパイルエラーにならない！
int result = age + grade; // 25 + 65 = 90
return 0;
}
これは正しく型チェックエラーになる:
#include <string>
int main() {
int age = 25;
std::string name = "Alice";
// intとstd::stringには暗黙変換がないのでコンパイルエラー
int result = age + name;
// => invalid operands to binary expression ('int' and 'std::string' (aka 'basic_string<char>'))
return 0;
}
参考:
Java
C++と似たような感じだけど、紛れ込みにくくなった。
罠っぽさは減ったけど、完全ではない。
またC++と比べて、型の計算ができなくなった。[2]
これは正しく型チェックエラーになる:
import java.util.ArrayList;
import java.util.List;
void main() {
List<String> names = new ArrayList<>();
names.add("Alice");
names.add(42);
// Main.java:7: エラー: addに適切なメソッドが見つかりません(int)
// names.add(42);
// ^
// メソッド List.add(String)は使用できません
// (引数の不一致: intをStringに変換できません:)
// メソッド List.add(int,String)は使用できません
// (実引数リストと仮引数リストの長さが異なります)
}
これは型チェックエラーにならない（警告にはなる）:
import java.util.ArrayList;
import java.util.List;
void main() {
List<String> names = new ArrayList<>();
names.add("Alice");
List rawList = names;
rawList.add(42); // コンパイルエラーなし（警告のみ）
// Main.java:8: 警告: [unchecked] raw型Listのメンバーとしてのadd(E)への無検査呼出しです
// rawList.add(42); // コンパイルエラーなし（警告のみ）
// ^
// Eが型変数の場合:
// インタフェース Listで宣言されているE extends Object
// ...
// 警告1個
String s = names.get(1); // → ClassCastException（実行時エラー！）
// Exception in thread "main" java.lang.ClassCastException: class java.lang.Integer cannot be cast to class
// java.lang.String (java.lang.Integer and java.lang.String are in module java.base of loader 'bootstrap')
// at Main.main(Main.java:9)
}
これは完全に型チェックエラーにならない:
void main() {
char grade = 'A';
int age = 25;
// C++同様、charがintに暗黙変換されてしまう
int result = age + grade; // 25 + 65 = 90 -- エラーなし
}
参考:
C#
実行時に型が残るようになって、Javaよりもさらに紛れ込みにくくなった。
（Javaは実行時に型が残らない場合が多い。）
これは正しく型チェックエラーになる（警告にもならず、絶対に許されない）:
var numbers = new List<int>();
numbers.Add(42);
List rawList = numbers; // error CS0305: ジェネリック 種類 'List<T>' を使用するには、1 型引数が必要です
rawList.Add("Hello");
List<object> objectList = numbers; // error CS0029: 型 'System.Collections.Generic.List<int>' を 'System.Collections.Generic.List<object>' に暗黙的に変換できません
objectList.Add("Hello");
実行時に型情報が残る（具体化されたジェネリクス）。
ジェネリック引数の型も実行時に取得できる。
var numbers = new List<int>();
Type type = numbers.GetType();
Console.WriteLine(type);
// → System.Collections.Generic.List`1[System.Int32]
Type elementType = type.GetGenericArguments()[0];
Console.WriteLine(elementType);
// → System.Int32
C#は静的な型システムとランタイムの型情報について十分リッチだが、以下のようなエスケープハッチはあり、乱用の恐れはある。
dynamic x = "hello"; // dynamic型: コンパイル時の型チェックをバイパスできる
x = 42; // 型が変わってもエラーなし
Console.WriteLine(x.NonExistentProperty); // 実行時エラー（コンパイル時に検出できない）
参考:
TypeScript
意図的に紛れ込ませやすいように設計されている。
（漸進的型付き言語であることも強い要因。）
また型情報は実行時に残らない。
ただし型を関数にかけて、型を計算できるようになった。
（「型関数」で型を計算するという意味では、C++のTMPに近い。）
仮定:
{
"strict": true,
"noUncheckedIndexedAccess": true
}
これは型チェックエラーにならない:
const numbers: number[] = [42]
const list: unknown[] = numbers
list.push("Hello") // numberの配列にstringをpushしているが、エラーにならない
console.log(numbers) // [ 42, "Hello" ]
この例のように、TypeScriptにおいて破壊的代入の多くは、型システムの破綻をもたらす。
（array.push()も破壊的代入の一種である。）
筆者は破壊的代入を禁止することをおすすめする。
その際は後述のHaskellを学び、模範的な関数型プログラミングを学ぶとよい。
これは正しく型チェックエラーになる:
const numbers: number[] = [42]
const list: unknown[] = numbers
// list.push("Hello")
// 型チェックエラー
// Type 'unknown' is not assignable to type 'string'.
const s: string | undefined = list[0]
これは型チェックエラーにならない:
const num: number = 42
const x: any = num // any型の変数はどの型の値も代入でき、
const str: string = x // またどの型の変数へ代入することもできる（この例ではstring型の変数str）
型関数（型の計算）の例（※正しく型チェックエラーになる）:
type IsString<T> = T extends string ? 'yes' : 'no'
type Yes = IsString<string> // 'yes'
type No = IsString<number> // 'no'
// 型チェックエラー
// Type '"yes"' is not assignable to type '"no"'.
const expectedYes: IsString<boolean> = 'yes'
この例のように型の計算をすることで、型チェック時にロジックの正しさを部分的に証明することができる。
ここで「部分的に」「証明」というワードが重要になってくる。
それぞれ後述の、以下の章で説明する。
- 「部分的に」: Haskell
- 「証明」: Idris
参考:
Haskell
頑張らないと別の型と別の型を紛れ込ませられない。
また単純な値（IntやChar）だけでなく処理（IOなど）にも型が付く。 [3]
そのため、IOがついていない関数は、入出力処理が行えない。
（IO以外にも「処理」の種類はあるが、ここではIOのみを例示する。）
またHKTというものの手厚いサポートにより、intやcharのような値だけではなく、値に特徴をつけることができるなど、かなりの応用が効く。
HKTこそ、多くのプログラマーの考える「十分な型システム」を超える、本来の「十分な型システム」の機能のひとつである。
（入出力の処理に前述のIOに操作に型が付くのも、その応用のひとつである。）
これは正しく型チェックエラーになる:
-- 通常の関数 - IO型なし・入出力なし
double :: Int -> Int
double x = x * 2
-- IO型が付いた関数 - 入出力（ここではputStrLn）ができる
greet :: String -> IO ()
greet name = putStrLn ("Hello, " ++ name)
-- 型チェックエラー！
-- IOがついていないので入出力ができない
badGreet :: String -> ()
badGreet name = putStrLn ("Hello, " ++ name)
-- Main.hs:12:17: error: [GHC-83865]
-- • Couldn't match expected type ‘()’ with actual type ‘IO ()’
-- • In the expression: putStrLn ("Hello, " ++ name)
-- In an equation for ‘badGreet’:
-- badGreet name = putStrLn ("Hello, " ++ name)
これは型チェックエラーにならない（頑張ってunsafeと名前がついている関数をわざわざ呼び出す必要がある）:
import System.IO.Unsafe (unsafePerformIO)
-- IOを持たない関数から副作用を実行できてしまう
thisHasUnknownSideEffect :: Int -> Int
thisHasUnknownSideEffect x = unsafePerformIO (do -- doはブロックの始まり。Pythonのブロック始まりの`:`と似ている
putStrLn "so bad"
return (x + 10)
)
これは型チェックエラーにならない:
-- 型は正しいがパターンが網羅されておらず実行時エラーになりうる
foo :: Int -> Int
foo x =
let y = head [] :: Int -- head [] は実行時エラー（型チェックを通過する）
in x + y
-- 例外:
-- Main.hs: Prelude.head: empty list
関数型プログラミングでは、このような例外を出す関数（または無限ループ・無限再起をする関数）をしばしば「不純な関数」と呼ぶ。
これはその逆の、例外・無限ループ・無限再起を出さない関数を「純粋関数」と呼ぶことへの、対比である。
（Haskellでは本来「IO型でない関数こそ純粋」「IO型の関数こそ不純」とされるが、実際にはこのheadや前述のunsafe系など、「IO型でないのに不純な関数」が存在できてしまう。Haskellのうち、模範的でない部分の代表である。）
HKTの例:
-- 「型を受け取る型（他の言語でいう、ジェネリクス（型引数）を持つ型）」を受け取ることができる
-- 「型を受け取る型」の一例
data Maybe a = Nothing | Just a
-- 今回、戻り値には興味がないので、単純化している
f :: forall f a. f a -> Int
f x = 10
-- 一般の`forall x y.`は、JavaやTypeScriptのジェネリクス`function f<X,Y>`と同じものだが⋯（後述に続く）
-- また通常の場合、Haskellではそのようなジェネリクス（型引数）の宣言を省略することができる。今回は後述との対比のために、明示的に書いている
result :: Int
result = f (Just True) -- 型推論されているが、fにMaybe型を渡せている
-- => 10
-- ここでfに渡しているのは単一の型`Maybe Bool`ではなく、`Maybe`と`Bool`の2つの型である
これをちょうど擬似的にTypeScriptに書き直すとすると（実際はTypeScriptにはHKTがないため、書くことができない）:
type Maybe<A> = A | null
// TypeScriptはこの
// F<_>のような「型を受け取る型」を、ジェネリクスにできない。
// より踏み込んでいえば、ジェネリクスにできるのは1階層の型で、このような2階層の型をジェネリクスにはできない。
function f<F<_>, A>(x: F<A>): number {
return 10
}
// HKTをサポートしている言語では、2階層**以上**の型もジェネリクスにできる。
// 例えばG<_<_>>のような「「型を受け取る型」を受け取る型」もジェネリクスにできる。
const result: number = f<Maybe, boolean>(true) // => 10
参考:
Scala
Haskell同様にHKTが手厚くサポートされており、（特にScala3が）Haskellよりもモダンだが、操作に型をつけても処理の制限ができなくなった。
しかし、かなりモダン。
これは正しく型チェックエラーになる:
// 前述のHaskellのコードと同じ、HKTの例
// 「型を受け取る型」の一例
enum Maybe[A]:
case Nothing
case Just(value: A)
def f[F[_], A](x: F[A]): Int = 10
val result: Int = f(Maybe.Just(true)) // => 10
これらは型チェックエラーにならない:
// Haskellと違い、IO型なしに副作用を書ける（型で制限されない）
def thisHasUnknownSideEffect(): Int =
println("so bad") // IOでないが、出力できてしまう
42
// cats-effectなどのライブラリを使えば型での明示も可能だが ―
import cats.effect.IO
val impureFunction: IO[Int] = IO {
println("side effect")
42
}
// ― あくまで明示なので、型をつけずに副作用を書いてしまうこともできる
import cats.data.State
val stateful: State[Int, Unit] = State { s =>
println("so bad") // IOでない中でも普通に書ける
(s + 1, ()) // （この戻り値の形は、今は特に気にしなくていいやつ。Stateの作法。）
}
型システムからは若干離れるのでここでは語らないが、Scala3のモダンな部分に興味があれば、筆者は型クラス周りの仕様をおすすめする。
参考:
Idris
Haskellをかなりベースにしている印象の言語。
おそらく本当に、Haskellを参考にしている気がする。
依存型という、例えば「要素の数が5つのという情報を型引数にもつ型Vector 5 Int」のような応用ができるものがある。
またcovering・partial・totalという、「例外を投げるか・無限ループ（無限再帰）をするか・それともしないか」という、関数の性質を区別する機能もある。
【依存型】
これは正しく型チェックエラーになる:
import Data.Vect
-- 要素数が型に含まれるVect（依存型の例）
-- これは正しい。vec変数は型チェックエラーにならない
vec : Vect 3 Int
vec = [1, 2, 3]
-- 要素数が合わないので型チェックエラー！
badVec : Vect 2 Int
badVec = vec
-- 1/1: Building Main (Main.idr)
-- Error: While processing right hand side of badVec. When unifying:
-- Vect 3 Int
-- and:
-- Vect 2 Int
-- Mismatch between: 1 and 0.
【total】
これは正しく型チェックエラーになる:
-- total: ケースが網羅されていて、かつ例外が起きないことを保証できる（無限ループや無限再帰・例外を禁止できる）
-- これはケースを網羅していないので、型チェックエラー！
total
badCountdown : Nat -> List Nat
badCountdown Z = [Z]
-- badCountdown (S n) = (S n) :: countdown n -- 必要な部分をコメントアウトしてみる
-- Error: badCountdown is not covering.
--
-- Main:4:1--5:31
-- 4 | total
-- 5 | badCountdown : Nat -> List Nat
--
-- Missing cases:
-- badCountdown (S _)
これは正しく、型チェックエラーにならない（ならないのが正しい。正常なコード）:
-- これは正しい。ケースを網羅しているので型チェックエラーにならない
total
countdown : Nat -> List Nat
countdown Z = [Z]
countdown (S n) = (S n) :: countdown n
main : IO ()
main = print $ countdown 5 -- [5, 4, 3, 2, 1, 0]
【partial】
これは正しく、型チェックエラーにならない（ならないのが正しい。正常なコード）:
-- partial: ケースが網羅されていないこと・例外が起きる可能性があることを明示する（無限ループや無限再帰も許可する）
-- ケースを網羅していない
partial
badCountdown : Nat -> List Nat
badCountdown Z = [Z]
-- badCountdown (S n) = (S n) :: countdown n
partial -- badCountdownがpartialなので、mainにもpartialが必要
main : IO ()
main = print $ badCountdown 5
-- ↓ 実行時エラー（型チェックエラーではない）
-- ERROR: Unhandled input for Main.betterCountdown at Main:5:1--5:24
-- 例外を出す例（通常は使用しない）
partial
badCountdown : Nat -> List Nat
badCountdown Z = [Z]
badCountdown (S x) = idris_crash "badCountdown does not handle S n" -- 例外を投げる
partial
main : IO ()
main = print $ badCountdown 5
-- ↓ 実行時エラー（型チェックエラーではない）
-- ERROR: badCountdown does not handle S n
【covering】
-- covering: ケースが網羅されていていること・例外が出ないことを保証するが、無限ループ（無限再帰）が起きることを許す
covering
forever : Nat -> Nat
forever n = forever (n + 1) -- 無限再帰する
forever' : Nat -> Nat -- Idrisはデフォルトでcoveringなので、total・partial・coveringを明示しなかった場合は、coveringになる
forever' n = forever (n + 1)
covering -- 前述のため、このcoveringも書く必要はないが、書いてもよい
main : IO ()
main = do
putStrLn "Start"
print $ forever 0
putStrLn "End" -- 出力されない
ところで、前述の total countdown をもう一度見てほしい。
total
countdown : Nat -> List Nat
countdown Z = [Z] -- 基底ケース（0のとき）
countdown (S n) = (S n) :: countdown n -- 帰納ステップ（nで成り立つなら、n+1でも成り立つ）
これは実は、数学の帰納法そのものになっている。
型チェッカーが証明の正しさを、型チェック時に検証している。
この「型チェック時の証明」は、より先進的なバグの予防手法である。
[4]
-- 「長さnのVect」と「長さmのVect」を「長さn + mのVect」に連結する関数
total
vAppend : Vect n a -> Vect m a -> Vect (n + m) a
vAppend [] ys = ys -- 基底ケース
vAppend (x :: xs) ys = x :: vAppend xs ys -- 帰納ステップ
-- 実装を間違えてみる（要素を1つ落とす）:
-- vAppend (x :: xs) ys = vAppend xs ys
-- ^^^^^^^^^^^^^^^^^^^^^^^^^^^
-- → コンパイルエラー！ Vect (n + m) a と Vect (pred n + m) a が合わない
要するに型が「長さnと長さmのリストを連結すると、結果のリストの長さはn + mになる」という命題になっていて、
vAppend : Vect n a -> Vect m a -> Vect (n + m) a
その実装
vAppend [] ys = ys
vAppend (x :: xs) ys = x :: vAppend xs ys
が証明になっている。
（なぜなら前述のようにここを誤ると、型チェックエラー（= 証明失敗）になるから。）
この関数が型チェックをパスした時点で、「連結後の長さがおかしい」というバグは原理的に起きない。
この「型が命題」に、「実装が証明」に対応していることを「カリー・ハワード同型対応」と呼ぶ。
つまり
「これがプログラミングにおける『証明』であり、おそらくはカリー・ハワード同型対応の、重要なひとつの通過点である。」
なのだ、ということを主張しておきたい。
参考:
- Idris 2 Documentation
- Idris-lang.org（公式サイト・解説あり）
Koka
Haskellのように、型で操作が制限できる。
また代数エフェクトというもので、高機能なtry-catchや限定継続などなどができる。
Idrisのように、例外を投げたり無限再帰をしたりするか否かも、区別されている。
正直Kokaの代数エフェクトは難しいので、ここではコード例の紹介に留める。
故に、理解しなくてもよい。
ここに関しては、読むのをスキップしてもよい。
これは正しく、型チェックエラーにならない（ならないのが正しい）:
// エフェクトが型に現れる
// exn エフェクト: 例外が起きうる
fun divide(x: int, y: int): exn int
if y == 0 then throw("division by zero")
else x / y
// div エフェクト: 無限再帰・無限ループが起きうる
fun loop(): div int
loop()
// io エフェクト: 入出力を行う関数
fun greet(name: string): io ()
println("Hello, " ++ name)
// 純粋関数はioエフェクトを持たない
fun double(x: int): int
x * 2
// 代数エフェクトハンドラー（try-catchの発展版）
fun safe-divide(x: int, y: int): int
with handler
return(r) -> r
throw(_) -> 0
divide(x, y)
参考:
- Koka Language Documentation
- Microsoft Research - Koka（研究プロジェクトページ・解説あり）
終わりに
ここまで
- C・C++のような、弱い型システムを持つ言語
- Java・C#のような、強い型システムを持つが、型の表現力は弱い言語
- TypeScriptのような、強い型システムとそこそこの表現力を持つが、意図的に壊れやすく設計され、型の表現力もまだ弱い言語
- Haskellのような、強い型システムと高い表現力（HKTなど）を持つ言語
- Scalaのような、強い型システムと高い表現力（HKTなど）を持つが、処理に型をつけることが強制されない言語
- Idrisのような、強い型システムと高い表現力（HKTなど）、さらに依存型による証明機構を持つ、プログラミングと数学的証明が融合した言語
- Kokaのような、なんかすごいいい感じの強い言語
を見てきた。
これを読んだ皆さんには、ぜひともIdrisレベルの言語を実用に持っていって…
とかはまあしなくてもいいので、
型システムに興味を持ってくれるとうれしい。
-
より正確には「型理論を基礎として設計されたシステム」 ↩︎
-
C++のテンプレートメタプログラミング（TMP）を使うと、我々が通常の（値の）関数で値を計算するように、型を型関数（テンプレート）で型を計算できる。この記事をもし初学者が見たときに、難解さゆえに脳を壊す恐れがあるため、ここでは解説しない。ただしすばらしく興味深いものなので、興味がある場合は
constexprと合わせて調べてみてほしい。 ↩︎ -
ここで「処理」と言っているが、これは必ずしも「関数」を表さない。例えば
putFoo = putStrLn "foo" :: IO ()のような「IO ()の式」は関数ではない。引数を受け取っていないことからわかる。IOとputStrLnについては、後述の例を参照。 ↩︎ -
Idrisが生まれたのは2011年なので、正確には先進的でもなんでもなく、現代のバグ予防手法は数年前よりも遅れていることになる。なんならAgda2は2007年に生まれている。（Idrisと似て、依存型が使え、Idrisほどの距離ではないものの、プログラミングにより距離が近い言語。） ↩︎
Discussion
とてもおもしろかったです。
Haskell HKTの部分ですが、ローカルで実行してみると以下のエラーがでました。
これが正しい(?)と思ったのでコメントします。私が間違っていたらご放念ください。
おそらくsigmaさんの例が正しいです
ありがとうございます！
修正Done🙏✨