《Type Driven Development with Idris》：所需更新

Edwin Brady 所著《Type-Driven Development with Idris》（可在 Manning 出版社获取，<https://www.manning.com/books/type-driven-development-with-idris>）一书中的代码大部分可在 Idris 2 中运行，但需做一些小的修改，详见本文档。更新后的代码也将成为测试套件的一部分（见 Idris 2 源码中的 tests/typedd-book 目录）。

如果你是 Idris 新手，并通过本书学习，建议先用 Idris 1 完成前 3-4 章的内容，这样无需关心本文档中提到的变更。之后如需继续，可参考本文件进行必要的修改。

第 1 章

输入 the Double (2.1 * 20)，而不是 2.1 * 20。

在 REPL 中运行 Hello.idr 时，输入 :exec main，而不是 :exec。

第 2 章

Prelude 比 Idris 1 更精简，许多函数已移至基础库。因此：

在 Average.idr 中添加：

import Data.String -- for `words`
import Data.List -- for `length` on lists
import System.REPL -- for `repl`

输入 the Double (6.0 + 3 * 12)，而不是 6.0 + 3 * 12。

在 AveMain.idr 和 Reverse.idr 中添加：

import System.REPL -- for 'repl'

在 REPL 中运行 AveMain.idr 的 main 时，输入 :exec main，而不是 :exec。

第 3 章

未绑定隐式参数的多重性为 0，因此运行时无法对其进行模式匹配。因此，在 Matrix.idr 中，需要修改 createEmpties 和 transposeMat 的类型，使得内部向量的长度可用于匹配：

createEmpties : {n : _} -> Vect n (Vect 0 elem)
transposeMat : {n : _} -> Vect m (Vect n elem) -> Vect n (Vect m elem)

出于同样原因，还需将 length 的类型修改为：

length : {n : _} -> Vect n elem -> Nat

第 4 章

基于上述原因：

  • 在 DataStore.idr 中添加 import System.REPL 和 import Data.String

  • 在 SumInputs.idr 中添加 import System.REPL

  • 在 TryIndex.idr 中添加一个隐式参数：

tryIndex : {n : _} -> Integer -> Vect n a -> Maybe a

  • 在 4.2 练习 5 中，添加一个隐式参数：

sumEntries : Num a => {n : _} -> (pos : Integer) -> Vect n a -> Vect n a -> Maybe a

第 5 章

虽然存在 String 到 Nat 的 Cast 实例，但其在 String 非数字时返回 Z 的行为容易引起混淆且易出错。现在推荐使用 Data.String 中的 stringToNatOrZ，其命名更清晰。因此：

在 Loops.idr 和 ReadNum.idr 中，建议添加 import Data.String 并将 cast 替换为 stringToNatOrZ。

在 ReadNum.idr 中，由于函数现在默认要求 covering，请为 readNumbers_v2 添加 partial 注解。（即书中第 135 页的 readNumbers 版本。）

第 5.3.4 节练习所需的文件操作函数已不在 Prelude 中。请导入 System.File.Handle 和 System.File.ReadWrite。

第 6 章

在 DataStore.idr 和 DataStoreHoles.idr 中添加 import Data.String 和 import System.REPL。此外，DataStore.idr 中 display 的 schema 参数需要用于匹配，因此请将类型修改为：

display : {schema : _} -> SchemaType schema -> String

在 TypeFuns.idr 中添加 import Data.String

清单 6.9 中 data Schema 声明了一个尚未定义的类型。在 Idris2 中，必须加冒号和类型：

data Schema : Type

第 7 章

Abs 现在已从 Neg 拆分为独立接口。因此，请将 eval 的类型修改为显式包含 Abs：

eval : (Abs num, Neg num, Integral num) => Expr num -> num

同时，将 abs 从 Expr 的 Neg 实现中移除，并添加如下 Abs 实现：

Abs ty => Abs (Expr ty) where
    abs = Abs

第 8 章

在 AppendVec.idr 中添加 import Data.Nat 以支持 Nat 证明

cong 现在需要显式传入要应用的函数。因此，在 CheckEqMaybe.idr 中将最后一个分支修改为：

checkEqNat (S k) (S j) = case checkEqNat k j of
                              Nothing => Nothing
                              Just prf => Just (cong S prf)

CheckEqDec.idr 也需做类似修改。

在 ExactLength.idr 中，exactLength 的 m 参数运行时需要，因此请将类型修改为：

exactLength : {m : _} ->
              (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)

ExactLengthDec.idr 也需做类似修改。此外，DecEq 已不在 prelude 中，请添加 import Decidable.Equality。

在 ReverseVec.idr 中添加 import Data.Nat 以支持 Nat 证明。

在 Void.idr 中，由于函数现在默认要求 covering，请为 nohead 及其辅助函数 getHead 添加 partial 注解。

在 8.2.5 练习 2 中，reverse' 的定义应改为 reverse' : Vect k a -> Vect m a -> Vect (k + m) a，否则 reverse' 中的 n 会与 myReverse 签名中的 n 绑定为同一值。

第 9 章

  • 在 ElemType.idr 中添加 import Decidable.Equality

  • 在 Elem.idr 中添加 import Data.Vect.Elem

在 Hangman.idr 中：

  • 添加 import Data.String、import Data.Vect.Elem 和 import Decidable.Equality

  • removeElem 对 n 进行模式匹配，因此需要在类型中显式写出：

removeElem : {n : _} ->
             (value : a) -> (xs : Vect (S n) a) ->
             {auto prf : Elem value xs} ->
             Vect n a

  • letters 被 processGuess 使用，因为它会传递给 removeElem：

processGuess : {letters : _} ->
               (letter : Char) -> WordState (S guesses) (S letters) ->
               Either (WordState guesses (S letters))
                      (WordState (S guesses) letters)

  • guesses 和 letters 是 game 的隐式参数，但在定义中被使用，因此需要在类型中显式写出：

game : {guesses : _} -> {letters : _} ->
       WordState (S guesses) (S letters) -> IO Finished

在 RemoveElem.idr 中

  • 添加 import Data.Vect.Elem

  • removeElem 需按上述方式更新。

第 10 章

本章需要做大量修改，尤其是在构造视图时，因为 Idris 2 的统一（unification）实现更加精确和严格，递归 with 应用的规则也更严格。

在 MergeSort.idr 中添加 import Data.List

在 MergeSortView.idr 中添加 import Data.List，并将视图的参数显式写出：

mergeSort : Ord a => List a -> List a
mergeSort input with (splitRec input)
  mergeSort [] | SplitRecNil = []
  mergeSort [x] | SplitRecOne x = [x]
  mergeSort (lefts ++ rights) | (SplitRecPair lefts rights lrec rrec)
       = merge (mergeSort lefts | lrec)
               (mergeSort rights | rrec)

在 10-1 练习第 1 题中，TakeN 的数据构造器 Exact 的 rest 参数需显式写出。

data TakeN : List a -> Type where
  Fewer : TakeN xs
  Exact : (n_xs : List a) -> {rest : _} -> TakeN (n_xs ++ rest)

在 SnocList.idr 的 my_reverse 中，Snoc rec 与 xs ++ [x] 之间的关联需显式写出。Idris 1 会自动推断 xs 和 x 为 Snoc 的相关隐式参数，但这只是基于类型检查的猜测，而 Idris 2 对统一的要求更精确。因此，x 和 xs 需作为 Snoc 的显式参数：

data SnocList : List a -> Type where
     Empty : SnocList []
     Snoc : (x, xs : _) -> (rec : SnocList xs) -> SnocList (xs ++ [x])

相应地，模式匹配时也需显式写出。例如：

my_reverse : List a -> List a
my_reverse input with (snocList input)
  my_reverse [] | Empty = []
  my_reverse (xs ++ [x]) | (Snoc x xs rec) = x :: my_reverse xs | rec

snocListHelp 和 my_reverse_help 也需做类似修改。详见 tests/typedd-book/chapter10/SnocList.idr。

此外，snocListHelp 中 input 运行时会用到，因此需在类型中绑定：

snocListHelp : {input : _} ->
               (snoc : SnocList input) -> (rest : List a) -> SnocList (input +

在 snocListHelp 的模式中不再需要显式写出 {input}，但写出来也无妨。

在 IsSuffix.idr 中，模式匹配写法需略作调整。Idris 1 的递归 with 应用其实不应允许这种写法！注意 Snoc - Snoc 分支必须写在最前，否则 Idris 会对 input1 和 input2 进行 case tree 分裂，而不是对 SnocList 对象分裂，导致许多分支被判定为缺失。

isSuffix : Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (snocList input1, snocList input2)
  isSuffix _ _ | (Snoc x xs xsrec, Snoc y ys ysrec)
     = (x == y) && (isSuffix _ _ | (xsrec, ysrec))
  isSuffix _ _ | (Empty, s) = True
  isSuffix _ _ | (s, Empty) = False

不过，这样写仍无法通过完备性检查器，因为它无法识别 pair 内部结构。

在第 10-2 节后练习 4 的 VList 视图中，请从 contrib 库导入 Data.List.Views.Extra。

在 DataStore.idr 中：这有点尴尬——我也不清楚 Idris 1 是怎么让它通过的！可能是它在统一时太"热心"了。修正方法：为 StoreView 增加一个 schema 参数，并将 SNil 的类型改为显式指定 empty 是 DataStore 中定义的函数。同时将 SAdd 的 entry 和 store 参数显式写出：

data StoreView : (schema : _) -> DataStore schema -> Type where
     SNil : StoreView schema DataStore.empty
     SAdd : (entry, store : _) -> (rec : StoreView schema store) ->
            StoreView schema (addToStore entry store)

由于 DataStore 记录中的 size 是显式参数，因此在 storeViewHelp 的类型中也需显式写出：

storeViewHelp : {size : _} ->
                (items : Vect size (SchemaType schema)) ->
                StoreView schema (MkData size items)

在 TestStore.idr 中：

  • 在 listItems 中，empty 需写为 DataStore.empty，以明确指代该函数

  • 在 filterKeys 中，SNil 分支存在错误，之前未被发现是因为上文 SNil 的类型问题。应修改为：

filterKeys test DataStore.empty | SNil = []

第 11 章

在 Streams.idr 中添加 import Data.Stream 以支持 iterate。

在 Arith.idr 和 ArithTotal.idr 中，Divides 视图现在需要显式传入被除数和余数，因此在 bound 中需显式写出：

bound : Int -> Int
bound x with (divides x 12)
  bound ((12 * div) + rem) | (DivBy div rem prf) = rem + 1

此外，shiftR 现在对移位次数采用更安全的类型，因此需添加 import Data.Bits：

randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
                   (seed' `shiftR` 2) :: randoms seed'

在 ArithCmd.idr 中，按上述方式更新 DivBy、randoms 和 import Data.Bits，并添加 import Data.String 以支持 String.toLower。

在 ArithCmd.idr 中，按上述方式更新 DivBy、randoms、import Data.Bits 和 import Data.String。此外，导出规则现在按命名空间而非文件生效，因此需从 CommandDo 和 ConsoleDo 命名空间导出 (>>=)。

在 ArithCmdDo.idr 中，由于 (>>=) 已导出，Command 和 ConsoleIO 也需导出。同时按上述方式更新 randoms 和 import Data.Bits。

在 StreamFail.idr 中，为 labelWith 添加 partial 注解。

如需为自定义类型（如 RunIO）支持 do 语法，需要实现 (>>=)``（用于 ``do 块中的值绑定）和 ``(>>)``（用于无绑定的顺序计算）。完整实现见 tests。

例如，以下 do 块会被脱糖为 foo >>= (\x => bar >>= (\y => baz x y))：

do
  x <- foo
  y <- bar
  baz x y

而如下写法会被转换为 foo >> bar >> baz：

do
  foo
  bar
  baz

第 12 章

基于上述原因：在 ArithState.idr 中添加 import Data.String 和 import Data.Bits，并更新 randoms。此外，由于 (>>=) 操作符位于独立命名空间，需设置为 export；在 getRandom 中，DivBy 需额外传入 div 和 rem 参数。

在 ArithState.idr 中，由于 (>>=) 已导出，Command 和 ConsoleIO 也需导出。

Control.Monad.State 中的 evalState 现在需首先传入 stateType 参数。

第 13 章

在 StackIO.idr 中：

  • tryAdd 对 height 进行模式匹配，因此需在类型中显式写出：

tryAdd : {height : _} -> StackIO height

  • height 也是 stackCalc 的隐式参数，但在定义中被使用，因此需在类型中显式写出：

stackCalc : {height : _} -> StackIO height

  • 在 StackDo 命名空间中导出 (>>=)：

namespace StackDo
  export
  (>>=) : StackCmd a height1 height2 ->
          (a -> Inf (StackIO height2)) -> StackIO height1
          (>>=) = Do

在 Vending.idr 中：

  • 在 strToInput 中添加 import Data.String 并将 cast 替换为 stringToNatOrZ

  • 在 MachineCmd 类型中，为 (>>=) 数据构造器添加隐式参数：

(>>=) : {state2 : _} ->
        MachineCmd a state1 state2 ->
        (a -> MachineCmd b state2 state3) ->
        MachineCmd b state1 state3

  • 在 MachineIO 类型中，为 Do 数据构造器添加隐式参数：

data MachineIO : VendState -> Type where
  Do : {state1 : _} ->
       MachineCmd a state1 state2 ->
       (a -> Inf (MachineIO state2)) -> MachineIO state1

  • runMachine 对 inState 进行模式匹配，因此需在类型中显式写出：

runMachine : {inState : _} -> MachineCmd ty inState outState -> IO ty

  • 在 MachineDo 命名空间中，为 (>>=) 添加隐式参数并导出：

namespace MachineDo
  export
  (>>=) : {state1 : _} ->
          MachineCmd a state1 state2 ->
          (a -> Inf (MachineIO state2)) -> MachineIO state1
  (>>=) = Do

  • vend 和 refill 对 pounds 和 chocs 进行模式匹配，因此需在类型中显式写出：

vend : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs)
refill: {pounds : _} -> {chocs : _} -> (num : Nat) -> MachineIO (pounds, chocs)

  • pounds 和 chocs 是 machineLoop 的隐式参数，但在定义中被使用，因此需在类型中显式写出：

machineLoop : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs)

第 14 章

在 ATM.idr 中：

  • 在 runATM 中添加 import Data.String 并将 cast 替换为 stringToNatOrZ

在 Hangman.idr 中添加：

import Data.Vect.Elem -- `Elem` now has its own submodule
import Data.String -- for `toUpper`
import Data.List -- for `nub`

  • 在 Loop 命名空间中导出 GameLoop 类型及其数据构造器：

namespace Loop
  public export
  data GameLoop : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
    (>>=) : GameCmd a state1 state2_fn ->
            ((res : a) -> Inf (GameLoop b (state2_fn res) state3_fn)) ->
            GameLoop b state1 state3_fn
    Exit : GameLoop () NotRunning (const NotRunning)

  • letters 和 guesses 被 gameLoop 使用，因此需在类型中显式写出：

gameLoop : {letters : _} -> {guesses : _} ->
           GameLoop () (Running (S guesses) (S letters)) (const NotRunning)

  • 在 Game 类型中，为 InProgress 数据构造器添加隐式参数 letters：

data Game : GameState -> Type where
  GameStart : Game NotRunning
  GameWon : (word : String) -> Game NotRunning
  GameLost : (word : String) -> Game NotRunning
  InProgress : {letters : _} -> (word : String) -> (guesses : Nat) ->
               (missing : Vect letters Char) -> Game (Running guesses letters)

  • removeElem 对 n 进行模式匹配，因此需要在类型中显式写出：

removeElem : {n : _} ->
             (value : a) -> (xs : Vect (S n) a) ->
             {auto prf : Elem value xs} ->
             Vect n a

第 15 章