型システムの表記はどう読めばよいのか？

 (langdev.stackexchange.com)
1 ポイント 投稿者 GN⁺ 2023-08-17 | 1件のコメント | WhatsAppで共有
  • 型システムの表記は資料ごとに異なっていても、文法、型付け関係、推論規則という共通の枠組みを理解すれば、たいていの変種を追うことができる
  • 型システムは言語の抽象構文の上で動作するため、まず型を持つ項(term)と型そのものを文法として区別する必要がある
  • ⊢ e: τ は「式 e は型 τ を持つ」という型付け判断であり、横線の上の条件がすべて真なら下の結論も真である推論規則として読む
  • 変数と関数が入ると Γ ⊢ e: τ のようにコンテキストが付き、現在のスコープ内の変数名と型を追跡する
  • 多くの型付け規則は再帰的な型検査関数のように読めるが、すべての論理的判断がそのまま決定可能な型検査アルゴリズムになるわけではない

文法から始める型システム表記

  • 型システムはプログラミング言語の構文的システムであり、言語の抽象構文に対して動作する規則の集合である
  • 包括的な型システムの説明では、通常まず扱う構文構造を文法で示し、それをBNF表記で表す
  • 最も単純な型付き言語でも、構文は大きく二つの範疇に分かれる
    • e: 型を持つ式(expression)
    • τ: 式に付く型(type)
  • 例の言語では、ブールリテラル、整数リテラル、条件式、算術演算、比較演算を式として持ち、Bool と Int を型として使う
  • 型記号は資料によって τ の代わりに t、T、σ、あるいは他の小文字ギリシャ文字が使われることもあるが、全体の構造は似ている
  • より複雑な言語では、文、パターンマッチのパターンのような、さらに多くの構文範疇を含むことがある

型付け関係と判断の読み方

  • 文法を定めたあとは、通常 e : τ という形の型付け関係を定義する
    • 1 + 2 : Int は「1 + 2 は Int 型」という意味である
    • 1 + 2 : Bool は同じ式が Bool 型だという意味になり、正しくない
    • true + 2 : Int は式そのものが成立しておらず、どの型も持たない
  • ⊢ e : τ は型付け判断であり、⊢ は「後ろの文が真である」と読める
  • 横線の上に何もない規則は、常に真である公理(axiom) である
    • ⊢ true : Bool
    • ⊢ false : Bool
    • ⊢ 0 : Int, ⊢ 1 : Int, ⊢ -1 : Int のような整数リテラルの規則
  • 横線の上と下の両方がある規則は推論規則である
    • 上の条件がすべて真なら、下の結論が真である
    • e₁ と e₂ がどちらも Int なら e₁ + e₂ は Int
    • e₁ と e₂ がどちらも Int なら e₁ < e₂ は Bool

条件式と型変数

  • if ... then ... else ... の二つの分岐はどんな型でもよいが、互いに同じ型でなければならない
    • if true then 1 else 2 は可能である
    • if true then false else true も可能である
    • if true then 1 else true は不可能である
  • これを表現するために、規則では分岐の型を表す変数 τ を使う
    • 条件式 e₁ は Bool でなければならない
    • then 分岐 e₂ と else 分岐 e₃ は同じ τ 型でなければならない
    • 条件式全体の型も τ になる
  • 規則を適用するときは、どんな型でも τ として選べるが、同じ規則の中ではその選択を一貫して保つ必要がある

推論規則をアルゴリズムのように読む

  • この表記法は形式論理に由来し、型システムの記述方法は特に自然演繹に似ている
  • このような規則はシステムの性質についての形式的証明を組み立てる際に使われ、型安全性のような性質を証明するうえで重要である
  • 論理的判断が常にそのまま決定可能な型検査アルゴリズムに対応するわけではない
  • 多くの場合 ⊢ e : τ は、式 e から型 τ を得る関数のように読むことができる
    • 文法の各式の形ごとに、通常ひとつの規則がある
    • 各型付け規則は、再帰的な型検査関数のひとつの分岐として見なせる
  • 例の infer 関数は次の流れに対応する
    • true または false は Bool
    • 整数リテラルは Int
    • e₁ + e₂ は両方の推論結果がともに Int か確認したうえで Int
    • e₁ < e₂ は両方がともに Int か確認したうえで Bool
    • if e₁ then e₂ else e₃ は条件が Bool か確認し、二つの分岐の型が同じか確認したうえでその型を返す
  • 直接アルゴリズムに落とし込めなくても、判断において e を入力、τ を出力のように考えると、情報の流れを理解しやすい

変数とコンテキスト

  • 実用的なプログラミング言語を扱うには変数が必要であり、例では関数を追加して simply typed lambda calculus の形に拡張する
  • 拡張された文法には次が含まれる
    • 変数 x
    • 関数抽象 λx:τ. e
    • 関数適用 e e
    • 関数型 τ → τ
  • λx:τ. e は TypeScript の (x:τ) => e に対応し、f x は f(x) に対応する
  • 変数の型は、その変数が現れるコンテキストに依存するため、単純な ⊢ x : ??? という形では規則を書けない
  • そのため、型付け判断は Γ ⊢ e : τ に拡張される
    • Γ はコンテキストまたは型環境である
    • ⊢ は左側の文脈上の仮定と、右側の証明すべき文を区切る
    • 「コンテキスト Γ のもとで、式 e は型 τ を持つ」と読む
  • アルゴリズム的には、Γ は Map<Variable, Type> の形をした追加の入力のように見なせる
  • 形式的には、コンテキストも構文構造として明示される
    • ∅: 空コンテキスト
    • Γ, x:τ: 変数束縛を追加したコンテキスト
    • ときには ∅ の代わりに • が空コンテキストとして使われる
  • この表現では、コンテキストは変数名を型に対応付ける association list に近い

コンテキストが規則の中で果たす役割

  • 多くの型付け規則は、コンテキストを変更せずそのまま受け渡す
    • Γ ⊢ true : Bool
    • Γ ⊢ e₁ : Int と Γ ⊢ e₂ : Int なら Γ ⊢ e₁ + e₂ : Int
  • 変数の使用とラムダ式の規則では、コンテキストが中心的な役割を果たす
    • x:τ ∈ Γ なら Γ ⊢ x : τ
    • Γ, x:τ₁ ⊢ e : τ₂ なら Γ ⊢ (λx:τ₁. e) : τ₁ → τ₂
  • ラムダ式の本体 e を型検査するとき、コンテキストは新しい束縛 x:τ₁ で拡張される
  • 変数規則は、現在のコンテキストに変数束縛があれば、その変数はその型を持つと判断する
  • コンテキストは、ラムダ式の規則と変数規則のあいだで情報を受け渡す通信メカニズムとして使われる
  • 単純化のため、この種の型システム記述では通常、すべての変数がすでに解決され一意になっていると仮定し、変数シャドーイングは扱わない
  • 関数適用規則では、関数式と引数式の型をあわせて確認する
    • e₁ は τ₁ → τ₂ 型でなければならない
    • e₂ は τ₁ 型でなければならない
    • 式全体の適用 e₁ e₂ の型は τ₂ になる

よく出てくる追加表記

  • 推論規則は、常に縦方向だけで書かれるとは限らない
    • 複数の条件が横に並べて置かれることがある
    • 縦配置と横配置が同じ規則の中で混在することもある
  • 横線の上の条件は通常ほかの判断だが、任意のブール条件である副条件(side condition) が置かれることもある
    • 変数規則の x:τ ∈ Γ がその例である
    • アルゴリズム的な型システムでは α fresh が使われることがあり、これは α が他の型変数と区別される新しい型変数でなければならないことを意味する

サブタイピング

  • サブタイピングは、型どうしの適合性を厳密な同値性よりも緩く扱う関係であり、明示的に定義する必要がある
  • 通常 τ₁ <: τ₂ と書き、「τ₁ は τ₂ のサブタイプ」と読む
  • 単純なサブタイピング関係では、トップ型 ⊤ とボトム型 ⊥ を導入できる
    • τ <: τ: すべての型は自分自身のサブタイプ
    • τ <: ⊤: すべての型は ⊤ のサブタイプ
    • ⊥ <: τ: ⊥ はすべての型のサブタイプ
  • 最初の規則は反射律であり、しばしば refl と略される
  • サブタイピングを許可するには、それを許容する各型付け規則の中で、その関係を明示的に使う必要がある
    • 関数適用規則では、引数型 τ₁ がパラメータ型 τ₂ のサブタイプであれば適用を許可できる

複数のコンテキストと双方向型検査

  • 一部の型システムでは、ひとつ以上のコンテキストを含む型付け判断を定義する
    • 二つ目のコンテキストは通常 Δ と呼ばれる
    • Γ;Δ ⊢ e : τ は、二つのコンテキストがどちらも入力のように使われるときによく使われる
    • Γ ⊢ e : τ ⊣ Δ は、Δ が出力のように使われるときによく使われる
  • 二つ目のコンテキストは用途に応じて異なる使われ方をする
    • 特定の変数をある式の中でだけ参照できるようにできる
    • リソース意識型プログラミング言語では、どの変数が消費されたかを追跡する出力コンテキストとして使える
  • 双方向型検査は、制約ソルバなしで制限付きの非局所的型推論を行うアプローチである
  • 双方向システムでは、一般的な Γ ⊢ e : τ という判断を二つの専門的な判断に分ける
    • Γ ⊢ e ⇐ τ: 式 e が期待される型 τ を持つかを確認する検査(checking) 判断であり、アルゴリズム的には τ は入力である
    • Γ ⊢ e ⇒ τ: 期待型情報がないときに使う推論(inference) 判断であり、アルゴリズム的には τ は出力である
  • 二つの判断は相互再帰的に定義され、型情報を双方向に受け渡す
  • この方式では一部の型注釈を省略でき、ラムダ抽象の検査規則では期待される関数型からパラメータ型を得られるため、変数束縛子の注釈を省略できる

関連記事

1件のコメント

 
GN⁺ 2023-08-17
Hacker Newsの意見

  • Guy Steeleは以前、このテーマで発表したことがある。いくつかの表記には検索しやすい名前も付けていて、たとえば2次元推論規則ダイアグラムのようなもの
    彼はこれをコンピュータサイエンスのメタ表記法と呼んでいるが、個人的にはプログラミング言語理論寄りに見える。 https://m.youtube.com/watch?v=dCuZkaaou0Q

  • この表記法はFregeまでさかのぼる。何を探せばよいか分からないと検索しにくいが、この記事はかなり良い要約に見える: https://plato.stanford.edu/entries/frege-logic
    ターンスタイル記号 |- はすでに使われており、授業で「Fregescher Schlussstrich」、つまりFregeの結論線と呼ばれていた横線は、もともとターンスタイル自体の一部だったものが、現代の表記では別要素になったようだ

    • 「Schlussstrich」はおそらく演繹線や推論線に近い訳だと思う

  • Benjamin C. PierceのTypes and Programming Languagesは、こうした内容を扱う良い教科書

    • TAPLは皮肉なことに、自分が使っている構文の基本的な意味を説明する点ではかなり不明確。この回答のほうがTAPLより桁違いに明確

  • コンピュータサイエンス専攻なのに、|– と |= の意味の違い、そして使われている変数がそれぞれどのメタ構文レベルにあるのか、いまだに混乱する
    皮肉なことに、表記法自体に明示的な型がないことが一因

  • 読もうか迷っている人へ: この記事はコンピュータサイエンス論文に出てくる型システム表記法の説明で、実質的には型システムのためのBNF記法、推論規則などの入門書
    良い要約に見える

    • 正直、記号を英単語でどう読むかを教えてくれるチートシートだけあればいい
      型適用の論理的概念は理解しているが、コンピュータサイエンス論文を頻繁に読むわけではないので、記号と意味の対応が頭に定着しにくい
    • こういうものが長年にわたって徹底的に抽象化されてきた点に、コンピュータサイエンスらしさが表れている

  • 例の中で 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 は「𝗍𝗋𝗎𝖾+2 は 𝖨𝗇𝗍 型である」という意味だが、𝗍𝗋𝗎𝖾+2 という式自体が意味をなさず型もないので、さらにおかしい、とされている
    ところがPythonでは True + 2 は実際に整数で、値も3。そうあるべきかどうかは別として、実際にそうなっているという話

    • True + 2 が意味をなすと思うなら、それを許す判断規則を自分で定義すればよい
      論理と型システム理論は、どの公理と推論規則を使うか自体には関心がなく、その規則と相互作用を推論できるようにするだけ。たとえば |- True : Bool, |- True : Int のように置いたり、特定の式でだけ許したいなら |- x : Int から |- True + x: Int を導くように作れる
    • これは言語ごとに違うのでは？ たとえばCでは true が1にマッピングされるので true+1=2 になる
    • PythonやCで True + 2 がエラーを出さないとしても、プログラマに少しの糖衣構文を与えるために言語の意味論を推論しにくくしているので、やはり愚か

  • 良い。数年間気になっていたが、もっと調べるには検索語をどうすればいいのか分からなかった

  • たまに苦労して身につけた秘伝の知識を誰かが無料で公開してしまうと、なんとなく嫌になる ;) 自分がこれを学んだときにこういう記事があったら本当に良かったと思う。アクセスしやすくなれば、ひどい言語が減ることを願う

  • Ada Reference Manualを読んだとき、この種の構文にはすぐ気づいた。名前は知らなかったが、実際の使用例として見ると興味深く、言語全体がその記法で定義されている
    例: https://ada-lang.io/docs/arm/AA-3/AA-3.7#syntax

  • ここは、私が最後まで押し通すことにした持論を布教するのにちょうどよさそうな場所だ。コロンを使う型注釈の書式では、コロンの両側の空白は同じであるべきだ
    私には、たまたま同じ形、つまり二つの点で書かれる別々の記号があるように見える。一つは英語の場合のように前半が後半を導入する、あるいは左側が右側のラベルであるラベル用コロンで、Python のブロック開始、キー・バリューのペア、C や Rust の構造体の名前・値ペアがこれに当たる
    もう一つは数学から借りてきた型注釈だ。これは二項関係であり、二項関係では左右の空白を同じにする。x= 1、x> y、x+ zとは書かないのと同じで、x: Xではなくx : Xと書くほうが自然だ
    a: bを見るとすぐにラベル用コロンとして読めてしまい、型注釈の場合は毎回ごく小さいながら追加の頭の中での変換が必要になる。これはプログラミング言語の構文についての話で、個人的にはX xよりx : Xのほうがずっと好みだ
    [1] “Evangelion”は εὐαγγέλιον、つまり良い知らせという意味に由来する格好いい単語だ。[2] https://en.wikipedia.org/wiki/Colon_(punctuation)#Usage_in_E...

    • いくつか誤解があるかもしれない。数学の文章でもf: X->Yのようにコロンの右側にだけ空白を多く置く表記は実際に出てきて、確認した本3冊のうち1冊はその表記だけを使っていた
      また、それもなおラベリングに近く、特定の形の写像にラベルを付けているものだ。数学でコロンが本当に別の意味で使われるのは、such thatの略として使われる場合で、たとえば{ x : x \in IN and x | 2}のような集合の定義や、量化子と一緒によく使われる
    • 面白い見方だ。追加の精神的ステップについての話は、私がよくあるX x表記を読むときに感じることと同じだ。x: Xのほうが私にはずっと自然で、自然言語でコロンを使うやり方にも近く感じられる
      何らかの命題があり、コロンの後ろがその命題をさらに詳しく説明する、という形で、型も左側にあるものについての追加情報だという点でぴったり合う
    • 型理論では、普通はt[空白]:[空白]Tのようにコロンの両側に同じ空白を置くのが標準的な慣習だと思う
      型理論全般には一貫性のない混乱した面もあるが、この場合だけは、みながかなり一貫している珍しい例だ。学部時代に自分がどう書いていたか気になって見てみたら、私も見栄えよく対称に書いていた: https://dvt.name/logic/horse2.pdf
    • x: Xは「コロンの後ろに説明が来る」用法に対応している
      つまり、variable x: It’s an X.のような形だ
    • age: intは英語で「person’s age: an integer」のように簡単に読み替えられる
      だからコロンが特に気になったことはない