依存タプルを処理する関数の例

現在、おそらく最も強力な型システムを持つと思われるLean 4によるコード。型ファミリーや依存タプルを含む型を定義して、型チェックは型システムに任せる。プログラマは、データの整合性をチェックするようなコードは書かない。処理のみを書く。

/-- 既婚かどうかのフラグにより変化する型の定義
既婚の場合は配偶者の名前である文字列型
未婚なら特に値はない（空集合ではなくて、Void = Unit 型）
-/
def Partner (married : Bool) : Type := 
  match married with
  | true => String -- married = true なら文字列型
  | false => Unit -- married = false ならUnit型

/-- アンケートデータを引数にもらって処理する関数
name : 本人の名前
married : 既婚かどうか
partner : 配偶者の名前（ただし、既婚の場合だけ）
-/
def processEnqueteData
  (name : String) -- 本人の名前
  (married : Bool) -- 既婚かどうか
  (partner : Partner married) -- 配偶者の名前（ただし、既婚の場合だけ）
  : String -- 戻り値の型
:=
  -- 既婚なら、本人の名前と配偶者の名前を " and " を挟んでつなぐ
  -- 未婚なら、本人の名前のみ
  match married with
  | true => .append (.append name " and ") partner
  | false => name

型定義と関数定義の区別がないことに注意。型も「Type型の値」とみなすので、型定義も「型という値を計算する関数」となる。$`|{\bf Set}|`$ もサイズがでかいけど集合に違いはない、と考えるのと同じ。

宇宙階層は型システムに正式に組み込まれている（「火の鳥」の世界観が実装されている）。宇宙に関する多相は universe polymorphism と呼ぶ。例えば、どの宇宙でも動作する関数は宇宙多相関数〈universe polymorphic function〉という。