什麼是類型理論中的所有類型的所有實例的常見超類型

我試圖設計一個本體，如可以使用OWL或主題地圖定義，包括支持多態類型，如列表[T]其中T是一個Interval Kind In（Nothing，Any）的類型參數，List是函數種類* - > *。最終，我想用語義語言描述一個類型系統本體，它具有足夠的細節和嚴密性，可以成爲用相同語義語言編寫的類型安全軟件代碼的基礎。什麼是類型理論中的所有類型的所有實例的常見超類型

考慮到這個目標，我試圖找出Kinds的層次結構，其中Type，Interval Kind和Function Kind都是Kind的實例。所有種類的共同'超級'有沒有正式名稱？我能想到的最好的詞是'Kind Instance'。這在類型理論中甚至是一個有意義的概念嗎？即使不是這樣，我需要這樣一個概念來說（例如在主題地圖術語中）「一個函數參數類型約束關聯有一個角色'allowed-type'，其玩家必須是類型'Kind Instance 「」。除此之外，我只是開始爲自己的項目教授自己的類型理論，在我能夠完成它之前還有很多東西需要學習。我已經閱讀了一些關於類型理論的scala相關論文，其中包括更高類的泛型（http://adriaanm.github.com/files/higher.pdf），並開始通過Scala中的安全類型抽象（Simple Type-level Abstraction） http://adriaanm.github.com/files/scalina-final.pdf）和Type Constructor Polymorphism for Scala[pdf]。我對Haskell的瞭解比Scala少，但是我遇到了一些相關的論文，如System F with Type Equality Coercions[pdf]，我需要更先進的Haskell理解才能理解。如果任何人都可以建議閱讀材料的進展，從初學者的水平開始學習Haskell的類型系統，並一直引導到先進的原則，如廣義代數數據類型，這也將非常感激。最後，如果您知道任何現有的企圖用OWL或主題地圖等語義本體語言來描述類型系統，或者如果您對如何做到這一點有任何建議，我也很樂意聽到這一點。

來源

2012-12-28 Chris Barnett

類型理論沒有Benjamin Pierce的「類型和編程語言」更好的介紹。我認爲以上種類的標準化名稱不存在，但「排序」是一種常見的選擇。另一個常見的選擇是直接跳轉到依賴類型並將層次扁平化，這樣畢竟只有一個層次。在這種情況下添加一個常見的打字規則（當處理其邏輯內容通常不那麼重要的日常編程語言時）是「Type：Type」規則，因此，例如，3：Int：Type ：類型：類型：...

來源

2012-12-28 02:38:55

IIUC，具有依賴類型和Type：Type規則，存在會導致類型檢查器無限循環的程序 - 但這些程序必須非常努力地嘗試，而不是每天都會發生 - 所以如果你有程序而不是憑證，那麼Type：Type與簡單的選擇相比簡單可能是值得犧牲的。 – luqui

你能給我一個解釋「類型：類型」規則的東西的鏈接，並舉例說明它在實踐中的用途。另外，是否有某種方法可以防止或識別會導致無限循環的程序？這可能會成爲我所考慮的應用程序中的一個安全問題，因爲它涉及執行由第三方編寫的代碼。 –

@ChrisBarnett在CoqArt中有一些關於'Type：Type'的討論; Google也建議http://webcache.googleusercontent.com/search?q=cache:http://adam.chlipala.net/cpdt/html/Universes.html。至於無限循環，好吧，我相信你知道停止問題。基本上你唯一的希望，如果你需要檢查終止是寫保守的東西，然後你不可避免地排除一些有趣的程序。 Coq和Agda擁有非常複雜的終止檢測器，但即使如此，每個開發的某些部分也包括證明事件終止的類型檢測器的滿意度。 –

什麼是類型理論中的所有類型的所有實例的常見超類型

回答

相關問題