ていうか、Haskellとかその辺の型システム（以下『前者』）って、人間と計算機の間の齟齬を最小限にしつつも記述を簡潔にする為にあって、Adaとかそっち方面の型システムは、前者の応用で、人間と人間でも（もっと言うとあるひとりのプログラマ自身と自身でも）齟齬を起こさないために明示的に意思を毎回わざわざ確認する、ある種の意思決定システムなので、なんと言うか、数学と工学のようというか、理学と工学のような、基礎と応用（？）の関係みたいな違いがある？＞＜
フォロー
それを踏まえると単に「型システム」と言うと、Haskellerが思い浮かべる物を指す方がより正確（？）なんだろうけど、じゃあ『その応用でAdaみたくガチガチで頭堅くて「明示的！！明示的記述！！命名せよ！！！暗黙は人を殺すミスを犯す！！！」みたいな、型を書かせる事によって齟齬を検出する意味での型システム』ってなんて言うんだろ？＞＜
雑に言うと、Haskellerがいう型システムだと「『リンゴが3つ』と『バナナが3つ』はこの場合は同じ」みたいな発想だけど、Ada的発想でいう型システムだと「まず果物にそろえよ！ そもそもバナナが3つってなんだ！？ 房か！？本数か！？質量か！？ 数え方と単位も明示せよ！」って感じかも？＞＜
前者だと現在の小学校の算数の教え方とあんまり変わらない・・・＞＜
Ada方式の方が小学校1年生くらい？での「1ってなに？ なんで1の次は2なの？」とか「おにぎり＋おにぎりはでっかいおにぎりじゃん！？ さんすうわけわからない さんすうきらい・・・」みたいなことを小学校で教えたり救ったりできるかも？＞＜