型駆動開発なるものがあるらしい

ここ数年静的型付けの言語がHOTで、型レベルのプログラミングを意識することが多くなったと思う。

その中で疑問に思ってたのが、数値、文字列レベルでの制約はつけられるけど、

RDBみたく数量等に関しての制約は書けられないという点。

普段はvalidationとしてI/O時に制約をかけているが、そもそも型として制約すればよくないと思って、ChatGPTに聞いてみた。

やっぱり実現している言語はあるらしくF*（エフスター）、Idris という言語が出てきた。

これらの言語では、上記でいうvalidationを依存型という仕組みで解決しているらしい。

どちらも関数型言語の発展型の言語らしいので、前提として関数型言語の知識が必要そう。

これらが普及してない点として、定義するのがかなり複雑になってしまう点があるよう。

型制約が複雑になると、その制約を満たせているかの証明が必要になり、結果としてややこしくなる感じ。

なので、型を定義する側に一定の数学的知識が必要になってくると思われる。

もう少し緩くして、大小比較等や特定の文字列に依存しているかなど、

レベルをもう少し落とした言語とかは出ないのかとも思う。

でもそれだと、現行のモデルのI/Oをvalidで制限かけてあげたりvalidationライブラリを使ったほうがコストが少ないから良いという話になっているのかも。

その観点で見ると、2020年あたりから流行っていると思われるTypeScriptは”丁度いい塩梅”なのかもしれない。