問題を解決するつもりでキッチリ型を付けた先にある高い壁 - ぼくのぬまち 出張版

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

[atsushifx]

問題を解決するツールができても、問題そのものの難しさが変わらない罠。言語やシステムの機能をきっちり使えるのであれば、RDB設計で制約を使っているはず

[tsimo]

“型レベルへ条件を持ち上げることは「人はミスせずに作業ができるか」という問題を「人は定理証明ができるか」という問題へと変換すること”

[tackman]

ですよね〜〜なんとなくそういう気はしていました

[n314]

Haskellで言うと、IOを外すときだけガチガチにチェックしてそれ以外はゆるくやりたい、的な。

[pandaman64]

先行研究

[ruicc]

僕が考えてるやつはこの延長線上とは少し違うかもしれないんだけどまあ僕の型と触れ合う時間が少なすぎるというのはある