ふーん、関数型を前提としない型理論って聞いたことなかったです