怎麼評價 Idris 語言？

01-12

請各位大牛從語言設計，語言實現，社區建設上點評一下 Idris 語言，這貨有什麼優缺點？有前途么？和 Haskell 比較的優勢是什麼？

正準備入坑, 剛讀完 Tutorial, 來發表一下感想

大體上看, Idris 這個語言的設計, 基本上是Haskell的延續, 整體上語法和Haskell十分接近, Haskell程序員用起來基本上只會更爽, 不太會有什麼不適 (除了不是默認Lazy這一點需要適應之外).

所以簡而言之, Idris 就是帶 Dependent Type 的 Haskell, 外加各種語法上的改良, 解決了諸多由 Haskell 所遺留的問題, 是 Haskeller 心目中的理想語言.

說一些比較具體的點:

1. Dependent Type. 就不細說了, 畢竟是 Haskeller 朝思暮想的特性, Haskell 加了各種擴展也只是部分支持, 還有各種遺留問題. 現在直接換 Idris 就可以丟掉包袱繼續嗨皮了 (づ??????)づ

2. Nat字面值 (不知道這個名字是不是合適, 有更好的名字請告知). 將 0, 1, 2, 3 ... 和 Z, (S Z), (S (S Z)), (S (S (S Z))) ... 這兩種表示在用戶層面統一了, 這樣用戶不用操心應該用哪種表示了, 只管寫, 編譯器會給你選擇適當的後端處理邏輯, 不用擔心會因為寫成了皮亞諾自然數就影響性能. 官方 Tutorial 上的介紹原文如下:

3. Holes 的語法支持. 這樣一來 "Holes Oriented Programming" 就不再是黑科技而變成官方支持了.

什麼是 Holes ? 大概就是說留個坑後面再寫, 然後讓編譯器幫你推斷這個坑應該滿足的約束這樣子:

為什麼這東西有用呢? 官方解釋是這樣的:

雖然這種語法支持微不足道, 但是顯示出的是百分百的貼心啊, 有木有 (?&>?&

4. Laziness 支持. 雖然 Idris 默認是嚴格求值的, 但是我覺得這個 Laziness 方案的設計還是很到位的, 基本能彌補默認非 Lazy 的不爽. 雖然 Lazy 變成了 explicit 的了, 看起來相比與 Haskell 的默認 Lazy 是加重了程序員的心智負擔, 但其實, 考慮到實際的工程應用代碼中對程序求值策略的可控性的需求, 這種 explicit 其實是降低了用戶控制求值策略的難度的 (不知道這樣有沒有說明白我的意思. 囧). 而且對於 Lazy 的控制, 只需要在類型簽名里註明就好了, 實現代碼的里可以無差別使用立即值和惰性值.

5. Totality 檢查, 能確保某些代碼是總能確定停機並返回期望類型的結果. 雖然可能很多人覺得這個特性在工程應用中意義不大, 但我覺得這個在關鍵應用場景還是有意義的, 另外 Idris 編譯器也會使用這個檢查結果.

6. Constructor Name Overload. 構造器名稱可以被重載, 這個功能真的是太貼心了, 之前寫 Haskell 總是覺得取名字難, 因為名字不能重複使用. 用 Idris 就完全沒有這個問題啦, 聰明的她會自己通過類型推斷來消歧, 還支持通過 Explicit Namespaces 來顯式地消歧. (所以你驚喜地發現, fmap 已經消失了, 直接變成了 map, 如此等等)

7. !-notation . 簡而言之就是比 do 語法糖更甜的語法糖, 直接讓你回到寫 c 的體驗, 但是記住此時你的代碼邏輯的底層還是 Monad 這個抽象, 你的分號仍然是可編程的, 於是你完全沒有了任何拒絕 Monad 的理由!

這個 !-notation大概這麼用:

原理大概就是這樣:

8. Monad Comprehensions. 就是把 Haskell 中的 List Comprehension 擴展到了 Monad 上, 於是像 Maybe 這種類似容器的東西就也可以用類似 List Comprehension 的語法了.

9. Idiom Notation. 就是 &<*&> 的語法糖, 終於不用再連著寫一堆 &<*&> 了. (雞凍

10. Named Implementations. 就是說現在可以給 instance 取個名字了.

這東東有什麼用呢?

看, 終於可以跟 Haskell 里 Sum 和 Product 這種莫名其妙的 datatype 說拜拜了...

(注意: 以上提到的只是 Idris 語言的部分特性, 且都是和 Haskell 作對比的, 所以和 Haskell 相似的部分並未提及

總得來說, Idris 擊中了很多 Haskeller 隱忍了多年的痛點, 讓 FP 實踐變得更舒服了. 可以注意到 Idris 所有語言層面的設計, 在保持理論上的先進的同時, 還不忘立足於解決實踐中遇到的問題. 所有計算機領域的從業者應該都能感受到這一點的難能可貴.

如果說 Haskell 是 Pure FP 編程語言的探索者和先驅的話, 那麼 Idris 就是這個領域的集大成者. Idris 是 FP 社區對於多年 Pure FP 實踐的總結和歸納. 同時它更是將Dependent Type應用於工程實踐的探索者和先驅. 我完全可以想像現在的這點星星之火將在未來的幾十年里發出多麼璀璨耀眼的光芒!

----------------------------- 2017/04/17 更新 ------------------------------

沒想到一個這麼冷門的話題 (目前知乎 Idris 話題的關注者只有59) , 竟然引來這麼多贊 (此處應感謝B大), 感覺這個坑還是要補一下... 畢竟之前沒有認真回答題主的問題 (捂臉

現階段而言, 這個語言最大的問題在於不成熟. 這點在官方FAQ里已經寫得很清楚了.

什麼叫不成熟呢?

一方面是語言本身, 可以看到目前為止github上還有400多個issue沒有解決.

另一方面就是周邊的生態, 比如說parser庫, 官方wiki (idris-lang/Idris-dev) 上列了4個, 其中3個都不可用了... (捂臉

再有就是後端生成的代碼執行效率上, 由於缺少 Haskell 這麼多年的打磨, 性能能不能拼過 Haskell ?

以上這些都是現階段的問題.

然後說到社區的話, 基本上可以說社區成員是 Haskell 社區的子集 (這個暫時沒有數據支持, 只是個人感覺, 有時間的話可以後面搞一個數據分析...).

下面是各個網站上的基本情況:

Github:

Stackoverflow:

作為對比, 放一下 Haskell 的情況:

Github:

Stackoverflow:

Reddit:

額, 畢竟GHC只是mirror到Github上的, 所以這個對比可能意義不大...

總之, 作為一個 "學完找不到工作" 的語言, 能建立一個這樣規模的社區, 我覺得還是很了不起的... (作為對比, 可以參考垠神的yin語言, ((逃...

@霧雨魔理沙說「這門語言很有趣」——這算是很高的評價了吧（笑

我說一點吧：Idris 是極少幾種可以實現強類型 printf 的語言。

特性偏向於真的拿來編程，而非去證定理（儘管也能做），有在 Real world 探索 DT 用處的用意。

比如下面的例子，讓編譯器檢查入口參數是否合法，支持動態傳入的參數哦，只要你給出它符合條件的證據就可以了：

import Data.So


NAMES : List String

NAMES = ["fun", "far"]
InListCheck : String -&> List String -&> Bool

InListCheck s ss with (elemIndex s ss)

	| Just x  = True

	| Nothing = False
InListProof : String -&> List String -&> Type

InListProof s ss = So (InListCheck s ss)
load : (x : String ** InListProof x NAMES) -&> Nat

load (name ** pf) with (elemIndex name NAMES)

	| Just n = n + 1

	| Nothing impossible
-- 沒有問題，輸出 1

load ("fun" ** Oh)

-- 沒有問題，輸出 2

load ("far" ** Oh)

-- 報錯「類型不匹配：True 不是 False」

load ("what" ** Oh)

dynamic_load : String -&> Nat dynamic_load x = case (choose $ InListCheck x NAMES) of Left p =&> load (x ** p) Right p =&> 0

即使不走 Verified 路線的話，Idris 也相當於是自帶 N 多擴展的 Haskell，比如它自帶的 Multi-parameter interface 是相當有用的抽象，可以很好解決 expression problem。

interface Convertible a b where convert : a -&> b Convertible Int Float where convert = prim__toFloatInt Dump a =&> Convertible a String where convert = dump Parse a =&> Convertible String a where convert = parse

另外說幾個坑：

頂層函數必須要寫聲明，相互遞歸也必須標出來……DT 的副作用。
箭頭 → 因為是 Binder 因此無法實現介面，需要用 Morphism 類型倒騰一下。
「命題」和「布爾值」之間的關係會讓很多人困惑，你可以對比下 (==) 與 decEq。
不過儘管語言設計的很好，不論 Edwin 還是社區都對後端和支持庫沒啥興趣，這就導致 Idris 的後端一團稀爛，那個 js 後端不知道是誰寫的……可以考慮對接下 libuv 或者改掉 js 後端之後對接 nodejs。

Idris, a language that will change the way you think about programming (2015)