型と型安全と、時々、型推論
型と型安全と、時々、型推論
はじまるよ〜〜〜〜〜！！！！
自己紹介
趣味でやっていること
本当に話したかったこと
TypeScriptの型推論の仕組みを
ちょっと見てみる
準備中の様子……
うんうん……
TaPLとか
準備中の様子……
ん？？
TaPLとか
準備中の様子……
そもそも型ってなんだ？
TaPLとか
準備中の様子……
型ってなんだ
準備中の様子……
型ってなんだ
準備中の様子……
型ってなんだ？
準備中の様子……
型ってなんだ？
型ってなんだ？
準備中の様子……
型ってなんだ？
型ってなんだ？
そもそも論から始めて、
型推論はほんの少しだけにします👶
型推論の話は入れられませんでした😭
もっと、そもそも……
そもそも
プログラミング言語
ってなんなのさ
プログラミング言語を作ってみる(とする)
どんなふうに書くことができて、
どんなふうに動くか
を考える必要がある
要するに、2つの要素を考える
どんなふうに書くことができて、
どんなふうに動くか
いわゆる文法: Syntax
いわゆる評価方法: Semantics
(インタプリタはこれに従うってワケ)
syntaxとsemanticsが言語を規定する
ECMAScriptの例
ECMAScript specifications
syntaxとsemanticsが言語を規定する
C言語の例
ISO/IEC 9899:TC3 Committee Draft — Septermber 7, 2007; https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf
👶「syntaxに則っていれば動くんだね！」
syntaxに則っていればいいのか？その1
JavaScriptの例
文法は問題ないが、�nullへのプロパティ�アクセスをしている
👉動かない、エラーでとまる
syntaxに則っていればいいのか？その2
C言語の例
文法は問題ないが、�インデックスが
オーバーしている
👉動くけど、変なことが起きる
syntaxに則っていたらいいわけではない
なぜsyntaxに則っているだけ
ではだめなのか
syntaxは文脈から切り離されている……
ECMAScript specifications
syntaxは文脈から切り離されている……
ISO/IEC 9899:TC3 Committee Draft — Septermber 7, 2007
ECMAScript specifications
syntaxは文脈から切り離されている……
ISO/IEC 9899:TC3 Committee Draft — Septermber 7, 2007
ECMAScript specifications
Haskell 2010 Language Report�https://www.haskell.org/onlinereport/haskell2010/
syntaxは文脈から切り離されている……
ISO/IEC 9899:TC3 Committee Draft — Septermber 7, 2007
ECMAScript specifications
Haskell 2010 Language Report�https://www.haskell.org/onlinereport/haskell2010/
直前までの情報は
文法で考慮されていない
syntaxは文脈から切り離されている……
ISO/IEC 9899:TC3 Committee Draft — Septermber 7, 2007
ECMAScript specifications
Haskell 2010 Language Report�https://www.haskell.org/onlinereport/haskell2010/
直前までの情報は
文法で考慮されていない
やってはじめて、直前までの情報が
コンピューターの状態として顕現して
文法がその状態のもとで評価される
syntaxは文脈から切り離されている……
ISO/IEC 9899:TC3 Committee Draft — Septermber 7, 2007
ECMAScript specifications
Haskell 2010 Language Report�https://www.haskell.org/onlinereport/haskell2010/
直前までの情報は
文法で考慮されていない
やってはじめて、直前までの情報が
コンピューターの状態として顕現して
文法がその状態のもとで評価される
syntaxに沿っていても
プログラムがうまく動くかは
やってみるまでわからない
👶「やってみるまでわからない？本当に？」
何が起きるんだったっけ
などなど……
何が起きるんだったっけ
などなど……
事前にわかる(=静的解析ができる)
ものもありそう……
どうできるだろうか？？
nullが来ないことを確認
数字のみが来ることを確認
変数の定義状態を確認
変数の使用状況を確認
配列の範囲を確認
どうできるだろうか？？
nullが来ないことを確認
数字のみが来ることを確認
変数の定義状態を確認
変数の使用状況を確認
配列の範囲を確認
Rustはこれ
データの種類に関する話があるな？
nullが来ないことを確認
数字のみが来ることを確認
変数の定義状態を確認
変数の使用状況を確認
配列の範囲を確認
データの種類ならなんとかなるのでは？
bにはnullが入っている
という文脈のもとで
下の部分を解析(≠評価)して、だめだよって言えばいいのでは？
データの種類ならなんとかなるのでは？
bにはnullが入っている
という文脈のもとで
下の部分を解析(≠評価)したらいいのでは？
要するに
データの種類という「文脈」を考慮し
プログラムの正しさを解析してみる
理論上、道は少なくとも2つある
理論上、道は少なくとも2つある
文脈依存文法？
https://www.jstage.jst.go.jp/article/jssst/3/4/3_4_377/_pdf/-char/en
属性文法
https://www.jstage.jst.go.jp/article/jssst/3/4/3_4_377/_pdf/-char/en
文脈依存文法？
https://www.jstage.jst.go.jp/article/jssst/3/4/3_4_377/_pdf/-char/en
実装がすごく難しいらしい
(やったわけではないので知らない)
文脈依存文法？
https://www.jstage.jst.go.jp/article/jssst/3/4/3_4_377/_pdf/-char/en
だったら分けよう
「データの種類」という文脈を使った検査を
文法からも評価からもわけてやろう
型検査とは、つまりこういうことだね
型検査とは、つまりこういうことだね
なんだこれ！？
型検査をすれば
プログラムが安全かどうか
やるまえにわかるぞ！
型検査をすれば
プログラムが安全かどうか
やるまえにわかるぞ！
うまく動くとか
安全とかってなに！？
安全という言葉は多義的で、文脈による
いわゆる「型安全性」はここまで
話し手によりさまざま
(本当の本当にオリジナルの定義はたぶん、未定義かどうかが主だと思う)
型安全性は個々の型検査に関する性質だね
👉(通常はあまりないけど)同じ言語でも型検査のやり方が異なれば、厳密には型安全性は変わってくる
型安全性は個々の型検査に関する性質だね
👉でもまあ型検査のやり方含めて言語の仕様だと思うのが普通だよね
👉だから「XXっていう言語は型安全」って言える
まとめ