Subtype

Subtype は、大雑把に言えば型 A : Type の部分集合を表します。すなわちある述語 p : A → Prop があったとき、Subtype p は A の項であって p という性質を満たすようなものの全体を表します。

-- 正の数を表す subtype
#check Subtype (fun n => n > 0)

{x : T // p x} という専用の構文が用意されていて、これで Subtype を表すことができます。

-- 正の数を表す subtype
#check { n : Nat // n > 0 }

実行時の性質

型 A の Subtype は実行時には A の項であるかのように振る舞います。言い換えれば、{ x : A // p x} の項は計算の実行時には A の項と同一視されます。これは、Subtype でラップしてもメモリアドレスが変わらないことから確認できます。

unsafe def checkSubtype : IO Unit := do
  let x : Nat := 42
  let pos : { n : Nat // n > 0} := ⟨x, by omega⟩
  if ptrAddrUnsafe x != ptrAddrUnsafe pos then
    throw <| .userError "メモリアドレスが異なります。"

#eval checkSubtype

用途

Subtype を使うと、ある型 A が U という型の一部を切り取ったものだということをコードで表現することができます。たとえば、自然数の型 Nat に対して、正の数だけを抜き出して正の整数の型 Pos を定義することを考えてみます。

このとき、Subtype を使わずに Pos を帰納型として以下のように定義することもできるのですが、こうすると Pos と Nat は実装上まったく無関係ということになってしまいます。

inductive Pos where
  | one
  | succ (n : Pos)

その結果、Nat に対するコンパイラ上の演算の最適化の恩恵を受けることができなくなり、たとえば足し算が非常に遅くなります。

namespace Inductive
  /- ## 別の帰納型として正の整数を定義する -/

  inductive Pos where
    | one
    | succ (n : Pos)

  def Pos.ofNat (n : Nat) : Pos :=
    match n with
    | 0 => Pos.one
    | 1 => Pos.one
    | n + 2 => Pos.succ (Pos.ofNat n)

  instance (n : Nat) : OfNat Pos (n + 1) where
    ofNat := Pos.ofNat n

  def Pos.add (m n : Pos) : Pos :=
    match n with
    | Pos.one => Pos.succ m
    | Pos.succ n' => Pos.succ (Pos.add m n')

  instance : Add Pos where
    add := Pos.add

end Inductive

namespace Subtype
  /- ## Subtype として正の整数を定義する -/

  def Pos := { n : Nat // n > 0 }

  def Pos.ofNat (n : Nat) : Pos :=
    ⟨n + 1, Nat.succ_pos n⟩

  instance (n : Nat) : OfNat Pos (n + 1) where
    ofNat := Pos.ofNat n

  def Pos.add (m n : Pos) : Pos :=
    ⟨m.val + n.val, by
      have mp := m.property
      have np := n.property
      omega
    ⟩

  instance : Add Pos where
    add := Pos.add

end Subtype

-- 帰納型として定義すると5倍以上も遅くなってしまう
#reduce (500 : Subtype.Pos) + (500 : Subtype.Pos)
#reduce (500 : Inductive.Pos) + (500 : Inductive.Pos)