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
正文到此结束
热门推荐
相关文章
近期评论
-
文章和留言都翻到11页了 没有OOM
-
-
朋友，翻页到11页，及以后，会出现OOM，无法访问
-
-
搞个gitee的项目
-
-
版本号是多少，你可以下载哪个代码仓库，jdk选1.8 直接跑就行
-
-
-
Loading...
![[HBLOG]公众号](https://www.liuhaihua.cn/img/qrcode_gzh.jpg)
