OCaml中的依賴類型

有很多關於Haskell和Scala中依賴類型的信息。對於OCaml而言，並非如此。有沒有人有足夠的技巧來提供一個關於如何在OCaml中實現這一點的代碼示例（如果可能的話）？當然，（放棄）Dependent ML，但似乎不可能將這些東西納入「常規」OCaml代碼。OCaml中的依賴類型

基本上，我想要做的就是刪除assert(n > 0)之類的代碼，並在編譯時檢查它。

編輯

作爲一個側面說明，這是值得一提的OCaml的Hybrid Contract Checking分支，即可以填補一些的依賴型系統的需要。取而代之的assert(n > 0)你會再編寫一個合同：

contract f = {x : x > 0} -> int 
let f x = x + 1 
let dummy_variable = f (-1) (* Won't compile *)

來源

2013-03-28 Olle Härstedt

請問這是「關於Haskell和Scala中相關類型的大量信息」？儘管對Haskell社區進行了合理的概述，但我不知道你指的是什麼。（我肯定會認爲UPenn在[Dependently-Typed Haskell]（http://www.cis.upenn.edu/~sweirich/）上的工作是相關的，但這是極其研究而非實際的，可能不是「很多」體積）。我不知道你在爲Scala想什麼 - 除了可能與路徑依賴類型的關係？ – gasche

Ehm，在stackoverflow上，我在想。也許我被斯卡拉路徑依賴類型愚弄。 –

參考鏈接是Oleg的lightweight dependent typing頁，實例（OCaml中或可以轉化爲OCaml的）的ML語言中使用依賴般的技術。他在2007年與Chung-chieh Shan在Lighweight static capabilities (PDF)上的論文尤其相關。編輯：從版本4.00（在編寫上述文檔之後發佈）開始，OCaml具有GADT，它可以簡化精煉靜態信息（以前依賴於幻像類型技術）的一些技術，特別是「單例類型」模式在Omega中顯示。已經表明，它們對於獲得強有力的類型編程並不是必不可少的，但它們仍然可以被野外發現的各種示例所使用。

來源

2013-03-29 05:50:45 gasche

OCaml中的依賴類型

回答

相關問題