Idris

依赖类型

Idris 支持对依赖类型（）的定义。如下定义了，即元素类型 的 -元组类型：
data Nat = O | S Natinfixr 5 ::data Vect : Type -> Nat -> Type where
    VNil : Vect a O
  | (::) : a -> Vect a k -> Vect a (S k)

类型提供器（Type Provider）

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

语法

Idris 的语法与Haskell 有许多相似之处。一个最简单的Hello World 程序如下：
module Mainmain : IO ()main = putStrLn "Hello, World!"
该程序与Haskell 的等效写法仅有两点不同：类型签名使用单个冒号“:”而不是双冒号“::”；开头的模块声明中不必使用where 从句。
Idris 亦支持where 从句、let 表达式、with 规则、简单的case 表达式和模式匹配等。

依赖类型

一个在Idris 中使用依赖类型的示例：
totalappend : Vect n a -> Vect m a -> Vect (n + m) aappend Nil       ys = ysappend (x :: xs) ys = x :: append xs ys
该函数将一个包含m 个类型a 的元素的vector 连接到一个包含n 个类型a 的元素的vector 之后。由于输入vector 的确切类型依赖于它的值，故在编译（类型检查）时即可保证输出的vector 必将包含(n + m) 个类型a 的元素。
关键字“total”将会执行函数的完整性（totality）检查。若函数定义未涵盖所有可能的情形（partial function），则检查器会报错。
另一个使用依赖类型的示例：
totalpairAdd : Num a => Vect n a -> Vect n a -> Vect n apairAdd Nil       Nil       = NilpairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys
Num a 标志着类型a 属于 Type class Num。注意在这里，该函数被认为是完整的（total），尽管并未定义一个参数是Nil 而另一个参数非Nil 的模式。原因在于两个作为参数的vector 只能具备相同的长度，这一点通过依赖类型系统得到了保证，因此在编译时两者长度不同的情形绝无可能发生。这使得该函数定义仍然是完整的。

求值策略

Idris 默认采取及早求值（Eager evaluation），而非Haskell 的惰性求值（Lazy evaluation）方式。Idris 支持使用Lazy 关键字显式地指定惰性求值：
data Lazy : Type -> Type where
  Delay : (val : a) -> Lazy aForce : Lazy a -> aboolCase : Bool -> Lazy a -> Lazy a -> a;boolCase True t e = t;boolCase False t e = e;