給 Haskell 用家的 Idris 入坑指南

02-01

沒有 Cabal 或者 Stack 這樣的包管理器，也沒有 Idris Platform 之類的東西，到官網下二進位包解壓完就可以了。
然而，Idris 確實有「包描述文件」ipkg。安裝網上的包的話，你需要把包下載下來，然後運行 idris --install xxx.ipkg。
你幾乎不需要開擴展——因為自帶的功能已經夠多了……擴展幾乎是只牽涉到 ER 元編程、DSL Notation 等少數幾個高級特性。
Idris 默認是嚴格求值的，不過可以用 Lazy 類型實現惰性求值。這個類型是特殊實現的，會自動加上隱式轉換。
Idris 和 Haskell 裡面 : 和 :: 的用法正好相反。: 用於聲明，:: 用於數組連接。表達式中的「卡類型」不用 (x : t) 而是用 the 函數：the t x。
Idris 的頂層函數必須寫類型聲明，而且和 C/C++ 一樣，必須先聲明再使用。相互遞歸的話用 mutual 塊。
對 data，構造器和類型名字不能相同。Edwin 的慣例是用 Mk 前綴，我習慣用 New 前綴。
String 是個原始類型，不是 List Char。可以使用 unpack 函數將 String 轉換為 List Char，用 pack 轉換回來。
用 [] 去圍類型來代表 List 的語法糖是沒有的，需要完整寫 List a。不過，Pair、Unit 的語法糖仍然存在。（雖然……我用 Pair 和 Either 之前鐵定會弄倆運算符 / 和 /。）
Idris 的 Type class 叫做介面（Interface），對應的實例叫做實現（Implementation）。介面的方法中什麼都可以放，包括次級類型。（不過這麼做很容易造成編譯的時候推不出來就是了……）
由於箭頭是 Binder，因此 Idris 的「->」不是一個正常的類型構造符，也無法實現介面。對於非依賴的函數，Data.Morphism 中定義了 Morphism 類型（符號是 ~>），可以像 Haskell 中的 (->) 那樣實現介面。
Idris 允許對於名稱的直接重載，像 (::) 就被重載過（Vect.(::), List.(::), Stream.(::)）。有時候可能需要顯式消歧義來處理推不出來的情況。
Idris 中的 head、index 是不能隨便用的，它們的簽名中有一個命題項 ok，你得說服編譯器「數組不空」或者「沒有越界」。如果不想去哄編譯器的話，可以用 head 和 index，它們返回一個 Maybe。
沒有 fmap、return 和 mapM，用 map、pure 和 traverse。
Haskell 里 Data.Map 對應物是 contrib 包中的 Data.SortedMap，用平衡樹實現的。
因為有 Dependent Type 所以不需要用 Pair 做「鏈表」模擬 Nat。（這條是說給 @帥氣可愛魔理沙聽的。）
deriving 的功能目前由 Elaborator Reflection 元編程實現：derive-all-the-instances。使用的時候需要開啟 ElabReflection 擴展。
Idris 默認的導出規則是 private，因此當你需要導出函數的時候請用 export；導出 data、interface 的時候請用 public export。export 和 public export 的區別是，前者只導出其類型，後者會連同定義一起導出。對於類型別名來說，僅僅以 export 導出會導致使用這個別名的模塊無法把它和它的本體聯繫起來。
Haskell 裡面的 Guard Pattern 在 Idris 裡面可以用 with 實現。
儘管寫證明很美好，不過測試框架還是很有意義的：Idris 中你可以在 ipkg 文件中聲明代表測試的模塊，然後 idris --testpkg xxx.pkg 會運行這些模塊導出的函數進行測試。可以使用 david-christiansen/idris-quickcheck 等模塊輔助測試。
儘管 Idris 有一個 JS 的後端，也有人寫了 JavaScript 的 Binding（IdrisScript），不過這個後端也只是能運行罷了……
網上很多 Idris 編輯器支持的語法文件都停留在幾年前（那個沒有 rewrite、interface 還叫 class 的年代）。然而 VSCode 的插件——vscode-idris 裡面的語法是對的。因為是我改的。
最後，Idris 里有我的代碼，在 RTS 裡面。