# 接口¶

```interface Show a where
show : a -> String
```

```show : Show a => a -> String
```

```Show Nat where
show Z = "Z"
show (S k) = "s" ++ show k
```
```Idris> show (S (S (S Z)))
"sssZ" : 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
```

## 默认定义¶

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

```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` 的最小完整实现只需要定义 `==``/=` 二者之一，而不需要二者都定义。 若缺少某个方法定义，且存在它的默认定义，那么就会使用该默认定义。

## 扩展接口¶

```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）：第一趟为类型，第二趟为定义。当互用块中包含接口声明时， 第一趟会繁释接口的头部而不繁释方法类型；第二趟则繁释方法类型以及所有的默认定义。

## 函子与应用子¶

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

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

```infixl 2 <*>

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

## 单子与 `do`-记法¶

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

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

### 模式匹配绑定¶

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

```readNumbers : IO (Maybe (Nat, Nat))
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))
```

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

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

### `!`-记法¶

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

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

```(!) : m a -> a
```

```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'
```

### 单子推导式¶

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

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

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

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

```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_app : Maybe (a -> b) -> Maybe a -> Maybe b
m_app (Just f) (Just a) = Just (f a)
m_app _        _        = Nothing
```

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

```Applicative Maybe where
pure = Just

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

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

### 错误处理解释器¶

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

```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)
```

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

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

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

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

```interface Semigroup ty => Monoid ty where
neutral : ty
```

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

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

```[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 ()
```

 [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