接口

我们经常希望定义的函数能在几种不同的数据类型中工作。例如，我们希望算术运算符至少能在 Int, Integer 和 Double 上工作。我们希望 == 能在大多数数据类型上工作。我们希望能够以一种统一的方式显示不同的类型。

为了实现这一点，我们使用 接口 ，它类似于 Haskell 中的类型类或 Rust 中的 traits 。为了定义一个接口，我们提供一个可重载函数的集合。一个简单的例子是 Show 接口，它被定义在 prelude 中，提供了一个将数值转换为 String 的接口：

interface Show a where
    show : a -> String

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

show : Show a => a -> String

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

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

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

一个类型对于同一个接口只能有一种实现——实现不得重合。实现声明本身可以有约束。为了帮助解决这个问题，实现的参数必须是构造函数（数据或类型构造函数）或变量（也就是说，你无法为函数赋予实现）。例如，为向量定义一个 Show 的实现，我们需要知道有一个 Show 的实现用于元素类型，因为我们要用它把每个元素转换为 String ：

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

请注意，我们需要在 show' 函数中明确 forall n . ，因为 n 已经在作用域内，并且固定为顶层的 n 的值。

默认定义

Prelude 定义了一个 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

Ord 接口允许我们比较两个值并确定它们的顺序。只有 compare 方法是必需的；其他每个方法都有一个默认的定义。利用这一点，我们可以写一些函数，比如 sort ，这个函数可以将一个列表按递增顺序排序，前提是列表的元素类型在 Ord 接口中。我们在胖箭头 => 的左边给出类型变量的约束，在胖箭头的右边给出函数类型：

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

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

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

约束和类型一样，是语言中的一等对象。你可以在 REPL 中看到这一点：

Main> :t Ord
Prelude.Ord : Type -> Type

所以， (Ord a, Show a) 是一对普通的 Types ，将两个约束作为该对的第一个和第二个元素。

注：接口和 mutual 块

Idris是严格的 "先定义后使用"，除了在 mutual 块中。在 mutual 块中，Idris 分两遍进行扫描：第一遍是类型，第二遍是定义。当 mutual 块包含一个接口声明时，它在第一遍中扫描接口头，但没有方法类型，在第二遍扫描方法类型和所有的默认定义。

参数的量

默认情况下，在 interface 声明中没有明确赋予类型的参数被分配为数量 0 。这意味着该参数在运行时不能在方法的定义中使用。

例如， Show a 在 show 方法的类型中产生了一个数量为 0 的类型变量 a ：

Main> :set showimplicits
Main> :t show
Prelude.show : {0 a : Type} -> Show a => a -> String

然而有些用例要求一些参数在运行时可用。例如，我们可能想为 Storable 类型声明一个接口。约束 Storable a size 意味着我们可以将 a 类型的值存储在一个 Buffer 中，正好是 size 字节。

如果用户提供一个方法来在通过给定一个偏移量读取类型 a 的值，那么我们可以通过计算 k 和 size 的适当偏移量来读取存储在缓冲区中的 k 的元素。这可以通过为 peekElementOff 方法提供一个默认的实现来证明，该方法通过 peekByteOff 和参数 size 来实现。

data ForeignPtr : Type -> Type where
  MkFP : Buffer -> ForeignPtr a

interface Storable (0 a : Type) (size : Nat) | a where
  peekByteOff : HasIO io => ForeignPtr a -> Int -> io a

  peekElemOff : HasIO io => ForeignPtr a -> Int -> io a
  peekElemOff fp k = peekByteOff fp (k * cast size)

请注意， a 被明确标记为运行时不相关，所以它被编译器删除了。相当于我们可以写成 interface Storable a (size : Nat) 。 | a 的含义在 确定参数 中有解释。

函子与应用子

到目前为止，我们看到的都是单参数接口，其中参数的类型是 Type 。一般来说，可以有任何数量的参数（甚至是零个），而且参数可以有 任何 类型。如果参数的类型不是 Type ，我们需要给出一个明确的类型声明。例如， Functor 接口在 prelude 中是这样定义的：

interface Functor (0 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 (0 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

还有一个不进行绑定操作的运算符， Monad 将其定义为：

v >> e = v >>= \_ => e

在 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 -- Extract value from x
               y' <- y -- Extract value from y
               pure (x' + y') -- Add them

如果两个值都是有值的，这个函数将从 x 和 y 中提取数值，或者如果一个或两个都不是（"快速失败"），则返回 Nothing 。管理 Nothing 的情况是由 >>= 操作符实现的，被 do 符号所隐藏。

Main> m_add (Just 82) (Just 22)
Just 94
Main> m_add (Just 82) Nothing
Nothing

do 符号的翻译完全是句法性的，所以没有必要将 (>>=) 和 (>>) 操作符作为 Monad 接口中定义的操作符。一般来说，Idris 会尝试区分你所指的运算符的类型，但你可以用限定的 do 符号明确选择，例如：

m_add : Maybe Int -> Maybe Int -> Maybe Int
m_add x y = Prelude.do
               x' <- x -- Extract value from x
               y' <- y -- Extract value from y
               pure (x' + y') -- Add them

Prelude.do 意味着 Idris 将使用在 Prelude 中定义的 (>>=) 和 (>>) 。

模式匹配绑定

在 do 记法中，有时我们想在一个函数的结果上立即进行模式匹配，例如，假设我们有一个函数 readNumber 从控制台读取一个数字，如果该数字有效，则返回一个形式为 Just x 的值，否则为 Nothing ：

import Data.String

readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if all isDigit (unpack input)
     then pure (Just (stringToNatOrZ 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 的情况，所以 readNumbers 不再是完全函数！我们可以把 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 替换为 x 。表达式从左到右，从深度开始提升。在实践中， ! - notation 允许我们以更直接的方式进行编程，同时仍然提供一个符号线索，说明哪些表达式是单子。

例如，表达式：

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

被提升为：

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

单子推导式

我们在 更多表达式 一节中看到的列表推导式符号更为通用，它适用于任何实现了 Monad 和 Alternative 的数据类型：

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

一般来说，推导式的形式是： [ exp | qual1, qual2, …, qualn ] 其中 quali 可以是下列之一：

• 生成器 x <- e

• 一个 守卫 ，它是一个类型为 Bool 的表达式

• let 绑定 let x = e

翻译一个推导式 [exp | qual1, qual2, ..., qualn] ，首先使用以下函数将任何作为 guard 的限定符 qual 转换为 guard qual ：

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

然后将推导式转换为 do 记法：

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

使用单子推导式， m_add 的另一个定义是：

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

接口和IO

一般来说， IO 库中的操作不是直接使用 IO 编写的，而是通过 HasIO 接口编写的：

interface Monad io => HasIO io where
  liftIO : (1 _ : IO a) -> io a

HasIO 的解释，通过 liftIO 解释了如何将一个原语 IO 操作转换为某个底层类型的操作，只要该类型有一个 Monad 实现。 这些接口允许程序员定义一些更具表现力的交互式程序的概念，同时仍然可以直接访问 IO 原语。

习语括号

虽然 do 记法给序列另一种含义，但习语给了 应用子 另一种含义。本节中的符号和较大的例子是受 Conor McBride 和 Ross Paterson 的论文 "Applicative Programming with Effects " 的启发 [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 ，而是可以使用习语括号来为我们完成这项工作。要做到这一点，我们可以让 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      -- variables
          | Val Int         -- values
          | Add Expr Expr   -- addition

求值器将相对于上下文映射变量（表示为 Strings) 到 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

例如：

InterpE> runEval [("x", 10), ("y",84)] (Add (Var "x") (Var "y"))
Just 94
InterpE> runEval [("x", 10), ("y",84)] (Add (Var "x") (Var "z"))
Nothing

命名实现

对于同一类型的接口，可能需要有多个实现，例如，为排序或打印数值提供替代方法。为了实现这一点，实现可以被 命名 ，如下所示：

[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]

我们可以使用默认的 Ord 实现进行排序，通过使用 sort 函数， import Data.List 后可用，然后我们可以用命名的实现 myord 进行尝试，在 Idris 提示符下输入：

Main> show (sort testList)
"[1, 3, 4]"
Main> show (sort @{myord} testList)
"[4, 3, 1]"

有时，我们还需要访问一个命名的父级实现。例如，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 A a where
  getA : a

interface A t => B t where
  constructor MkB

  getB : t

然后 MkB : A t => t -> B t 。如果我们有

A Nat where
 getA = Z

getAB : (t : B a) => (a, a)
getAB = (getA, getB)

然后我们可以使用函数 getAB ，即使我们没有为 Nat 实现接口 B ，也可以通过内联传递一个实现

natAB = getAB { t = MkB (S Z) } -- === (Z, (S Z))

确定参数

当一个接口有一个以上的参数时，如果用来寻找实现的参数受到限制，就会有助于解决。比如说：

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

在这个接口中，只需要知道 m 就可以找到这个接口的实现，然后 s 可以从实现中确定。这是在接口声明之后用 | m 声明的。我们称 m 为 MonadState 接口的 决定性参数 ，因为它是用来寻找实现的参数。这类似于Haskell中 功能依赖 的概念* ` <https://wiki.haskell.org/Functional_dependencies>`_ 。

[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 https://dx.doi.org/10.1017/S0956796807006326