接口¶

我们经常想要定义能够跨多种不同数据类型工作的函数。例如，我们想要算术运算符至少可以作用于 Int、Integer 和 Double。我们想要 == 作用于大部分的数据类型。我们想要以一种统一的方式来显示不同的类型。

为此，我们使用了 接口（Interface），它类似于 Haskell 中的类型类（Typeclass）或 Rust 中的特性（Trait）。为了定义接口，我们提供了一组可重载的的函数。Show 接口就是个简单的例子，它在 Prelude 中定义，并提供了将值转换为 String 的接口：

interface Show a where
    show : a -> String

它会生成一个类型如下的函数，我们称之为 Show 接口的 方法（Method）：

show : Show a => a -> String

我们可以把它读作：「在 a 实现了 Show 的约束下，该函数接受一个输入 a 并返回一个 String。」我们可以通过为它定义接口的方法来实现该接口。例如，Nat 的 Show 实现可定义为：

Show Nat where
    show Z = "Z"
    show (S k) = "s" ++ show k

Idris> show (S (S (S Z)))
"sssZ" : String

一个类型只能实现一次某个接口，也就是说，实现无法被覆盖。实现的声明自身可以包含约束。为此，实现的参数必须为构造器（即数据或类型构造器）或变量（也就是说，你无法为函数赋予实现）。例如，要为向量定义一个 Show 的实现，我们需要确认其元素实现了 Show，因为要用它来将每个元素都转换为 String：

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

提示

译者更愿意将它读作：对于一个实现了 Show 的 a， Vect n a 对 Show 的实现为……

默认定义¶

库中定义了 Eq 接口，它提供了比较值是否相等的方法，所有内建类型都实现了它：

interface Eq a where
    (==) : a -> a -> Bool
    (/=) : a -> a -> Bool

要为类型实现一个接口，我们必须给出所有方法的定义。例如，为 Nat 实现 Eq：

Eq Nat where
    Z     == Z     = True
    (S x) == (S y) = x == y
    Z     == (S y) = False
    (S x) == Z     = False

    x /= y = not (x == y)

很难想象在哪些情况下 /= 方法不是应用了 == 方法的结果的否定。因此，利用接口声明中的某个方法为其它方法提供默认的定义会很方便：

interface Eq a where
    (==) : a -> a -> Bool
    (/=) : a -> a -> Bool

    x /= y = not (x == y)
    x == y = not (x /= y)

Eq 的最小完整实现只需要定义 == 或 /= 二者之一，而不需要二者都定义。若缺少某个方法定义，且存在它的默认定义，那么就会使用该默认定义。

扩展接口¶

接口也可以扩展。逻辑上，相等关系 Eq 的下一步是定义排序关系 Ord。我们可以定义一个 Ord 接口，它除了继承 Eq 的方法外还定义了自己的方法：

data Ordering = LT | EQ | GT

interface Eq a => Ord a where
    compare : a -> a -> Ordering

    (<) : a -> a -> Bool
    (>) : a -> a -> Bool
    (<=) : a -> a -> Bool
    (>=) : a -> a -> Bool
    max : a -> a -> a
    min : a -> a -> a

sort : Ord a => List a -> List a

函数、接口和实现可拥有多个约束。多个约束的列表写在括号内，以逗号分隔，例如：

sortAndShow : (Ord a, Show a) => List a -> String
sortAndShow xs = show (sort xs)

注意：接口与 `mutual` 块¶

除 mutual 块外，Idris 严格遵循「先定义后使用」的规则。在 mutual 块中， Idris 会分两趟进行繁释（elaborate）：第一趟为类型，第二趟为定义。当互用块中包含接口声明时，第一趟会繁释接口的头部而不繁释方法类型；第二趟则繁释方法类型以及所有的默认定义。

函子与应用子¶

目前，我们已经见过形参类型为 Type 的单形参接口了。通常，形参的个数可为任意个（甚至零个），而形参也可为任意类型。若形参的类型不为 Type，我们则需要提供显式的类型声明。例如，Prelude 中定义的函子接口 Functor 为：

interface Functor (f : Type -> Type) where
    map : (m : a -> b) -> f a -> f b

函子允许函数应用到结构上，例如将一个函数应用到 List 的每一个元素上：

Functor List where
  map f []      = []
  map f (x::xs) = f x :: map f xs

Idris> map (*2) [1..10]
[2, 4, 6, 8, 10, 12, 14, 16, 18, 20] : List Integer

定义了 Functor 之后，我们就能定义应用子 Applicative 了，它对函数应用的概念进行了抽象：

infixl 2 <*>

interface Functor f => Applicative (f : Type -> Type) where
    pure  : a -> f a
    (<*>) : f (a -> b) -> f a -> f b

单子与 `do`-记法¶

单子接口 Monad 允许我们对绑定和计算进行封装，它也是「do」记法一节中 do-记法的基础。单子扩展了前面定义的 Applicative，其定义如下：

interface Applicative m => Monad (m : Type -> Type) where
    (>>=)  : m a -> (a -> m b) -> m b

在 do 块中会应用以下语法变换：

x <- v; e 变为 v >>= (\x => e)
v; e 变为 v >>= (\_ => e)
let x = v; e 变为 let x = v in e

IO 实现了 Monad，它使用原语函数定义。我们也可以为 Maybe 定义实现，其实现如下：

Monad Maybe where
    Nothing  >>= k = Nothing
    (Just x) >>= k = k x

通过它，我们可以定义一个将两个 Maybe Int 相加的函数，并用单子来封装错误处理：

m_add : Maybe Int -> Maybe Int -> Maybe Int
m_add x y = do x' <- x -- 从 x 中提取值
               y' <- y -- 从 y 中提取值
               pure (x' + y') -- 二者相加

若 x 和 y 均可用，该函数会从二者中提取出值；若其中一个或二者均不可用，则返回 Nothing （「fail-fast 速错原则」）。Nothing 的情况通过 >>= 操作符来管理，由 do-记法来隐藏。

*Interfaces> m_add (Just 20) (Just 22)
Just 42 : Maybe Int
*Interfaces> m_add (Just 20) Nothing
Nothing : Maybe Int

模式匹配绑定¶

有时我们需要立即对 do-记法中某个函数的结果进行模式匹配。例如，假设我们有一个函数 readNumber，它从控制台读取一个数，若该数有效则返回 Just x 形式的值，否则返回 Nothing ：

readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if all isDigit (unpack input)
     then pure (Just (cast input))
     else pure Nothing

如果接着用它来编写读取两个数，若二者均无效则返回 Nothing 的函数，那么我们可能想要对 readNumber 进行模式匹配：

readNumbers : IO (Maybe (Nat, Nat))
readNumbers =
  do x <- readNumber
     case x of
          Nothing => pure Nothing
          Just x_ok => do y <- readNumber
                          case y of
                               Nothing => pure Nothing
                               Just y_ok => pure (Just (x_ok, y_ok))

如果有很多错误需要处理，它的嵌套层次很快就会变得非常深！我们不妨将绑定和模式匹配组合成一行。例如，我们可以对 Just x_ok 的形式进行模式匹配：

readNumbers : IO (Maybe (Nat, Nat))
readNumbers =
  do Just x_ok <- readNumber
     Just y_ok <- readNumber
     pure (Just (x_ok, y_ok))

然而问题仍然存在，我们现在忽略了 Nothing 的情况，所以该函数不再是完全的了！我们可以把 Nothing 的情况添加回去：

readNumbers : IO (Maybe (Nat, Nat))
readNumbers =
  do Just x_ok <- readNumber | Nothing => pure Nothing
     Just y_ok <- readNumber | Nothing => pure Nothing
     pure (Just (x_ok, y_ok))

此版本的 readNumbers 效果与初版完全一样（实际上，它是初版的语法糖，并且会直接被翻译回初版的形式）。每条语句的第一部分（Just x_ok <- 和 Just y_ok <-）给出了首选的绑定：若能匹配，do 块的剩余部分就会继续执行。第二部分给出了候选的绑定，其中的绑定可以有不止一个。

`!`-记法¶

在很多情况下，do-记法会让程序不必要地啰嗦，在将值绑定一次就立即使用的情况下尤甚，例如前面的 m_add。此时我们可以使用更加简短的方式：

m_add : Maybe Int -> Maybe Int -> Maybe Int
m_add x y = pure (!x + !y)

!expr 记法表示 expr 应当在求值后立即被隐式绑定。从概念上讲，我们可以把 ! 看做拥有以下类型的前缀函数：

(!) : m a -> a

然而请注意，它并不是一个真的函数，而是一个语法！在实践中，子表达式 !expr 会在 expr 的当前作用域内尽可能地提升，将它绑定到一个全新的名字 x，然后用它来代替 !expr。首先表达式会按从左到右的顺序深度优先地上升。在实践中，! 记法允许我们以更直接的方式来编程，同时该记法也标出了哪些表达式为单子。

例如，表达式：

let y = 42 in f !(g !(print y) !x)

会被提升为：

let y = 42 in do y' <- print y
                 x' <- x
                 g' <- g y' x'
                 f g'

单子推导式¶

我们之间在更多表达式一节中看到的列表推导记法其实更通用，它可应用于任何实现了 Monad 和 Alternative 的东西：

interface Applicative f => Alternative (f : Type -> Type) where
    empty : f a
    (<|>) : f a -> f a -> f a

通常，推导式形式为 [ exp | qual1, qual2, …, qualn ] 其中 quali 可以为：

一个生成式 x <- e
一个 守卫式（Guard），它是一个类型为 Bool 的表达式
一个 let 绑定 let x = e

要翻译一个推导式 [exp | qual1, qual2, …, qualn]，首先任何作为 守卫式 的限定式 qual 会使用以下函数翻译为 guard qual：

guard : Alternative f => Bool -> f ()

接着该推导式会被转换为 do-记法：

do { qual1; qual2; ...; qualn; pure exp; }

使用单子推导式，m_add 的选取（alternative）定义为：

m_add : Maybe Int -> Maybe Int -> Maybe Int
m_add x y = [ x' + y' | x' <- x, y' <- y ]

习语括号¶

do-记法为串连提供了另一种写法，而习语则为应用提供了另一种写法。本节中的记法以及大量的例子受到了 Conor McBride 和 Ross Paterson 的论文「带作用的应用子编程」 [1] 的启发。

首先，让我们回顾一下前面的 m_add。它所做的只是将一个操作符应用到两个从 Maybe Int 中提取的值。我们可以抽象出该应用：

m_app : Maybe (a -> b) -> Maybe a -> Maybe b
m_app (Just f) (Just a) = Just (f a)
m_app _        _        = Nothing

我们可以用它来编写另一种 m_add，它使用了函数应用的选取概念，带有显式的 m_app 调用：

m_add' : Maybe Int -> Maybe Int -> Maybe Int
m_add' x y = m_app (m_app (Just (+)) x) y

与其到处插入 m_app，我们不如使用习语括号（Idiom Brackets）来做这件事。为此，我们可以像下面这样为 Maybe 提供一个 Applicative 的实现，其中 <*> 的定义方式与前面的 m_app 相同（它已在 Idris 库中定义）：

Applicative Maybe where
    pure = Just

    (Just f) <*> (Just a) = Just (f a)
    _        <*> _        = Nothing

按照 <*> 的实现，我们可以像下面这样使用它，其中函数应用 [| f a1 … an |] 会被翻译成 pure f <*> a1 <*> … <*> an：

m_add' : Maybe Int -> Maybe Int -> Maybe Int
m_add' x y = [| x + y |]

错误处理解释器¶

习语记法在定义求值器时通常很有用。McBride 和 Paterson 就为下面这样的语言描述了求值器 [1] ：

data Expr = Var String      -- 变量
          | Val Int         -- 值
          | Add Expr Expr   -- 加法

求值会被根据上下文将变量（表示为 String）映射为 Int 值，且可能会失败。我们定义了数据类型 Eval 来包装求值器：

data Eval : Type -> Type where
     MkEval : (List (String, Int) -> Maybe a) -> Eval a

将求值器包装在数据类型中意味着我们之后可以为它提供接口的实现。我们首先定义一个函数，它在求值过程中从上下文取出值。

fetch : String -> Eval Int
fetch x = MkEval (\e => fetchVal e) where
    fetchVal : List (String, Int) -> Maybe Int
    fetchVal [] = Nothing
    fetchVal ((v, val) :: xs) = if (x == v)
                                  then (Just val)
                                  else (fetchVal xs)

在定义该语言的求值器时，我们会应用 Eval 上下文中的函数，这样它自然会为 Eval 提供 Applicative 的实现。在 Eval 能够实现 Applicative 之前，我们必须为 Eval 实现 Functor：

Functor Eval where
    map f (MkEval g) = MkEval (\e => map f (g e))

Applicative Eval where
    pure x = MkEval (\e => Just x)

    (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
        app : Maybe (a -> b) -> Maybe a -> Maybe b
        app (Just fx) (Just gx) = Just (fx gx)
        app _         _         = Nothing

现在就可以在求值表达式时，通过应用的习语来处理错误了：

eval : Expr -> Eval Int
eval (Var x)   = fetch x
eval (Val x)   = [| x |]
eval (Add x y) = [| eval x + eval y |]

runEval : List (String, Int) -> Expr -> Maybe Int
runEval env e = case eval e of
    MkEval envFn => envFn env

命名实现¶

有时我们希望一个类型可以拥有一个接口的多个实现，例如为排序或打印提供另一种方法。为此，实现可以像下面这样命名：

[myord] Ord Nat where
   compare Z (S n)     = GT
   compare (S n) Z     = LT
   compare Z Z         = EQ
   compare (S x) (S y) = compare @{myord} x y

它像往常一样声明了一个实现，不过带有显式的名字 myord。语法 compare @{myord} 会为 compare 提供显式的实现，否则它会使用 Nat 的默认实现。我们可以用它来反向排序一个 Nat 列表。给定以下列表：

testList : List Nat
testList = [3,4,1]

我们可以在 Idris 提示符中用默认的 Ord 实现来排序，之后使用命名的实现 myord：

*named_impl> show (sort testList)
"[sO, sssO, ssssO]" : String
*named_impl> show (sort @{myord} testList)
"[ssssO, sssO, sO]" : String

有时，我们也需要访问命名的父级实现。例如 Prelude 中定义的半群 Semigroup 接口：

interface Semigroup ty where
  (<+>) : ty -> ty -> ty

接着又定义了幺半群 Monoid，它用「幺元」 neutral 扩展了 Semigroup：

interface Semigroup ty => Monoid ty where
  neutral : ty

我们可以为 Nat 定义 Semigroup 与 Monoid 的两种不同的实现，一个基于加法，一个基于乘法：

[PlusNatSemi] Semigroup Nat where
  (<+>) x y = x + y

[MultNatSemi] Semigroup Nat where
  (<+>) x y = x * y

加法的幺元为 0，而乘法的幺元为 1。因此，我们在定义 Monoid 的实现时，保证扩展了正确的 Semigroup 十分重要。我们可以通过 using 从句来做到这一点：

[PlusNatMonoid] Monoid Nat using PlusNatSemi where
  neutral = 0

[MultNatMonoid] Monoid Nat using MultNatSemi where
  neutral = 1

using PlusNatSemi 从句指明 PlusNatMonoid 应当扩展 PlusNatSemi。

确定形参¶

当接口的形参多于一个时，通过限定形参可帮助查找实现。例如：

interface Monad m => MonadState s (m : Type -> Type) | m where
  get : m s
  put : s -> m ()

在此接口中，查找该接口的实现只需要知道 m 即可，而 s 可根据实现来确定。它通过在接口声明之后添加 | m 来声明。我们将 m 称为 MonadState 接口的 确定形参（Determining Parameter） ，因为它是用于查找实现的形参。

[1]	(1, 2) Conor McBride and Ross Paterson. 2008. Applicative programming with effects. J. Funct. Program. 18, 1 (January 2008), 1-13. DOI=10.1017/S0956796807006326 http://dx.doi.org/10.1017/S0956796807006326

接口¶