核心概念
階層的型理論(StraTT)は、型の階層を表す代わりに、型付け判断を階層化することで、一貫性を保ちつつ、より柔軟な型システムを実現する。
摘要
本論文では、階層的型理論(StraTT)を提案している。StraTTの主な特徴は以下の通り:
型の階層を表すのではなく、型付け判断を階層化する。これにより、一貫性を保ちつつ、より柔軟な型システムを実現できる。
階層化された従属関数型に加えて、レベルが浮動する非従属関数型を導入する。これにより、従属関数型では表現できない概念を表現できるようになる。
定数の「displacement」という単純な形式の多相性を導入する。これにより、定数の再利用が容易になる。
サブシステムのsubStraTTについては一貫性が証明されており、StraTT全体については型安全性が証明されている。ただし、完全な一貫性については未解決の問題が残されている。
具体的な例として、決定可能な型、命題的等価性、依存ペアなどを示し、StraTTの表現力を示している。
プロトタイプの型チェッカーを実装し、StraTTの実用性を示している。