idris- 類似Haskell的純函數編程語言

jopen 8年前發布 | 12K 次閱讀

Idris是一個類似Haskell的純函數編程語言，類型系統支持dependent types。

  • 依賴模式匹配的依賴類型系統

  • 簡單的C函數接口

  • 編譯器級別的編碼支持

  • where 語句, with 規則, 簡單的case 表達式, 模式匹配 let 和 lambda 綁定

  • Dependent records with projection and update

  • Type classes

  • 類型驅動的重載方案

  • do notation and idiom brackets

  • 縮進語法

  • 可擴充的語法

  • Cumulative universes

  • 整體驗證

  • 類似Hugs的交互環境 

data Nat     = Z       | S Nat
data Maybe a = Nothing | Just a
data List a  = Nil     | (::) a (List a)
(+) : Nat -> Nat -> Nat
Z     + y = y
(S k) + y = S (k + y)
infixr 5 ::
data Vect : Nat -> Type -> Type where
    Nil  : Vect Z a
    (::) : a -> Vect k a -> Vect (S k) a
app : Vect n a -> Vect m a -> Vect (n + m) a
app Nil       ys = ys
app (x :: xs) ys = x :: app xs ys

官方網站：http://www.baiduhome.net/lib/view/home/1452516194808


 本文由用戶 jopen 自行上傳分享，僅供網友學習交流。所有權歸原作者，若您的權利被侵害，請聯系管理員。
 轉載本站原創文章，請注明出處，并保留原始鏈接、圖片水印。
 本站是一個以用戶分享為主的開源技術平臺，歡迎各類分享！