Impredicative Typesについてのメモ
最近なかなかブログを更新できずにいて、気持ちとしては
しかしブログは「シリーズ物の記事」と考えて書こうとすると、シリーズ最後あたりは本当に書くのがつらくなるな
— zehnpaard (@zehnpaard) February 21, 2022
で少し自分の首を絞めている感覚がある。
初心に帰りもう少し肩の力を抜いて、調べ物についての備忘録のような記事も書いていきたい。
というわけで最近Types and Programming Languagesやその続編であるAdvanced Topics in Types and Programming Languagesを読んでいるので、気になったトピックについて拾っていく。まずはImpredicative Types。
この単語はMLやHaskellについて読んでいるとたまに見かけて、そもそも単語の意味からして全くわからないのでちょっと怖い印象を受けていた。TaPLの23.10章がImpredicativityだったのでそこをあたった。
Impredicative Typesとは何か
In general, a definition (of a set, a type, etc) is called "impredicative" if it involves a quantifier whose domain includes the very thing being defined.
TaPLでのImpredicative Typesの話題は23章の全称型、System Fについての話の流れで出てくる。
全称型というのは∀X. X→Xや∀X. X list→intのような「どんな型でも入る型変数Xを含んだ型」のこと。
∀X. X→Xはlet id x = x、∀X. X list→intはlet rec len = function [] -> 0 | _::xs -> 1 + len xsのような値の型になる。
Impredicativeというのはこの∀X. X→Xに出てくる型変数Xに当てはめられる型に何の制限もなく、特に∀X. X→Xそれ自体を当て嵌めても問題ない、というような型システムを指す用語。そうすると(∀X. X→X)→(∀X. X→X)のような関数の型が可能になる。
→の左辺に全称型が入る＝関数の引数の型が全称型である、というのは強い制約で「例えばInt->IntやBool->Boolな関数が入る」のではなく「多相的な関数しか引数として受け付けない」という意味である。
「型変数Xに当てはめられる型に何の制約もない」ということは(∀X. X→X)→(∀X. X→X)の左辺の∀Xに(∀X. X→X)を当てはめて((∀X. X→X)→(∀X. X→X))→(∀X. X→X)にもできる、ということだ。
関数型の左辺にどれくらいネストした全称型を許容するか、によって型システムはランクN多相に分類できる：
ランク1多相 ∀X. X→X
ランク2多相 (∀X. X→X)→(∀X. X→X)
ランク3多相 ((∀X. X→X)→(∀X. X→X))→(∀X. X→X)
ちなみに右辺に全称型が出る場合、Int→(∀X. X→X)はランク1、Int→(∀X. X→X)→(∀X. X→X)はランク2である。制約が全くない、つまりランクが無限なものがSystem Fであり、Impredicativeな型システムである。
ML系言語で有名なHindley Milner Type Inferenceのある型システムは基本的にランク1のlet多相。ランク2までは型推論が決定可能、ランク3以降は決定不能ということが証明されている。
名前の由来
なんでImpredicativeという名前がついているのか。TaPLによるとPredicativeの否定形で、集合論からきてラッセルのパラドックスと関連している、とのこと。Predicateとは集合を定義し得るものなので、定義した対象自体について適用はされ得ないものがPredicative。その対義語として「自身を含み得る定義」としてImpredicativeという単語が存在する、らしい。
追記：
そういえば二年ほど前にSPJがこんな発表をしていた。あの頃は「何のこっちゃ」だったが今なら少しわかるだろうか？
