自 Idris 1 以来的变化

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

Type Driven Development with Idris: Updates Required 章节描述了这些更改如何影响由 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
  aVisibile 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

This fails because n is in scope already, from the type of showVect, in the type declaration for showBody, and so the first clause showBody [] will fail to type check because [] has length Z, not n. We can fix this by locally binding n:

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

Or, alternatively, using a new name:

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

Idris 1 took a different approach here: names which were parameters to data types were in scope, other names were not. The Idris 2 approach is, we hope, more consistent and easier to understand.

Function application syntax additions

From now on you can utilise the new syntax of function applications:

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

There are three additions here:

1. More than one argument can be written in braces, separated with commas:

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. Arguments in braces can now correspond to explicit, implicit and auto implicit dependent function types (Pi types), provided the domain type is named:

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

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

Order of the arguments doesn’t matter as long as they are in braces and the names are distinct. It is better to stick named arguments in braces at the end of your argument list, because regular unnamed explicit arguments are processed first and take priority:

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

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

This snippet won’t type check, because “b” in badCall is passed first, although logically we want it to be second. Idris will tell you that it couldn’t find a spot for a = "a" (because “b” took its place), so the application is ill-formed.

Thus if you want to use the new syntax, it is worth naming your Pi types.

3. Multiple explicit arguments can be “skipped” more easily with the following syntax:

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

or

f {}

in case none of the named arguments are wanted.

Examples:

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 _ _

Last rule worth noting is the case of named applications with repeated argument names, e.g:

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

In this example the name x is given repeatedly to the Pi types of the data constructor MkWeirdPair. In order to deconstruct the WeirdPair a b in weirdSnd, while writing the left-hand side of the pattern-matching clause in a named manner (via the new syntax), we have to rename the first occurrence of x to any fresh name or the _ as we did. Then the definition type checks normally.

In general, duplicate names are bound sequentially on the left-hand side and must be renamed for the pattern expression to be valid.

The situation is similar on the right-hand side of pattern-matching clauses:

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 }

Named arguments should be passed sequentially in the order they were defined in the Pi types, regardless of their (imp)explicitness.

Better inference

In Idris 1, holes (that is, unification variables arising from implicit arguments) were local to an expression, and if they were not resolved while checking the expression, they would not be resolved at all. In Idris 2, they are global, so inference works better. For example, we can now say:

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

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

The ?, incidentally, differs from _ in that _ will be bound as an implicit argument if unresolved after checking the type of test, but ? will be left as a hole to be resolved later. Otherwise, they can be used interchangeably.

Dependent case

case blocks were available in Idris 1, but with some restrictions. Having better inference means that case blocks work more effectively in Idris 2, and dependent case analysis is supported.

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

The implicit arguments and original values are still available in the body of the case. Somewhat contrived, but the following is valid:

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

Record updates

Dependent record updates work, provided that all relevant fields are updated at the same time. Dependent record update is implemented via dependent case blocks rather than by generating a specific update function for each field as in Idris 1, so you will no longer get mystifying errors when trying to update dependent records!

For example, we can wrap a vector in a record, with an explicit length field:

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

Then, we can safely update the content, provided we update the length correspondingly:

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

Another novelty - new update syntax (previous one still functional):

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

The record keyword has been discarded for brevity, symbol := replaces = in order to not introduce any ambiguity.

Generate definition

A new feature of the IDE protocol supports generating complete definitions from a type signature. You can try this at the REPL, for example, given our favourite introductory example…

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

…assuming this is defined on line 3, you can use the :gd command as follows:

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

This works by a fairly simple brute force search, which tries searching for a valid right hand side, and case splitting on the left if that fails, but is remarkably effective in a lot of situations. Some other examples which work:

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

This is available in the IDE protocol via the generate-def command.

Chez Scheme target

The default code generator is, for the moment, Chez Scheme. Racket and Gambit code generators are also available. Like Idris 1, Idris 2 supports plug-in code generation to allow you to write a back end for the platform of your choice. To change the code generator, you can use the :set cg command:

Main> :set cg racket

Early experience shows that both are much faster than the Idris 1 C code generator, in both compile time and execution time (but we haven’t done any formal study on this yet, so it’s just anecdotal evidence).