示例用法

git clone https://github.com/maiavictor/formality
cd examples

# Interpreter evaluation
formality everything.formality.hs -e not_true 

# SIC evaluation
formality everything.formality.hs -s -f not_true 

# Type-checking
formality everything.formality.hs -t add
formality everything.formality.hs -t add-comm

形式语言非常简单。其程序由两个构建块组成：归纳数据类型，用于表示数据格式；以及函数，用于表示对这些类型数据的计算。这就是你需要的一切。

最简单的类型之一，布尔类型，可以声明为

data Bool : Type
| true    : Bool
| false   : Bool

否定函数可以声明为

let not(b : Bool) =>
    case b  -> Bool
    | true  => Bool.false
    | false => Bool.true

当我们想要检查数据类型的值时，都会使用模式匹配。

最简单的递归类型之一，自然数，可以声明为

data Nat : Type
| succ   : (n : Nat) -> Nat
| zero   : Nat

一个将其翻倍的功能可以写成

let double(a : Nat) =>
    case a       -> Nat
    | succ(pred) => Nat.succ(Nat.succ(fold(pred)))
    | zero       => Nat.zero

由于形式语言是全总性的，递归是通过使用fold关键字来执行的，这个关键字在模式匹配的case中可用。它允许我们将相同的逻辑递归地应用到结构上更小的值。

类型可以轻松地参数化

data Pair<A : Type, B : Type> : Type
| new : (x : A, y : B) -> Pair

声明多态函数就像将类型作为参数一样简单

let fst(A : Type, B : Type, pair : Pair<A, B>) =>
    case pair   -> A
    | new(x, y) => x

这允许你为多个具体类型重用同一个函数的实现，这是一个强大而古老的技巧，某些“现代系统语言”竟然无法正确实现。

形式语言允许类型不仅由其他静态类型参数化，还可以由运行时值参数化：我们称之为“索引”。经典的Vector类型，其长度在编译时是符号已知的，可以声明为

data Vect<A : Type> : (n : Nat) -> Type
| cons : (n : Nat, x : A, xs : Vect(n)) -> Vect(Nat.succ(n))
| nil  : Vect(Nat.zero)

当我们对那些类型进行模式匹配时，我们可以指定一个依赖于索引的返回类型

let tail(A : Type, n : Nat, vect : Vect<A>(Nat.succ(n))) =>
    case vect        -> (n) => Vect<A>(pred(n))
    | cons(n, x, xs) => xs
    | nil            => Vect<A>.nil

这允许我们编写强大的类型安全函数，例如一个不能溢出的向量的索引函数。我们还可以使用self关键字来引用匹配的结构本身，允许我们表达数学归纳（见示例）。

这些功能允许形式语言将定理表达为类型。例如，数学上的等价可以定义为

data Eq<A : Type> : (x : A, y : A) -> Type
| refl : (x : A) -> Eq(x, x)

而证明a == b意味着b == a的证明只是

let sym(A : Type, a : A, b : A, e : Eq<A>(a, b)) =>
    case e    -> (a, b) => Eq<A>(b, a)
    | refl(x) => Eq<A>.refl(x)

有了这么高的表现力，形式语言类型可以被视为“规范语言”。例如，我们可以写出“排序列表的类型”、“大于10的质数的类型”，甚至“不能被耗尽的智能合约的类型”。

以下形式语言程序

id(1000000000(List<Bool>, map(Bool, Bool, not), list))