自 Idris 1 以来的变化

Idris 2 主要向后兼容 Idris 1，但有一些小例外。本文档描述了这些变化，大致按照在实践中遇到它们的可能性排序。新特性在最后的章节 新的特性 中描述。

《Type Driven Development with Idris》：所需更新 章节描述了这些更改如何影响由 Edwin Brady 撰写的 《使用 Idris 进行类型驱动开发》 <https://www.manning.com/books/type-driven-development-with-idris> `_ 一书中的代码，可从 `Manning 获得。

备注

Idris 的文档已在知识共享 CC0 许可下发布。因此，在法律允许的范围内，Idris 社区 已经放弃了 Idris 文档的所有版权和相关或邻近的权利。

关于CC0的更多信息，可以在网上找到：http://creativecommons.org/publicdomain/zero/1.0/

新核心语言：类型中的数量

Idris 2 是基于 量化类型理论（QTT） ，这是由 Bob Atkey 和 Conor McBride 开发的核心语言。在实践中，Idris 2 中的每个变量都有一个 数量 与之相关。数量是的取值是下列其中之一：

• 0 ，表示变量在运行时被 擦除

• 1 ，表示变量在运行时 正好使用一次

• 不受限制 ，这与 Idris 1 的行为相同

有关这方面的更多详细信息，请参阅章节 多重性。在实践中，这可能会导致某些 Idris 1 程序由于尝试使用在运行时被擦除的参数而不能通过 Idris 2 的类型检查。

擦除

在 Idris 中，以小写字母开头的名称会自动绑定为类型中的隐式参数，例如在以下骨架定义中， n 、 a 和 m 是隐式绑定的：

append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = ?append_rhs

编译依值类型编程语言的困难之一是决定哪些参数在运行时使用，哪些可以安全地擦除。更重要的是，这也是编程时的困难之一：程序员如何 知道 什么时候会删除参数？

在 Idris 2 中，变量的数量告诉我们它在运行时是否可用。我们可以通过检查 REPL 上的孔来查看 append_rhs 作用域内变量的数量：

Main> :t append_rhs
 0 m : Nat
 0 a : Type
 0 n : Nat
   ys : Vect m a
   xs : Vect n a
-------------------------------------
append_rhs : Vect (plus n m) a

0 旁边的 m, a 和 n 表示它们在范用域内，但在运行时将会出现 0 次，也就是说，将会 保证 它们在运行时会被删除。

如果您在运行时使用隐式参数，这确实会在转换 Idris 1 程序时导致一些潜在的困难。例如，在 Idris 1 中，您可以获得向量的长度，如下所示：

vlen : Vect n a -> Nat
vlen {n} xs = n

这似乎是个好主意，因为它在恒定时间内运行并利用了类型级别的信息，但代价是 n 必须在运行时可用，所以在运行时我们总是需要如果我们调用 vlen 时可用的向量的长度。 Idris 1 可以推断出是否需要长度，但程序员没有简单的方法可以确定。

在 Idris 2 中，我们需要明确指出，在运行时需要 n

vlen : {n : Nat} -> Vect n a -> Nat
vlen xs = n

(顺便说一下，还要注意在 Idris 2 中，在类型中绑定的名字也可以在定义中使用，而不需要明确地重新绑定它们)

这也意味着，当你调用 vlen 时，你需要可用的长度。例如，这将产生一个错误

sumLengths : Vect m a -> Vect n a —> Nat
sumLengths xs ys = vlen xs + vlen ys

Idris 2 会报告：

vlen.idr:7:20--7:28:While processing right hand side of Main.sumLengths at vlen.idr:7:1--10:1:
m is not accessible in this context

这意味着它需要使用 m 作为参数传递给 vlen xs ，在这里它需要在运行时可用，但是 m 在 sumLengths 中不可用，因为它有多重性 0 。

我们可以通过将 sumLengths 的右侧替换成一个孔来更清楚地看到这一点......

sumLengths : Vect m a -> Vect n a -> Nat
sumLengths xs ys = ?sumLengths_rhs

...然后在REPL检查孔的类型：

Main> :t sumLengths_rhs
 0 n : Nat
 0 a : Type
 0 m : Nat
   ys : Vect n a
   xs : Vect m a
-------------------------------------
sumLengths_rhs : Nat

相反，我们需要为 m 和 n 提供无限制多重性的绑定

sumLengths : {m, n : _} -> Vect m a -> Vect n a —> Nat
sumLengths xs ys = vlen xs + vlen xs

请记住，在绑定器上不给出多重性，就像这里的 m 和 n 一样，意味着变量的使用不受限制。

如果你要将 Idris 1 程序转换到 Idris 2 中使用，这可能是你需要考虑的最大问题。但需要注意的是，如果你有绑定的隐式参数，例如...

excitingFn : {t : _} -> Coffee t -> Moonbase t

...那么最好确保 t 真的被需要，否则由于运行时间不必要地建立 t 的实例，性能可能会受到影响！

关于擦除的最后一点说明：试图对一个具有多重性 0 的参数进行模式匹配是一个错误，，除非其值可以从其他地方推断出来。因此，下面的定义会被拒绝

badNot : (0 x : Bool) -> Bool
badNot False = True
badNot True = False

这被拒绝了，错误是：

badnot.idr:2:1--3:1:Attempt to match on erased argument False in
Main.badNot

然而，下面的情况是好的，因为在 sNot 中，尽管我们似乎在被删除的参数 x 上进行了匹配，但它的值是可以从第二个参数的类型中唯一推断出来的

data SBool : Bool -> Type where
     SFalse : SBool False
     STrue  : SBool True

sNot : (0 x : Bool) -> SBool x -> Bool
sNot False SFalse = True
sNot True  STrue  = False

到目前为止，Idris 2 的经验表明，在大多数情况下，只要你在 Idris 1 程序中使用非绑定隐式参数，它们在 Idris 2 中无需过多修改即可工作。 Idris 2 类型检查器将指出你在运行时需要非绑定隐式参数的地方--有时这既令人惊讶又具有启发性！

线性

多重性为 1 的线性参数的完整细节在章节 多重性 中给出。简而言之，多重性 1 背后的直觉是，如果我们有一个具有以下形式的函数......

f : (1 x : a) -> b

...那么类型系统提供的保证是 if f x 只使用一次，然后 x 在此过程中只使用一次 。

Prelude 和 base 库

Idris 1 中的 Prelude 包含很多定义，其中许多很少需要。 Idris 2 中的哲学是不同的。 （相当模糊的）经验法则是它应该包含几乎所有非平凡程序所需的基本功能。

这是一个模糊的规范，因为不同的程序员会考虑不同的东西绝对必要，但结果是它包含：

• 细化器可以脱糖的任何东西（例如元组、 () 、 = ）

• 基本类型 Bool, Nat, List, Stream, Dec, Maybe, Either

• 最重要的实用函数： id 、 the 、composition 等

• 基本类型和基本类型的算术接口和实现

• 基本的 Char 和 String 操作

• Show ， Eq ， Ord ，以及 Prelude 中所有类型的实现

• 基本证明的接口和函数（ cong 、 Uninhabited 等）

• Semigroup, Monoid

• Functor, Applicative, Monad 和相关函数

• Foldable, Alternative 和 Traversable

• Range ，用于列表区间语法

• 控制台 IO

任何不适合此处的内容都已移至 base 库。在其他地方，您可以找到一些曾经在 prelude 中的函数：

• Data.List 和 Data.Nat

• Data.Maybe 和 Data.Either

• System.File 和 System.Directory ，（文件管理以前是 Prelude 的一部分）

• Decidable.Equality

较小的变化

有歧义名称的解析

Idris 1 非常努力地按类型解析有歧义的名称，即使这涉及与接口解析的一些复杂交互。这有时可能是导致类型检查时间过长的原因。 Idris 2 简化了这一点，代价是有时需要对有歧义的名称进行更多的程序员注释。

作为一般规则，Idris 2 将能够区分具有不同具体返回类型（例如数据构造函数）或具有不同具体参数类型（例如记录投影）的名称。如果一个名称需要解析接口，则可能难以解决歧义。如果无法立即解析名称，它将推迟解析，但与 Idris 1 不同，它不会尝试显着回溯。如果你有深度嵌套的有歧义名称（超过一个小阈值，默认为 3），Idris 2 将报告错误。您可以使用指令更改此阈值，例如：

%ambiguity_depth 10

然而，在这种情况下，明确地消除歧义肯定是一个更好的主意。

实际上，一般来说，如果您遇到名称歧义错误，最好的方法是明确给出命名空间。您还可以在局部重新绑定名称：

Main> let (::) = Prelude.(::) in [1,2,3]
[1, 2, 3]

剩下的一个困难是解决有歧义的名称，其中一种可能是接口方法，另一种可能是具体的顶级函数。例如，我们可能有：

Prelude.(>>=) : Monad m => m a -> (a -> m b) -> m b
LinearIO.(>>=) : (1 act : IO a) -> (1 k : a -> IO b) -> IO b

作为一个务实的选择，如果在更具体的名称有效的上下文中进行类型检查（此处为 LinearIO.(>>=) ，因此如果对已知具有类型 IO t 的表达式 t 进行类型检查），将选择更具体的名称。

这在某种程度上令人不满意，所以我们将来可能会重新审视这个！

模块、命名空间和导出

由 private 、 export 和 public export 修饰符控制的可见性规则现在指的是来自其他 命名空间 的名称的可见性，而不是其他 文件 。

因此，如果您有以下内容，且所有内容都在同一个文件中...

namespace A
  private
  aHidden : Int -> Int
  aHidden x = x * 2

  export
  aVisible : Int -> Int
  aVisible x = aHidden x

namespace B
  export
  bVisible : Int -> Int
  bVisible x = aVisible (x * 2)

...然后 bVisible 可以访 aVisible ，但不能访问 aHidden 。

和以前一样，记录在它们自己的命名空间中定义，但字段始终在父命名空间中可见。

此外，模块名称现在必须与定义它们的文件名匹配，但模块 “Main” 除外，它可以在任何名称的文件中定义。

%language 编译指示

Idris 1 中有几个 %language 编译指示，它们定义了各种实验性扩展。这些在 Idris 2 中都不可用，尽管将来可能会定义扩展。

还删除了用于默认可见性的 %access 编译指示，而是在每个声明上使用可见性修饰符。

let 绑定

let 绑定，即 let x = val in e 形式的表达式具有稍微不同的行为。以前，您可以依赖 e 作用域内的 x 的计算行为，因此类型检查可以考虑 x 替换为 val 。不幸的是，这导致了 case 和 with 子句的复杂化：如果我们想保留计算行为，我们需要对 case 和 with 的阐述方式进行重大改变。

所以，为了简单和一致（实际上，因为我没有足够的时间来解决 case 和 with 的问题）上面的表达式 let x = val in e 相当于 (\x => e) val 。

所以， let 现在有效地概括了一个复杂的子表达式。如果您确实需要定义的计算行为，现在可以使用局部函数定义来代替 - 请参阅下面的 局部函数定义 章节。

此外，还可以使用替代语法 let x := val in e 。有关更多信息，请参见 let 绑定 章节。

auto-隐式和接口

接口和 auto-隐式参数是相似的，因为它们调用表达式搜索机制来查找参数的值。在 Idris 1 中，它们是分开实现的，但在 Idris 2 中，它们使用相同的机制。考虑以下 fromMaybe 的 total 定义：

data IsJust : Maybe a -> Type where
     ItIsJust : IsJust (Just val)

fromMaybe : (x : Maybe a) -> {auto p : IsJust x} -> a
fromMaybe (Just x) {p = ItIsJust} = x

由于接口解析和 auto- 隐式现在是同一个东西， fromMaybe 的类型可以写成：

fromMaybe : (x : Maybe a) -> IsJust x => a

所以现在，约束箭头 => 意味着参数将通过 auto 隐式搜索找到。

在定义 data 类型时，可以通过为数据类型提供选项来控制 auto 隐式搜索将如何进行。例如：

data Elem : (x : a) -> (xs : List a) -> Type where
     [search x]
     Here : Elem x (x :: xs)
     There : Elem x xs -> Elem x (y :: xs)

search x 选项意味着 auto-隐式搜索类型为 Elem t ts 的值将在类型检查器解析值 t 后立即开始，即使 ts 仍然未知。

默认情况下， auto - 隐式搜索使用数据类型的构造函数作为搜索提示。数据类型上的 noHints 选项会关闭此行为。

您可以使用函数上的 %hint 选项添加自己的搜索提示。例如：

data MyShow : Type -> Type where
     [noHints]
     MkMyShow : (myshow : a -> String) -> MyShow a

%hint
showBool : MyShow Bool
showBool = MkMyShow (\x => if x then "True" else "False")

myShow : MyShow a => a -> String
myShow @{MkMyShow myshow} = myshow

在这种情况下，搜索 MyShow Bool 会找到 showBool ，如果我们尝试在 REPL 中对 myShow True 求值可以看到：

Main> myShow True
"True"

事实上，这就是接口的详细说明。然而， %hint 应该小心使用。提示过多会导致搜索空间过大！

记录字段

现在可以通过 . 访问记录字段。例如，如果您有：

record Person where
    constructor MkPerson
    firstName, middleName, lastName : String
    age : Int

并且您有一条记录 fred:Person ，那么您可以使用 fred.firstName 访问 firstName 字段。

完全性和覆盖性

%default covering 现在是默认状态，因此所有函数必须覆盖所有输入，除非另有说明 partial 注释，或切换到 %default partial``（不推荐 - 使用 ``partial 注释来代替函数是部分的最小可能位置）。

构建制品

这并不是真正的语言更改，而是 Idris 保存检查文件的方式的更改，并且仍然有用。所有检查的模块现在都保存在源代码树的根目录中的 build/ttc 目录中，目录结构遵循源目录结构。可执行文件放置在 build/exec 中。

包

对其他包的依赖现在用 depends 字段表示， pkgs 字段不再被识别。此外，具有 URLS 或其他字符串数据（模块或包名称除外）的字段必须用双引号引起来。例如：

package lightyear

sourceloc  = "git://git@github.com:ziman/lightyear.git"
bugtracker = "http://www.github.com/ziman/lightyear/issues"

depends = effects

modules = Lightyear
        , Lightyear.Position
        , Lightyear.Core
        , Lightyear.Combinators
        , Lightyear.StringFile
        , Lightyear.Strings
        , Lightyear.Char
        , Lightyear.Testing

新的特性

除了将核心语言更改为使用上述定量类型理论之外，还有其他几个新特性。

局部函数定义

现在可以使用 let 块在局部定义函数。例如，以下示例中的 greet ，它是在局部变量 x 的作用域内定义的：

chat : IO ()
chat
    = do putStr "Name: "
         x <- getLine
         let greet : String -> String
             greet msg = msg ++ " " ++ x
         putStrLn (greet "Hello")
         putStrLn (greet "Bye")

这些“ et 块可以在任何地方使用（在上面的 do 块中间，也可以在任何函数中，或在类型声明中）。 where 块现在通过翻译成局部 let 来阐述。

然而，Idris 不再尝试推断在 where 块中定义的函数的类型，因为这很脆弱。如果我们能想出一个好的、可预测的方法，这可能会被恢复。

隐式参数的作用域

类型中的隐式参数现在在定义主体的作用域内。我们已经在上面看到了，其中 n 自动在 vlen 的主体作用域内：

vlen : {n : Nat} -> Vect n a -> Nat
vlen xs = n

在使用 where 块或局部定义时记住这一点很重要，因为在声明局部定义的 type 时，作用域内的名称也将在作用域内。例如，下面的定义，我们试图为 Vect 定义我们自己的 Show 版本，将无法进行类型检查：

showVect : Show a => Vect n a -> String
showVect xs = "[" ++ showBody xs ++ "]"
  where
    showBody : Vect n a -> String
    showBody [] = ""
    showBody [x] = show x
    showBody (x :: xs) = show x ++ ", " ++ showBody xs

这失败了，因为 n 已经在作用域中，来自 showVect 的类型，在 showBody 的类型声明中，所以第一个子句 showBody [] 将无法通过类型检查，因为 [] 的长度是 Z，而不是 n。我们可以通过局部绑定 n 来修复这个问题：

showVect : Show a => Vect n a -> String
showVect xs = "[" ++ showBody xs ++ "]"
  where
    showBody : forall n . Vect n a -> String
    ...

或者，使用一个新名称：

showVect : Show a => Vect n a -> String
showVect xs = "[" ++ showBody xs ++ "]"
  where
    showBody : Vect n' a -> String
    ...

Idris 1 在这里采用了不同的方法：作为数据类型参数的名称在作用域内，其他名称则不在。我们希望 Idris 2 的方法更加一致且更容易理解。

函数应用语法补充

从现在开始，你可以使用新的函数应用语法：

f {x1 [= e1], x2 [= e2], ...}

这里有三个补充：

1. 多个参数可以用大括号写，用逗号分隔：

record Dog where
  constructor MkDog
  name : String
  age : Nat

-- Notice that `name` and `age` are explicit arguments.
-- See paragraph (2)
haveADog : Dog
haveADog = MkDog {name = "Max", age = 3}

pairOfStringAndNat : (String, Nat)
pairOfStringAndNat = MkPair {x = "year", y = 2020}

myPlus : (n : Nat) -> (k : Nat) -> Nat
myPlus {n = Z   , k} = k
myPlus {n = S n', k} = S (myPlus n' k)

twoPlusTwoIsFour : myPlus {n = 2, k = 2} === 4
twoPlusTwoIsFour = Refl

2. 大括号中的参数现在可以对应显式、隐式和自动隐式依赖函数类型（Pi 类型），只要域类型被命名：

myPointlessFunction : (exp : String) -> {imp : String} -> {auto aut : String} -> String
myPointlessFunction exp = exp ++ imp ++ aut

callIt : String
callIt = myPointlessFunction {imp = "a ", exp = "Just ", aut = "test"}

只要参数在大括号中且名称不同，参数的顺序就不重要。最好将命名参数放在参数列表的末尾，因为常规的未命名显式参数会先被处理并优先：

myPointlessFunction' : (a : String) -> String -> (c : String) -> String
myPointlessFunction' a b c = a ++ b ++ c

badCall : String
badCall = myPointlessFunction' {a = "a", c = "c"} "b"

这段代码无法通过类型检查，因为 badCall 中的 "b" 被首先传递，尽管从逻辑上我们希望它是第二个。Idris 会告诉你它找不到 a = "a" 的位置（因为 "b" 占据了它的位置），所以这个应用是不正确的。

因此，如果你想使用新的语法，值得命名你的 Pi 类型。

3. 多个显式参数可以更容易地使用以下语法"跳过"：

f {x1 [= e1], x2 [= e2], ..., xn [= en], _}

或者

f {}

在所有命名参数都不需要的情况下。

示例：

import Data.Nat

record Four a b c d where
  constructor MkFour
  x : a
  y : b
  z : c
  w : d

firstTwo : Four a b c d -> (a, b)
firstTwo $ MkFour {x, y, _} = (x, y)
-- firstTwo $ MkFour {x, y, z = _, w = _} = (x, y)

dontCare : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
dontCare {} = plusCommutative {}
--dontCare _ _ _ _ _ = plusCommutative _ _

最后值得注意的情况是具有重复参数名称的命名应用程序，例如：

data WeirdPair : Type -> Type -> Type where
  MkWeirdPair : (x : a) -> (x : b) -> WeirdPair a b

weirdSnd : WeirdPair a b -> b
--weirdSnd $ MkWeirdPair {x, x} = x
--                        ^
-- Error: "Non linear pattern variable"
-- But that one is okay:
weirdSnd $ MkWeirdPair {x = _, x} = x

在这个例子中，名称 x 被重复地赋予数据构造器 MkWeirdPair 的 Pi 类型。为了在 weirdSnd 中解构 WeirdPair a b，同时以命名方式（通过新语法）编写模式匹配子句的左侧，我们必须将第一次出现的 x 重命名为任何新名称或像我们那样使用 _。然后定义就能正常通过类型检查。

一般来说，重复的名称在左侧按顺序绑定，必须重命名才能使模式表达式有效。

在模式匹配子句的右侧情况类似：

0 TypeOf : a -> Type
TypeOf _ = a

weirdId : {0 a : Type} -> (1 a : a) -> TypeOf a
weirdId a = a

zero : Nat
-- zero = weirdId { a = Z }
--                      ^
-- Error: "Mismatch between: Nat and Type"
-- But this works:
zero = weirdId { a = Nat, a = Z }

命名参数应该按照它们在 Pi 类型中定义的顺序依次传递，无论它们是（隐式）显式的。

更好的推断

在 Idris 1 中，洞（即由隐式参数产生的统一变量）是表达式局部的，如果在检查表达式时没有解决，它们就永远不会被解决。在 Idris 2 中，它们是全局的，所以推断效果更好。例如，我们现在可以说：

test : Vect ? Int
test = [1,2,3,4]

Main> :t test
Main.test : Vect (S (S (S (S Z)))) Int

顺便说一下，? 与 _ 的区别在于，如果在检查 test 的类型后仍未解决，_ 将被绑定为隐式参数，而 ? 将作为洞留待稍后解决。除此之外，它们可以互换使用。

依赖 case

case 块在 Idris 1 中可用，但有一些限制。更好的推断意味着 case 块在 Idris 2 中工作更有效，并且支持依赖 case 分析。

append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys
    = case xs of
           [] => ys
           (x :: xs) => x :: append xs ys

隐式参数和原始值在 case 的主体中仍然可用。虽然有点做作，但以下是有效的：

info : {n : _} -> Vect n a -> (Vect n a, Nat)
info xs
    = case xs of
           [] => (xs, n)
           (y :: ys) => (xs, n)

记录更新

依赖记录更新可以工作，只要所有相关字段同时更新。依赖记录更新是通过依赖 case 块实现的，而不是像 Idris 1 那样为每个字段生成特定的更新函数，所以在尝试更新依赖记录时，你不再会遇到令人困惑的错误！

例如，我们可以将向量包装在记录中，并带有显式的长度字段：

record WrapVect a where
  constructor MkVect
  purpose : String
  length : Nat
  content : Vect length a

然后，只要我们相应地更新 length，就可以安全地更新 content：

addEntry : String -> WrapVect String -> WrapVect String
addEntry val = { length $= S,
                 content $= (val :: ) }

另一个新特性 - 新的更新语法（之前的语法仍然可用）：

record Three a b c where
  constructor MkThree
  x : a
  y : b
  z : c

-- Yet another contrived example
mapSetMap : Three a b c -> (a -> a') -> b' -> (c -> c') -> Three a' b' c'
mapSetMap three@(MkThree x y z) f y' g = {x $= f, y := y', z $= g} three

为了简洁起见，record 关键字已被弃用，符号 := 替换 = 以避免引入任何歧义。

生成定义

IDE 协议的一个新特性支持从类型签名生成完整的定义。你可以在 REPL 中尝试这个功能，例如，给定我们最喜欢的入门示例...

append : Vect n a -> Vect m a -> Vect (n + m) a

...假设这在第 3 行定义，你可以按如下方式使用 :gd 命令：

Main> :gd 3 append
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

这是通过一个相当简单的暴力搜索实现的，它尝试搜索有效的右侧，如果失败则在左侧进行 case 拆分，但在很多情况下都非常有效。其他一些有效的例子：

my_cong : forall f . (x : a) -> (y : a) -> x = y -> f x = f y
my_curry : ((a, b) -> c) -> a -> b -> c
my_uncurry : (a -> b -> c) -> (a, b) -> c
append : Vect n a -> Vect m a -> Vect (n + m) a
lappend : (1 xs : List a) -> (1 ys : List a) -> List a
zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c

这可以通过 IDE 协议中的 generate-def 命令使用。

Chez Scheme 目标

目前，默认的代码生成器是 Chez Scheme。Racket 和 Gambit 代码生成器也可用。与 Idris 1 一样，Idris 2 支持插件代码生成，允许你为你选择的平台编写后端。要更改代码生成器，你可以使用 :set cg 命令：

Main> :set cg racket

早期经验表明，两者在编译时间和执行时间上都比 Idris 1 的 C 代码生成器快得多（但我们还没有对此进行任何正式研究，所以这只是轶事证据）。