依存型
dependent type
型理論
直観主義型理論
型付きラムダ計算
型システム
https://ja.wikipedia.org/wiki/依存型