問題を解決するつもりでキッチリ型を付けた先にある高い壁 - ぼくのぬまち 出張版null安全おじさんになりかわりそれがしがお見せつかまつる 機械が理解できる複雑な契約の型表現がもたらすものは つまるところこのようなもの ずぶぶ(切った腹から証明オブジェクトを引き摺り出す)— Noriyuki OHKAWA (@notogawa) 2016年11月18日 過ぎたるは猶及ばざるがごとし． 最近null安全？だかの話のからみで，(静的な)型で契約云々を表現してシアワセになれるんだぜーと言うのをチラホラ見聞きする．たとえば，pythonで統計なり機械学習なりやっててnumpy弄るような人が，ndarray(多次元配列)のshape(多次元配列の形)が合わずエラーで落ちたりとかそういうアレについて云々という．なるほど型があれば実行前に止めることができ，実行時，エラー*1になってファーみたいなことは避けられるだろう． しかし，これが天国へ続く道かどうかはまた別の話．(依存)型で舗
