OWL やトピック マップで定義できるようなオントロジーを設計しようとしています。これには List[T] などのポリモーフィック型のサポートが含まれます。ここで、T は Interval Kind In(Nothing, Any) の型パラメーターであり、List は関数の種類 * -> *. 最終的には、型システムのオントロジーをセマンティック言語で記述し、同じセマンティック言語で記述されたタイプ セーフなソフトウェア コードの基礎となる十分な詳細と厳密さを備えたいと考えています。
この目標を念頭に置いて、Type、Interval Kind、Function Kind がすべて Kind のインスタンスである Kind の階層構造を理解しようとしています。すべての種類の共通の「スーパーカインド」の正式な名前はありますか? 私が思いつく最良の用語は「親切なインスタンス」です。これは型理論においても意味のある概念ですか? そうでない場合でも、(トピック マップの用語で) 「関数、引数、型、制約の関連付けには、ロールが「許可された型」があり、そのプレーヤーは「種類のインスタンス」型でなければならないというようなことを言うには、そのような概念が必要です。 」。
これを超えて、私はこのプロジェクトのために型理論を独学で学び始めたばかりであり、それを完了する前に学ぶべきことがたくさんあります。Generics of a Higher Kind (http://adriaanm.github.com/files/higher.pdf) を含む型理論に関する scala 関連の論文をいくつか読み、Scala での安全な型レベルの抽象化 ( http://adriaanm.github.com/files/scalina-final.pdf) およびScala のタイプ コンストラクター ポリモーフィズム[pdf]。私は Scala ほど Haskell に精通していませんが、System F with Type Equality Coercions[pdf]などの関連性のある論文に遭遇しました。理解するには、Haskell をより高度に理解する必要があります。Haskell の型システムを初心者レベルから一般化された代数データ型のような高度な原則に至るまで学習するための読み物の進行を提案できる人がいれば、それも大歓迎です。
最後に、OWL やトピック マップなどのセマンティック オントロジー言語で型システムを記述しようとする既存の試みを知っている場合、またはこれを行う方法について何か提案がある場合は、それもぜひ聞かせてください。