🎼

Haskellの型システム(+拡張)を実装して学ぶ

2022/11/23に公開

導入

Mark P. Jones: Typing Haskell in Haskellという論文があります。この論文は、題通りHaskellでHaskellの型チェッカを実装するというものです。詳細な解説がされており非常にわかりやすく、また型システムの体系的な知識が無くても理解できるように構成されています。

しかしながら、この論文にはソースコードを入力にとって型チェックを行うまでに必要な実装の全ては含まれておらず、プログラムを入力に取って動作させるまでにはいくつかの変換や解析が必要です。Titan Type Checkerは、これら不足している機能(+拡張)を実装し、実際にスタンドアロンに動作する型チェッカを実装したものです。本記事では、論文で解説されていない事柄を中心に振り返りたいと思います。

Typing Haskell in Haskellの動作まで

構文解析 (Parser.hs)

入力のソースコードは単なる文字列なので、まずは字句解析・構文解析によって入力をASTに変換する必要があります。TitanではASTはTT.hsに定義されています。

Typing Haskell in Haskellで実装する型システムはその名の通りHaskellのものなので、Haskellの構文をそのまま扱えると過不足がなく、構文を考える必要もなく丁度良いのですが、Haskellの構文はインデントベースで動作するなど若干パースが面倒なのもあり、非インデントベースの適当な構文を定義してmegaparsecでパーサを書きました。

名前解決 (Resolver.hs)

プログラム中の定義(Def)を集め、使用(Use)を解決します。現代的なプログラミング言語では、モジュールや名前空間等の機能の存在によってより複雑な前処理を必要となりますが、それは本筋ではないのでTitanでは「フラットな名前空間1つ」としました。これにより、名前解決の主要な仕事は「Map に定義を集め、全ての使用が解決可能かを検証する」だけで済みます。
それでもTitanでは、このフェーズで追加で行う仕事があります。

全称量化子の明示

恒等関数を考えます。恒等関数をScalaで書くときは、パラメタ化された型(Parameterized types)を用いるでしょう。

def identity[A](x: A): A = x

対してHaskellでは以下のように書きます。

identity :: a -> a
identity x = x

Haskellでは、型中の名前が小文字 [a-z] で始まる識別子は型変数として、大文字 [A-Z] で始まる識別子は型構成子として解釈されます。ここで、HaskellではScalaの [A] に相当する、型変数を宣言するような記述がありません。Haskellでは 型変数は暗黙に量化される ためです。GHCの ExplicitForAll 拡張で全称量化子 (forall <tyvars>.) を明示できます。

identity :: forall a. a -> a
identity x = x

Typing Haskell in HaskellおよびTitanの型推論のフェーズは、入力中の型シグネチャには全称量化子が明示されていることを前提とします。これは後述のカインド推論のフェーズも同様です。そのためTitanでは、カインド推論の前、この名前解決のフェーズで、型シグネチャ中に表れる量化されていない型変数に対応するように、全称量化子を補完します。この補完はカインド推論や型推論とは独立した単なるASTに対する変換操作であり、明示的な型シグネチャのない定義 (推論によって型シグネチャが与えられる定義) には何もしません。

カインド推論 (KindInference.hs)

Typing Haskell in Haskellでは、カインドは全て事前に決定済みの入力が与えられるとされていますが、入力のプログラムではあらゆるカインドが明示されているわけではないので、型推論の前にカインドの推論が必要となります (むしろHaskell標準ではカインドは常に推論によって決定される?)。例えば、

-- a はデータ型の位置で使用されているので a :: *
data F a = F a

-- a は Int :: * を引数に取り、結果がデータ型 * でなければならないので a :: * -> *
data F a = F (a Int)

-- a :: _1 -> *, b :: _1 と推論され、未確定のカインド _1 が * にdefaultingされる
data F a b = F (a b)

カインド推論について、Haskell 2010 Language Reportでは4.6 Kind Inferenceにサラッと書かれていて、以下のようなステップで行われます:

data, type (型シノニム), class 宣言を集め依存性解析を行う
それぞれの依存グループで型推論と同様の単一化アルゴリズムでカインドを決定していく
確定しないカインドは単に * (Type とも。データ型のカインド) にdefaultingする

依存性解析は、具体的には強連結成分の分解を行います。Titanにおいてはデータ型宣言の集合、型クラス宣言の集合でそれぞれ行います。^[1]

カインド推論と依存性解析についての例をもう一つ挙げておきます。

-- (1)
data F a
data G = G (F Maybe)

この例は、 F の a が a :: * -> * と推論されるのではなく、エラーとなります。 G は F に依存していますが、 F は G に依らず宣言されているため、 F の a は a :: * とdefaultingされ、 G のカインド推論時にエラーとなります。

他に実装中に気付いた点として、GHC では ScopedTypeVariables を有効にしていてもカインド推論はそれぞれの型シグネチャ単独で完結します。具体例としては、

foo :: forall m a. m a -> ()
foo _ =
  let bar :: forall f. a f -> ()
      bar _ = ()
  in ()

のような定義は m :: (* -> *) -> * a :: * -> * とは推論されず、 foo の型スキーム時点で m :: * -> * a :: * とdefaultingされ、ローカルな bar のカインド推論中にエラーとなります。Titanもこの挙動を採用しました。

型クラスに関する制約

Typing Haskell in Haskellの addClass, addInst のあたりで解説されているように、Haskell標準ではクラス宣言やインスタンス宣言に一定の制約が課せられています。GHCの FlexibleContexts, FlexibleInstances, UndecidableInstances 拡張あたりで緩和されるあれこれです。これらの制約にはいくつか理由があり、ものによっては保守的とも言えそうな制約もありますが、制約が果たす重要な役割にインスタンス解決の停止性の保証があります。

instance Num a => Num a

このインスタンスは、インスタンス解決が停止しません。 Num a を満たすために Num a を満たす必要があり、…とインスタンスの探索を繰り返してしまいます。

Typing Haskell in HaskellおよびTitanでは、これら制約を満たしているかのチェックの実装を省略しています。理由はいくつかあるのですが、TitanにはGHCのような言語拡張を有効にするプラグマのようなものを設けたくなく、その上で自由度が高く(しかし停止性は保証されない) UndecidableInstances 相当をデフォルトにしたという感じです。モナド変換子の例などにこの自由度が必要となります。

一方で、Titanでは以下のようなインスタンスの重複をeagerに弾くようにしました:

class A a
instance A Int
instance A a

GHCではこれは、インスタンスの解決時に複数のインスタンスが選択されて初めてエラーとなるようです。HaskellにはRustのようなOrphan rulesが存在せず、Orphan instancesが存在しうること辺りが理由ではないかと思います。

型推論 (TypeInference.hs)

構文解析、名前解決、カインド推論を経て、Typing Haskell in Haskellのメインである型推論のフェーズに入ることができます。基本的に論文の通りに実装していきましたが、いくつか変更やバグらしき挙動の調整を行いました。

レベルの導入

Titanでは、Extension of ML type system with a sorted equationtheory on types^[2]で取り上げられている手法を採用しました。型変数にレベルを導入することで実装が少しシンプルになります。

`tiImpls` の修正

Typing Haskell in Haskellの中でも下手すると最も複雑な関数 tiImpls の実装に、若干問題がありました。以下のような定義を考えます (コード自体に意味はありません):

f = fst g  -- f :: a
g = (f, 0) -- g :: Num b => (a, b)

f, g は相互参照しているので一つの [Impl] グループでまとめて型付けされます。ここで、コメントにある型シグネチャの a, b 相当の型変数について、

a はグループの全ての型 (f, g の型) に表れるため、defaulting出来なくて良い (呼び出し側によって常に型を決定できる)
b は f の型に表れないため、 f が呼び出されたときにも決定できるように、defaulting可能である必要がある

という違いがあります。この上で、Typing Haskell in Haskellの実装では、

tiImpls ce as bs = do
  ...
  let vss = map tv ts'
      gs  = foldr1 union vss \\ fs -- (1)
  (ds, rs) <- split ce fs (foldr1 intersection vss) ps' -- (2)
  if ... then do -- この問題の本筋でない
    ...
  else do
    let scs' = map (quantify gs . (rs :=>)) ts' -- (3)
    return (ds, zipWith (:>:) is scs')

(1)でいずれかの型に表れる型変数を集め、(3)で全ての関数で量化する対象の型変数として渡しています。こちらは問題ありません(quantifyによって無関係な型変数は取り除かれる)。
(2)で全ての型に必ず表れる型変数を split に渡し、 split で得られたいずれかの関数でdefaultingが必要になる型変数が含まれる述語を取り除いた述語セット rs を(3)で全ての関数でスキームのコンテキスト部分として使用しています (rs :=>)。

…自然言語で書いても難解なんですが、結果として以下のように推論されてしまいます。 (g にあるべき Num b が失われている)

f = fst g  -- f :: a
g = (f, 0) -- g :: (a, b)

修正には、 split 内で計算されている rs' を split の返値に加えた上で、各関数の quantify 時に、その関数の型に出てくる型変数に関連する述語を :=> の左辺に加える必要があります。

テスト

Titan Type Checkerは、「プログラムを入力にとり、型チェックが成功するなら、推論された型シグネチャが明示された同等なプログラムとして出力でき、それを再度入力として取っても型チェックが成功し、一度目と同じ出力が得られる」という要件を満たすことにしました。これにより、テストコードを例えば以下のように記述できます。

spec = describe "Titan Type Checker" $ do
  it "type checks" $ do
    -- f の型が [(a : *) (b : *))] a -> b -> a と推論されシグネチャが付与される
    "val f = fun x y -> x"
      ==> "val f : [(a : *) (b : *)] a -> b -> a = fun x y -> x"
  ...

-- codeに与えられたプログラムを型チェックし、プログラムとして再出力する
titan :: String -> Either Error String
titan code =
  fmap (pprint . program)
       (parse "test" code >>= bind emptyGlobal >>= resolve >>= ki >>= ti)

-- code, resultはいずれも型チェック後はresultを出力する
(==>) :: HasCallStack => String -> String -> Expectation
code ==> result =
  forM_ [code, result] $ \code ->
    titan code `shouldBe` Right result

軽い気持ちでこのような要件を設定しましたが、実際にはこの要件によってこれまでの解説で触れていた ExplicitForAll, ScopedTypeVariables あたりのGHC拡張相当の機能が必須になり、オリジナルのTyping Haskell in Haskellより実装が複雑になってしまったという経緯があります。

しかしながら、ここまでの実装でも(これ以降に取り上げている拡張を実装せずとも)、HaskellのPreludeから適当に定義を抽出した0.prelude.titanがこのテストを通過するようになりました。

型システムの拡張

GHCで頻出の言語拡張に相当する機能などをいくつか加えてみました。以下は実装当時の記憶が薄く内容も薄いです…

型クラスが複数のパラメータを取れるようにする

GHCの MultiParamTypeClasses 相当の拡張です。

データ構造上で Pred が複数パラメータを取れる形に変更して、それによって発生する型エラーに沿ってコードを修正していけば自然と対応できたかと思います。(あまり覚えていないのですが…)

関数従属性 (Functional dependencies)

複数のパラメータを取る型クラスでは、推論結果の曖昧さが解消できないケースがしばしば実用上の問題になります。これを回避できるような型クラスの定義について、GHCではいくつの選択肢がありますが^[3]、モナド変換子などでは FunctionalDependencies 拡張が特に馴染み深いです。これをTitanに実装してみました。

class Monad m => MonadState s m | m -> s where
  get :: m s
  put :: s -> m ()

Mark P. Jones: Language and Program Design for Functional Dependenciesで関数従属性の背景、形式化その他が述べられています。実装にあたっては2.5が重要です。

まず、従属性を満たすようにインスタンスの実装を検査する必要があります。

class F a b | a -> b

-- a ~ [x] から b ~ y を一意に決定できない
instance F [x] y
-- こちらは F x y なので a ~ Maybe x より b ~ y を決定できる
instance F x y => F (Maybe x) y

-- 以下2つのインスタンスは a ~ Int に対する b が一貫していない
class F a b | a -> b
instance F Int Bool
instance F Int Int

この制約によって、従属性に基づいた型の単一化を推論中に自由に行うことができます。

class F a b | a -> b where
  f :: a -> b

instance F Bool Int where
  f _ = 5

g = f True -- F Bool a において、 a ~ Bool から一意に b ~ Int とできる
h x = (f x, f x) -- (F a b, F a c) において、同様に b ~ c とできる

関数従属性の実装によって、モナド変換子を含む2.mtl.titanを定義して解釈できるようになります。
ただ、Titanの関数従属性の実装はとりあえず実装してみたというレベルで、かなり計算効率を度外視した実装となっており、実用的な速度で動作させるには大きな改善が必要そうです。また、今はRustをよく書いていて関連型のほうが馴染み深くなったので、次の機会があったときは(fundepsは実装せず)そちらを実装するという選択を取りそうです。

列多相 (Row Polymorphism)

※この節は特に用語が怪しいかもしれません

列多相は、拡張可能なレコード型などに用いられている多相性で、GHCではなくPureScriptやOCamlなどで採用されています。その詳細はDaan Leijen: Extensible records with scoped labels 等で述べられています。

まずは多くのプログラミング言語でよく見られるレコードを考えます。レコード型を加え、それを以下のような構文糖衣だと考えます。

  { x : Int, y : Bool }
~ {_} <x : Int, y : Bool>
~ {_} <x : Int | <y : Bool>>
~ {_} <x : Int | <y : Bool | <>>>

先頭の型コンストラクタ {_} のカインドは # * -> * で、これは「# * を引数に取ってデータ型を構築する」というカインドになっています。 # * が * の Row … ラベルとデータ型(*)のマッピングです。

空のRowは <> で、Rowの拡張は <label : ty | row> で表現されます。 <x : Int | <y : Bool | <>>> によってラベル x, y とデータ型 Int : *, Bool : * のマッピングがRowとして表現され、それが {_} に適用されることでレコードのデータ型となります。なお、Rowは異なるラベルについて順番を入れ替えることができます。

このような構成要素でレコードが表現されるとどう嬉しいかというと、Rowの拡張 <label : ty | row> の row の位置に列変数(カインドが # _ である型変数)を置くことで、Rowについての多相をすんなり扱うことができます。こちらも構文糖衣があります。

  { x : Int, y : Bool | r }
~ {_} <x : Int, y : Bool | r>
~ {_} <x : Int | <y : Bool | r>>

列変数を含む単一化の具体例を挙げてみます。

{ x : Int, y : Bool, z : String } と { x : Int, y : Bool | r } の単一化では、r ~ < z : String > と単一化されます。
{ x : Int | r1 } と { y : Bool | r2 } の単一化では、 r1 ~ < y : Bool | r3 >, r2 ~ < x : Int | r3 > と単一化されます (r3 は新しい列変数)。

ある全容が明らかになっていないレコードについて、未決定の部分がうまく列変数で表現できることがわかります。

まとめ

Typing Haskell in Haskellの実装を通して、Haskellの型システムへの理解度を高めることができました。

ここで得られた知見はRustによる自作言語の実装にも活かしており、型チェッカ周りの実装はTitanをベースにしています。一方で、自作言語は実装言語がRustなので、unificationの実装には置き換え (substitution) 結果を格納するプールを破壊的に更新する形で扱っていたりと、手続きは大きく異なります。

脚注

Titanは型シノニムを持たず、またデータ型宣言に制約を含める機能も持たないため、データ型宣言は型クラスに依存し得ない ↩︎
これを解説している日本語の記事もありました ↩︎
GHCにおける関数従属性と関連型の比較: Type Families (TF) vs Functional Dependencies (FD) ↩︎