型別論

Cella 的核心是 Cubical 型別論（CCHM）。在它之上，同一個語言還有用量（QTT）、模態（MTT）、定義上的證明無關（SProp） 與使用者宣告的改寫規則。用它們不必換語言：每一種都只是幾個關鍵字，一條定義的 mode 決定它能用哪些。

這一頁的每個範例，網站建置時都由 Cella 檢查過。

一覽

型別論	給你什麼	怎麼寫	誰檢查
Cubical（CCHM）	路徑是區間上的函式、函式外延性、univalence、高階歸納型別	Path a b、fun i => ...、transport、ua、data ... = ... | c : Path a b	兩個 kernel
高階歸納型別（HIT）	有路徑建構子的型別：圓、懸垂、截斷、球面、環面、pushout、join	型別是路徑的建構子	兩個 kernel
用量（QTT）	抹除（0）與線性（1）的參數；自訂用量的 semiring	(0 x : A)、(1 x : A)、grades G := {...}	兩個 kernel
模態（MTT）	模態型別與鎖，模態與它們之間的定律都可以自己宣告	modality mu : m -> n、mu.Type A、(@mu x : A)、law	兩個 kernel
SProp	所有證明在定義上都相等的命題	data P : SProp = ...	兩個 kernel
改寫規則	替公設的常數加上計算規則	postulate、rule	兩個 kernel
mode	一條定義能用上面的哪些	@[mode core]、mode X extends ... grades ...	兩個 kernel（runtime 那一軸由 elaborator）

「兩個 kernel」是說同一條規則檢查兩次：一次由 kernel，一次由照同一份型別規則從零寫的獨立檢查器；兩邊都同意，定義才被接受。

Cubical 型別論

路徑 Path a b（Unicode 寫 a ≡ b，意思相同）是從區間到型別的函式，兩端固定。用 fun i => ... 寫出來， 套用在一個點 i 上使用；1 - i 把它反過來。

import std

def symm {A : Type} {a : A} {b : A} (p : Path a b) : Path b a := fun i => p (1 - i)

def ap {A : Type} {B : Type} (f : A -> B) {x : A} {y : A} (p : Path x y) : Path (f x) (f y) := fun i => f (p i)

def funext {A : Type} {B : Type} {f : A -> B} {g : A -> B} (h : (x : A) -> Path (f x) (g x)) : Path f g :=
  fun i => fun x => h x i

funext 只有一行，因為路徑就是函式：函式外延性在這裡不是公理，而且會計算。

Univalence。 ua 把型別之間的等價變成它們之間的路徑，沿著它 transport 就是套用那個等價。標準庫的 notEquiv 是由 not 給出的 Bool -> Bool 等價：

import std
import equiv

def flipped : Path (transport (ua notEquiv) true) false := refl

refl 就夠了：transport 算出來就是 not true。其他原語（transp、hcomp、Glue、unglue）也都有；import foundations、 path、equiv 在它們上面建好常用的函式庫。

兩種相等。 a = b 是歸納定義的相等（Eq，只用 data 與 match、不用 cubical 的原語），不需要 cubical 的 mode；Path a b 是 cubical 的路徑。refl 兩種都能證，Eq.toPath 與 Path.toEq（import identity.paths）互相轉換。

高階歸納型別

型別是路徑的建構子叫路徑建構子。對這種型別做 match 要寫它的分支，而這個分支必須是「兩端的像之間」的路徑；Cella 會檢查。

import std

data Circle = base | loop : Path base base

data Susp (A : Type) = north | south | merid (a : A) : Path north south

def flip {A : Type} (x : Susp A) : Susp A := match x with
  | north => south
  | south => north
  | merid a => fun i => merid a (1 - i)

def toCircle (x : Susp Bool) : Circle := match x with
  | north => base
  | south => base
  | merid b => (match b with
    | true => fun i => loop i
    | false => fun i => base)

flip 把 north 送到 south，所以經線要反過來。如果寫成 merid a => fun i => merid a i，會被拒絕，錯誤標在那個分支： 路徑的起點是 north，型別要的是 south。

路徑建構子可以有參數（merid (a : A)），也可以是路徑之間的路徑（2 維球面的 surf : Path (refl : Path base2 base2) (refl : Path base2 base2)）。 標準庫的 hits 模組有圓、懸垂、命題截斷、區間、環面、2 維球面、pushout 與 join，以及它們的消去子；winding 經由萬有覆蓋 （用 ua 建的）算出圓上一個迴圈的繞數：

import std
import int
import hits
import winding

def once : Path (winding loop) (pos 1) := refl
def twice : Path (winding (trans loop loop)) (pos 2) := refl

用量（QTT）

參數可以寫明能用幾次：0（抹除：只出現在型別裡，執行時不存在）、1（恰好一次），或不寫（任意次）。

import std

def length {A : Type} (0 n : Nat) (xs : List A) : Nat := List.length xs

def keep (1 x : Nat) : Nat := x

def twice (1 x : Nat) : Nat := add x x 會被拒絕：線性的 x 被交給 add 一個可以任意使用的參數。抹除的參數可以用在型別與 其他抹除的位置，不能在執行時當成值用。抹除不等於無關：抹除的引數照樣會被比較（data Box (0 A : Type) = box A 時， Box Nat 與 Box Empty 仍是不同的型別）。要「所有證明都相等」，用下面的 SProp。

自訂的 semiring。 除了 0、1、omega（任意次；Unicode 寫 ω），用量也可以來自你定義的有限 semiring：一個元素的型別，加上它的 add、mul 與順序， 用 grades G := { zero := ..., one := ..., add := ..., mul := ..., le := ..., true := ..., omega := ... } 宣告。Cella 以計算檢查 semiring 的 定律，再依它檢查每一次使用（經過函式呼叫與遞迴定義也算）。mode 決定它的定義能寫哪些用量：

import std

mode erasing extends core grades {0, omega}

@[mode erasing] def second (0 x : Bool) (y : Bool) : Bool := y

模態（MTT）

模態 mu : m -> n 從 mode m 到 mode n。mu.Type A 是模態型別，mu.mk a 把值放到模態底下（在鎖 mu 下檢查 a）， 參數 (@mu x : A) 帶著這個模態。

data B = tt | ff

modality secret : core -> core

def hide : secret.Type B := secret.mk tt

def keep (@secret b : B) : secret.Type B := secret.mk b

在鎖底下，不能用外面沒帶這個模態的變數：模態就是這樣控制什麼能流到哪裡。law mu nu = rho 說鎖怎麼合成， law mu => nu 讓帶 mu 的變數可以在 nu 底下使用；定律必須合流，宣告時由 Cella 檢查。做法依 Gratzer、Kavvos、Nuyts、 Birkedal 的 MTT；完整的語法見語言參考。

SProp：定義上的證明無關

宣告在 SProp 的型別是命題，它的證明在定義上全部相等，所以沒有東西會依賴「你拿的是哪一個證明」：

data STrue : SProp = sI
data SEmpty : SProp =

def irr (P : SProp) (F : P -> Type) (p : P) (q : P) (x : F p) : F q := x

def absurd (A : Type) (e : SEmpty) : A := match e with

irr 不需要 p 與 q 相等的證明。SProp 裡的證明拆開來只能做出另一個證明（空型別例外：它可以消去成任何型別）；SProp 的型別 沒有路徑建構子，而且 SProp 是直謂的。這是 Gilbert、Cockx、Sozeau、Tabareau（POPL 2019）的系統，和 Agda 的 --prop 相同。

改寫規則

postulate 引入沒有定義的常數；rule 給它一條計算規則，之後兩個 kernel 都照它計算：

data N = z | s N

postulate p : N -> N

rule pOfS (n : N) : Path (p (s n)) z

def t : Path (p (s (s z))) z := refl

規則的左邊是樣式；重疊的規則必須一致，依賴公設的定義會在判決裡說出來。

mode

mode 是一組特性。core 沒有上面任何一種，cubical 加上路徑與高階歸納型別，runtime 加上 IO 與外部呼叫； mode X extends ... 宣告你自己的 mode，連同它允許的用量。宣告在某個 mode 的定義，只能用那個 mode 允許的東西， 直接用或經由它依賴的任何定義都算。

data B = tt | ff

@[mode core] def neg (b : B) : B := match b with
  | tt => ff
  | ff => tt

@[mode cubical] def same (b : B) : Path b b := fun i => b

把 same 宣告在 core 會被拒絕：它用了路徑，需要 cubical。沒有宣告 mode 的定義不受限制。mode 之間只有包含關係 （core 在 cubical 裡、也在 runtime 裡），所以用多少付多少；core 裡的證明，對沒有 cubical 機制的檢查器也照樣有效。

語言裡還有

• 餘歸納型別（codata）：受保護的遞迴與生產性檢查。
• 宇宙層級（Type l）與累積性；用 sized type 證明終止。
• 完整的規則（每一條都附必須接受與必須拒絕的例子）在兩個 kernel 所依據的型別規則裡。