示例：良类型（Well-Typed）解释器

在本节中，我们将利用前面介绍的特性，编写一个更完整的示例：为一个简单的函数式编程语言实现解释器。该语言包含变量、函数应用、二元运算符以及 if...then...else 结构。我们将借助依值类型系统，确保所有可表示的程序都是良类型的。

语言的表示

首先，让我们定义该语言中的类型。我们有整数、布尔值和函数，这些都用 Ty 表示：

data Ty = TyInt | TyBool | TyFun Ty Ty

我们可以编写一个函数，将这些类型表示转换为具体的 Idris 类型——请记住，类型是一等公民，因此可以像其他值一样进行计算：

interpTy : Ty -> Type
interpTy TyInt       = Integer
interpTy TyBool      = Bool
interpTy (TyFun a t) = interpTy a -> interpTy t

我们将以一种只有良类型程序才能被表示的方式来定义我们的语言表示。我们会用表达式的类型以及局部变量的类型（上下文）来索引表达式的表示。上下文可以用 Vect 数据类型来表示，因此需要在源文件顶部导入 Data.Vect：

import Data.Vect

表达式由局部变量的类型和表达式本身的类型索引：

data Expr : Vect n Ty -> Ty -> Type

表达式的完整表示如下：

data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
    Stop : HasType FZ (t :: ctxt) t
    Pop  : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t

data Expr : Vect n Ty -> Ty -> Type where
    Var : HasType i ctxt t -> Expr ctxt t
    Val : (x : Integer) -> Expr ctxt TyInt
    Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)
    App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t
    Op  : (interpTy a -> interpTy b -> interpTy c) ->
          Expr ctxt a -> Expr ctxt b -> Expr ctxt c
    If  : Expr ctxt TyBool ->
          Lazy (Expr ctxt a) ->
          Lazy (Expr ctxt a) -> Expr ctxt a

上面的代码用到了 base 库中的 Vect 和 Fin 类型。Fin 可通过 Data.Vect 获得。全文中，ctxt 指的是局部变量上下文。

由于表达式是按其类型索引的，我们可以从构造函数的定义中直接读出该语言的类型规则。下面我们依次看看每个构造函数。

我们采用无名表示法（nameless representation）来表示变量——即 de Bruijn 索引。变量由其在上下文中的归属证明 HasType i ctxt T 表示，这表明在上下文 ctxt 中，变量 i 的类型为 T。定义如下：

data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
    Stop : HasType FZ (t :: ctxt) t
    Pop  : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t

我们可以将 Stop 视为对最近定义变量良类型的证明，而 Pop n 则证明如果第 n 个最近定义的变量是良类型的，那么第 n+1 个也是良类型的。实际上，这意味着我们用 Stop 表示最近定义的变量，用 Pop Stop 表示下一个，以此类推，通过 Var 构造函数实现：

Var : HasType i ctxt t -> Expr ctxt t

因此，在表达式 \x. \y. x y 中，变量 x 的 de Bruijn 索引为 1，用 Pop Stop 表示，变量 y 的索引为 0，用 Stop 表示。我们通过计算定义与使用之间的 lambda 数量来确定这些索引。

值（Value）携带一个整数的具体表示：

Val : (x : Integer) -> Expr ctxt TyInt

lambda（λ）表达式用于创建函数。在类型为 a -> t 的函数作用域内，会有一个类型为 a 的新局部变量，这通过上下文索引来表达：

Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)

函数应用：给定一个从 a 到 t 的函数和一个类型为 a 的值，将产生一个类型为 t 的值：

App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t

我们允许任意二元运算符，其类型决定了参数的类型要求：

Op : (interpTy a -> interpTy b -> interpTy c) ->
     Expr ctxt a -> Expr ctxt b -> Expr ctxt c

最后，If 表达式根据布尔值进行分支选择。每个分支必须具有相同的类型，并且我们会对分支进行惰性求值，只计算实际被选中的分支：

If : Expr ctxt TyBool ->
     Lazy (Expr ctxt a) ->
     Lazy (Expr ctxt a) ->
     Expr ctxt a

编写解释器

在对 Expr 进行求值时，我们需要知道当前作用域中的值及其类型。Env 是一个环境（environment），按当前作用域中的类型进行索引。环境本质上是列表的一种形式，但与局部变量类型向量有严格的对应关系。我们仍然使用常规的 :: 和 Nil 构造函数，以便可以使用常见的列表语法。只要有变量在上下文中已定义的证明，我们就能从环境中取出对应的值：

data Env : Vect n Ty -> Type where
    Nil  : Env Nil
    (::) : interpTy a -> Env ctxt -> Env (a :: ctxt)

lookup : HasType i ctxt t -> Env ctxt -> interpTy t
lookup Stop    (x :: xs) = x
lookup (Pop k) (x :: xs) = lookup k xs

基于上述定义，解释器就是一个函数，它将 Expr 按照特定环境（environment）翻译为具体的 Idris 值：

interp : Env ctxt -> Expr ctxt t -> interpTy t

完整的解释器定义如下，供参考。对于每个构造函数，我们都将其翻译为对应的 Idris 值：

interp env (Var i)     = lookup i env
interp env (Val x)     = x
interp env (Lam sc)    = \x => interp (x :: env) sc
interp env (App f s)   = interp env f (interp env s)
interp env (Op op x y) = op (interp env x) (interp env y)
interp env (If x t e)  = if interp env x then interp env t
                                         else interp env e

我们依次来看每种情况。对于变量，只需在环境中查找即可：

interp env (Var i) = lookup i env

对于值（Value），直接返回其具体表示即可：

interp env (Val x) = x

lambda（λ）表达式更有趣。在这种情况下，我们构造一个函数，该函数在环境中引入一个新值来解释 lambda 的作用域。因此，对象语言中的函数会被翻译为 Idris 函数：

interp env (Lam sc) = \x => interp (x :: env) sc

对于函数应用（application），我们分别对函数和参数进行解释，然后直接应用。由于类型信息，我们知道解释 f 必然得到一个函数：

interp env (App f s) = interp env f (interp env s)

运算符和条件表达式同样可以直接翻译为等价的 Idris 结构。对于运算符，直接将函数应用于操作数；对于 If，直接使用 Idris 的 if...then...else 结构。

interp env (Op op x y) = op (interp env x) (interp env y)
interp env (If x t e)  = if interp env x then interp env t
                                         else interp env e

测试

我们可以编写一些简单的测试函数。首先，两个输入相加 \x. \y. y + x 可以这样写：

add : Expr ctxt (TyFun TyInt (TyFun TyInt TyInt))
add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))

更有趣的是，阶乘函数 fact``（例如 ``\x. if (x == 0) then 1 else (fact (x-1) * x)）可以这样写：

fact : Expr ctxt (TyFun TyInt TyInt)
fact = Lam (If (Op (==) (Var Stop) (Val 0))
               (Val 1)
               (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
                       (Var Stop)))

运行

最后，我们编写一个 main 程序，用于对用户输入执行阶乘函数的解释：

main : IO ()
main = do putStr "Enter a number: "
          x <- getLine
          printLn (interp [] fact (cast x))

这里，cast 是一个重载函数（overloaded function），用于在可能的情况下将一个值从一种类型转换为另一种类型。在本例中，它将字符串转换为整数，如果输入无效则返回 0。以下是在 Idris 交互环境中运行该程序的示例：

$ idris2 interp.idr
     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.7.0
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main> :exec main
Enter a number: 6
720

补充说明：`cast`

Prelude（预定义库）中定义了一个接口 Cast，用于在类型之间进行转换：

interface Cast from to where
    cast : from -> to

它是一个*多参*接口（multi-parameter interface），定义了转换的源类型和目标类型。类型检查器在应用转换时必须能够推断出*两个*参数。只要有意义，所有原始类型之间都定义了转换。

示例：良类型（Well-Typed）解释器

语言的表示

编写解释器

测试

运行

补充说明：cast

补充说明：`cast`