宇宙と帰納的集合と部分的定義

Idris 2で次のコードを書けるようだ。

def typeDesc (ty : Type) : String :=
 match ty  with
 | Int => "integer"
 | String => "string"
 | List α => "list of " ++ typeDesc α
 | _ => "something else"

Leanでは無理だ。パターンマッチ match/withが帰納的集合の上でしか使えない。型宇宙Typeは帰納的に作られてない。もうひとつ、List α => "list of " ++ typeDesc α のように、いきなり出現する型変数もうまくない。

Idres 2 の場合、パターンマッチング場合分けというより、部分的に関数を定義していくことが許される。Lean構文ではないがLean風に書くと：

decl typeDesc (ty : Type) : String
typeDesc Int := "integer"
typeDesc String := "string"
typeDesc {α: Type} List α := "list of " ++ typeDesc α
typeDesc _ := "something else"

これだと、定義がいつ閉じるか（確定するか）は不明になる。型クラス・インスタンスの定義がこの方式になる。

宇宙も帰納的集合だという仮定もありえる。Idrisは帰納的宇宙を想定しているのかも知れない。