idris- 类似Haskell的纯函数编程语言

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.open-open.com/lib/view/home/1452516194808