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
正文到此结束
热门推荐
相关文章
近期评论
-
你这基本没有更新呀，最近文章显示还是2019年的文章。不符合要求哈
-
关键词：慕云博客 链接：https://www.lilun.me 描述：分享原创文字的个人博客
-
-
-
可以提供一下源码吗
-
不是商业站，鸡娃学习笔记
-
-
-
-
听他们说很厉害的样子
Loading...
![[HBLOG]公众号](http://www.liuhaihua.cn/img/qrcode_gzh.jpg)
