依存型の土地での果てしない不思議の中で、奇妙な考えが頭に浮かびました。私は多くのデータベースプログラミングを行っていますが、これらの健全性チェックと有効性チェックをすべて取り除くことができればいいと思います. 特に厄介なケースの 1 つは、Integer を受け入れ、それが特定のテーブルの有効な行 ID であることを期待する関数です。非常にばかげた例は次のとおりです。
function loadStudent(studentId: Integer) : Student
私の選択した言語が依存型を完全にサポートしていると仮定すると、型システムを利用してloadStudent有効な値のみを受け入れるようにすることは可能でしょうかstudentId:
function loadStudent(studentId : ValidRowId("students_table") ) : Student
はいの場合、型のデータ コンストラクターを作成するにはどうすればよいValidRowIdですか? これまで見てきた例はすべて純粋なものでした (IO は含まれていません)。