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

jopen 8年前

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