型理論を基礎としたほうが実用的