Linux学习笔记
当前位置:Linux学习笔记 > Linux 软件 > 正文

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

bbs.yuanmawu.net.jpg

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

未经允许不得转载:Linux学习笔记 » 类似Haskell的纯函数编程语言 idris

赞 (0)
分享到:更多 ()