开源中国

我们不支持 IE 10 及以下版本浏览器

It appears you’re using an unsupported browser

为了获得更好的浏览体验,我们强烈建议您使用较新版本的 Chrome、 Firefox、 Safari 等,或者升级到最新版本的IE浏览器。 如果您使用的是 IE 11 或以上版本,请关闭“兼容性视图”。
idris首页、文档和下载 - 类似 Haskell 的纯函数编程语言 - 开源中国社区
全部项目分类
我要评价
未知
C/C++
跨平台
分享
收藏
19 人收藏
收录时间:2016-01-11
idris 详细介绍

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



大家对 idris 的评论 (全部 1 条评论)
{{repayCom.userName}}
LSGX
依赖类型 #idris#
顶部