Idris是一个类似Haskell的纯函数编程语言，类型系统支持dependenttypes。
依赖模式匹配的依赖类型系统
简单的C函数接口
编译器级别的编码支持
where语句,with规则,简单的case表达式,模式匹配let和lambda绑定
Dependentrecordswithprojectionandupdate
Typeclasses
类型驱动的重载方案
donotationandidiombrackets
缩进语法
可扩充的语法
Cumulativeuniverses
整体验证
类似Hugs的交互环境
data Nat = Z | S Natdata Maybe a = Nothing | Just adata List a = Nil | (::) a (List a)(+) : Nat -> Nat -> NatZ + 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) aapp : Vect n a -> Vect m a -> Vect (n + m) aapp Nil ys = ysapp (x :: xs) ys = x :: app xs ys
评论