计算机科学

首页 > 计算机科学

Idris

2018-09-05 18:18:24     所属分类:程序设计语言
Idris
编程范型 函数式编程
设计者 Edwin Brady
稳定版本
1.1.1
( 2017年8月5日 (2017-08-05)
型态系统 静态类型, 强类型, 依赖类型
操作系统 跨平台
许可证 BSD-3
文件扩展名 .idr, .lidr
网站 Idris
启发语言
Agda, Coq, Epigram, Haskell, ML

Idris 是一个通用的依赖类型纯函数式编程语言,其类型系统与 Agda 以及 Epigram 相似。

Idris 语言具备堪与 Coq 媲美的交互式定理证明能力,自带 tactics,而其设计目标侧重于通用系统编程更甚于辅助证明。Idris 的其他设计目标还包括“可观的”代码性能,对副作用的控制,以及对于实现嵌入式领域特定语言(Embedded Domain Specific Language,EDSL)的支持。

Idris 通过一个依赖类型的核心语言 TT 生成C语言的中间代码并编译到本地机器码,并利用了一个基于Cheney算法英语Cheney's algorithm的垃圾收集器实现。Idris亦拥有 JavaScript、Java 和 LLVM 的编译器后端。[1]

Idris 的名字来自于20世纪70年代的英国儿童动画片《火车头艾弗英语Ivor_the_Engine#Idris_the_Dragon》里,一条会唱歌的龙。[2]

目录

  • 1 语言特性
    • 1.1 依赖类型
    • 1.2 嵌入式领域特定语言(EDSL)
    • 1.3 类型提供器(Type Provider)
  • 2 示例
    • 2.1 语法
    • 2.2 依赖类型
    • 2.3 求值策略
  • 3 参考文献
  • 4 外部链接

语言特性

依赖类型

Idris 支持对依赖类型()的定义。如下定义了,即元素类型 -元组类型:

data Nat = O | S Nat
infixr 5 ::

data Vect : Type -> Nat -> Type where
    VNil : Vect a O
  | (::) : a -> Vect a k -> Vect a (S k)

嵌入式领域特定语言(EDSL)

Idris 对嵌入式领域特定语言的支持主要包括以下方面[3]

  1. 编译期间求值。
  2. 可重载的语法。
  3. 与C语言库的接口,以及高效的代码生成英语Code generation (compiler)

类型提供器(Type Provider)

Idris 拥有与 F# 相似的类型提供器,它允许编译器在编译期间根据所执行代码的需求而生成新的类型信息。这使得静态类型系统更具可扩展性。[4]

示例

语法

Idris 的语法与 Haskell 有许多相似之处。一个最简单的 Hello World 程序如下:

module Main

main : IO ()
main = putStrLn "Hello, World!"

该程序与 Haskell 的等效写法仅有两点不同:类型签名使用单个冒号“:”而不是双冒号“::”;开头的模块声明中不必使用 where 从句。

Idris 亦支持 where 从句、let 表达式、with 规则、简单的 case 表达式和模式匹配等。

依赖类型

一个在 Idris 中使用依赖类型的示例:

total
append : Vect n a -> Vect m a -> Vect (n + m) a
append Nil       ys = ys
append (x :: xs) ys = x :: append xs ys

该函数将一个包含 m 个类型 a 的元素的 vector 连接到一个包含 n 个类型 a 的元素的 vector 之后。由于输入 vector 的确切类型依赖于它的值,故在编译(类型检查)时即可保证输出的 vector 必将包含 (n + m) 个类型 a 的元素。

关键字“total”将会执行函数的完整性(totality)检查。若函数定义未涵盖所有可能的情形(partial function),则检查器会报错。

另一个使用依赖类型的示例:

total
pairAdd : Num a => Vect n a -> Vect n a -> Vect n a
pairAdd Nil       Nil       = Nil
pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys

Num a 标志着类型 a 属于 Type class英语Type class Num。注意在这里,该函数被认为是完整的(total),尽管并未定义一个参数是 Nil 而另一个参数非 Nil 的模式。原因在于两个作为参数的 vector 只能具备相同的长度,这一点通过依赖类型系统得到了保证,因此在编译时两者长度不同的情形绝无可能发生。这使得该函数定义仍然是完整的。

求值策略

Idris 默认采取及早求值(Eager evaluation),而非 Haskell 的惰性求值(Lazy evaluation)方式。Idris 支持使用 Lazy 关键字显式地指定惰性求值:

data Lazy : Type -> Type where
  Delay : (val : a) -> Lazy a

Force : Lazy a -> a

boolCase : Bool -> Lazy a -> Lazy a -> a;
boolCase True t e = t;
boolCase False t e = e;

参考文献

  1. ^ Idris - News. 
  2. ^ Idris - FAQ. (原始内容存档于2012-03-11). 
  3. ^ Slides from Systems Programming with Dependent Types at DTP11 (PDF). [永久失效链接]
  4. ^ Christiansen, David. Dependent type providers (PDF). 2013. [永久失效链接]

外部链接

  • The Idris homepage, including documentation, frequently asked questions and examples
  • Idris at the Hackage repository
  • Idris Tutorial

版权声明:本文由北城百科网创作,转载请联系管理获取授权,未经容许转载必究。https://www.beichengjiu.com/computerscience/340554.html

显示全文

取消

感谢您的支持,我会继续努力的!

扫码支持
支付宝扫一扫赏金或者微信支付5毛钱,阅读全文

打开微信扫一扫,即可进行阅读全文哦


上一篇:Mama (软件)
下一篇:Iota函数
相关推荐
爱淘宝