OWLまたはトピックマップで定義できるような、List [T]のような多型のサポートを含むようなオントロジーを設計しようとしています。 Interval Kind In（Nothing、Any）の型パラメータであり、ListはFunction Kind * - > *です。最終的には、セマンティック言語の型システム・オントロジーを、同じセマンティック言語で記述された型安全なソフトウェア・コードの基礎となりうるという十分な詳細と厳密性で記述したいと考えています。タイプ理論のKindのすべてのインスタンスの共通のスーパータイプは何ですか
この目標を念頭に置いて、タイプ、間隔の種類、機能の種類がすべてKindのインスタンスである階層の構造を理解しようとしています。すべての種類の共通の「超人」の正式な名前はありますか？私が思いつくことができる最善の言葉は「Kind Instance」です。これは型理論においても意味のある概念ですか？そうでない場合でも、（Topic Mapsの用語では）関数の引数型制約の関連付けにRole 'allowed-type'があり、そのタイプが 'Kind Instance型でなければならない''
これ以外にも、私はこのプロジェクトのための型理論を教え始めたばかりであり、完成する前に多くのことを学ぶ必要があります。私は、Higher Kind（http://adriaanm.github.com/files/higher.pdf）のジェネリックスを含むタイプ理論に関するいくつかのscala関連の論文を読み、ScalaのSafe Type-Level Abstractionを通して作業を開始しました。 http://adriaanm.github.com/files/scalina-final.pdf）およびType Constructor Polymorphism for Scala[pdf]。私はスカスよりハスケルに親しみがありませんが、私は理解するためにははるかに高度な把握が必要なSystem F with Type Equality Coercions[pdf]のような関連性のある論文に遭遇しました。初心者レベルから始めて、一般化された代数データ型のような先進的な原則に至るまで、ハスケルの型システムを学習するための読書資料の進歩を示唆できる人は、大いに感謝しています。
最後に、OWLやTopic Mapsのような意味論的なオントロジー言語でタイプシステムを記述しようとする試みがある場合、またはこれを行う方法についてご提案がありましたら、それも聞きたいです。
依存型とタイプ：タイプのルールを持つIIUCには、型チェッカーに無限ループを引き起こすプログラムが存在しますが、それらのプログラムはかなり難しいですが、そうではありません日常的な出来事なので、証明ではなくプログラムを覚えているなら、一貫した代替案と比較した 'Type：Type'の単純さはおそらく犠牲になるでしょう。 – luqui
"Type：Type"ルールについて説明するリンクを教えてください。実際にどこで使用されているかの例を挙げてください。また、無限ループを引き起こすプログラムを防止または特定する方法がいくつかありますか？これは、第三者によって書かれたコードの実行を伴うので、私が心に留めているアプリケーションではセキュリティ上の問題になる可能性があります。 –
@ChrisBarnett CoqArtに 'Type：Type'の議論があります。 Googleではhttp://webcache.googleusercontent.com/search?q=cache:http://adam.chlipala.net/cpdt/html/Universes.htmlを提案しています。無限ループに関しては、まあ、私はあなたが停止問題について知っていると確信しています。基本的には、終了を確認する必要がある場合は、控えめなものを書くことが唯一の希望であり、必然的に興味深いプログラムを除外します。 CoqとAgdaは非常に洗練された終了チェッカーを持っていますが、すべての開発の一部では、型チェッカーが問題なく終了したことを証明する必要があります。 –