型の型：HaskellのKindシステム

Types of types: HaskellのKindシステム

Contents · 7 sections

• 値
• 型
• Kind
• Higher-Kinded Types
• Higher-Kinded Data
• カスタムKind
• 結論

HaskellのRedisサーバークローンに型付き設定を追加する作業中に、HaskellのKindシステムに端を発する新しいテクニックをいくつか学ぶことになりました。この記事では、そこで学んだことと、それを使って構築できたものについて議論します。

まずは最初から、値について始めましょう。

値

これらはプログラムで操作する構成要素、例えば 1、2、True、"hello" などです。関数型プログラミングの文脈では、「項（term）」とも呼ばれます。これらは消費し、作成し、計算し、出力するものです。値の管理と操作は、プログラミングやソフトウェアエンジニアリングの実践において大きな部分を占めます。

私たちは皆、日々さまざまな値を取り扱っています。ファンタジー設定の生き物のように、特定の特性を共有する値――同じ方法で作成、使用、操作される値――は同じ種に属します。形式的には、これらの「種」は「型（Type）」と呼ばれます。

型

型とは、関連する値のグループです。別の言い方をすれば、型の概念は、関連する値のグループを集合的に参照するための手段を提供してくれます。多くのプログラミング言語では、Int、string、Bool、Textなどの単語を使って型を示します。

値を型にグループ化する主な利点は、私の意見では抽象化です。型は、値の特性と、それに対してまたはそれを使って実行できる操作の種類を、プログラマーとコンパイラの両方に伝えます。ゲームの武器クラスを考えてみてください。多くのRPGには武器クラスがあり、武器のクラスはしばしば、実行できる攻撃の種類や、それを使って使用できるスキルを決定します。型も値に対して同様のことを行います。

これをさらに一歩進めて、型をどのように分類するか、と自問するかもしれません。分類する必要はあるのでしょうか？ なぜ？ これらの質問に答えるには、「Kind」の世界に足を踏み入れる必要があります。

Kind

Kindは、型にとって値が型にとってであるようなものです。Kindシステムの私の直感は、それが型レベルのすべてのものに対する分類手段であるということです。「型レベルのすべてのもの」は単に日常的な型を指すだけだろうと思うかもしれませんが、Haskell（および他のいくつかの言語）では、型レベルの数値（Kind Nat）、型レベルの文字列（Kind Symbol）、または型クラスからの制約（Kind Constraint）のような他の型レベルの構造も存在します。

これらの詳細には立ち入りませんが、NatとSymbolは型レベルプログラミングの文脈でよく現れます。一方、Kind Constraintのエンティティは、ほとんどの場合（完全に適用された）型クラスであるため、より馴染みがあるでしょう。例えば、Show型クラスはKind Type -> Constraintに属し、Show IntはKind Constraintに属します。

通常の型はKind Typeに属します。紛らわしいのは分かっています。型コンストラクタ、つまりMaybe、Either、Last、Proxy、Dualなどのものは、以下の表に示すように、そのarityとパラメータのKindによってKindが決まります。

* vs Type

古いドキュメントや一部のGHCエラーメッセージでは、私がTypeと書くところに*が見られます。これらは同じものです。私の理解では、*はTypeの同義語であり、その逆も同様です。*は古い名前であり、GHCはそれを非推奨にする予定です（-Wallは既に使用時に警告します）。

豆知識

技術的には、通常の型も型コンストラクタであり、パラメータを持たない型コンストラクタです。これらは「nullary type constructors（ナル型コンストラクタ）」と呼ばれることがあります。

Kindがなければ、Maybe、Maybe Int、Showのような型レベルの構造を区別する方法はないと私は思います。Haskellの学習段階によっては、これらの他の型レベルエンティティの利点が完全には明らかでないかもしれませんが、それらはすべてHaskellの型システムをより表現力豊かにするために機能し、型システムでより多くのことをコード化できるようになり、結果としてより安全なプログラムを書くことが容易になると保証できます。

Higher-Kinded Types

さて、以前に型が値に対する抽象化を可能にすると述べました。これは、型を通じて値のセットを集合的に参照できることを意味します。同様に、特定のKindを持つことで、型レベルの構造のコレクションに名前を付けます。例えば、Kind Type -> Typeは、単一の通常の型を引数として取るすべての型コンストラクタを集合的に参照します。これにはMaybeのようなものだけでなく、Either StringやThree Int Stringのような部分適用も含まれます。同様に、Kind Type -> Type -> Typeは、2つの通常の型を引数として取るすべての型コンストラクタを集合的に参照します。これを値/項レベルに戻すと、関数シグネチャに似ています。Int -> Boolという関数シグネチャは、Intを引数として取りBoolを返すすべての関数を集合的に参照します。

Int -> Boolのようなシグネチャが関数のセットを集合的に参照することは知っていますが、(Int -> Int) -> Boolのようなものについてはどうでしょうか？ それは何を意味するのでしょうか？ そのシグネチャは、Int -> Intというシグネチャを持つ関数を引数として受け取った後にのみブール値を返すすべての関数を表します。このタイプのシグネチャは非常に一般的であり、このようなシグネチャを持つ関数は高階関数と呼ばれます。

さて、このアイデアをKindレベルに外挿しようとするとどうなるでしょうか？ Type -> TypeのTypeパラメータを(Type -> Type)に置き換えたらどうなるでしょうか？ まず、(Type -> Type) -> Typeのようなシグネチャが得られます。Typeはすべての通常の型のKindであり、Type -> Typeは単一の通常の型を引数として取るすべての型コンストラクタのKindであることを知っています。これらを組み合わせると、(Type -> Type) -> Typeというシグネチャは、型コンストラクタを引数として取るすべての型レベル構造のKindを表すことになります。どこに向かっているか分かりますか？ (Int -> Int) -> Boolのようなシグネチャを持つ関数が高階関数と呼ばれるのと同様に、(Type -> Type) -> Typeや(Type -> Type) -> (Type -> Type) -> TypeのようなKindを持つ型コンストラクタは、総称してHigher-Kinded Types、略してHKTと呼ばれます。

小さな例を挙げましょう。

data Wrap (f :: Type -> Type) = Wrap (f Int)

Wrapは型コンストラクタfを取り、その中にIntを格納します。そのため、Kindは(Type -> Type) -> Typeです。Wrap Maybeは通常の型であり、Wrap []も同様です。Wrap (Just 5)とWrap [1, 2, 3]はそれぞれの値です。前の表のComposeも、パラメータが多いだけで別の例です。

別の角度から見ると、MaybeやEitherのようなパラメータ化された型が他の言語でジェネリクスと呼ばれるものだとすれば、HKTは他のジェネリクスを引数として取ることができるジェネリクスです。

HKTの概念は、型クラスと組み合わさることで、型レベルの構造に対して特定の機能（functionality）を実装する能力を与えてくれます。これは、多くのコンテキストで操作を再利用できるため便利です。例として、Functor :: (Type -> Type) -> Constraintを取り上げましょう。Functor自体はHKTではありません。そのKindはConstraintで終わっており、Typeではありません。しかし、そのパラメータは型コンストラクタであり、これは高階（higher-Kinded）です。

型コンストラクタがFunctorインスタンスを持っている場合、fmap関数を使用してその内容をマッピングできます。さらに、Functorの高階性のおかげで、適切にKind付けされた型コンストラクタ（具体的にはType -> Type）に対して単一のFunctorインスタンスを定義するだけで、その型コンストラクタの任意の特殊化でfmapを使用できます。私が言いたいのは、例えばMaybe aではなくMaybeに対してFunctorインスタンスを定義するため、Maybe Int、Maybe String、Maybe BoolなどのMaybe aのすべての具体的なバージョンでfmapを使用できるということです。実際、それは他の方法では機能しません。FunctorのKindシグネチャはKind Type -> Typeの型コンストラクタしか受け付けないため、Kind TypeのMaybe Intのようなものは候補にすらなりません。インスタンスはMaybe自体に属します。この原則は、他のすべての上位Kind型クラスと適切にKind付けされた型コンストラクタに適用されます。

非技術的な言葉で言うと、食べるためのボウルを想像してください。ボウル自体を電子レンジ対応にすれば、その中に食べ物を入れて温めることができます。この場合、ボウルは「適切にKind付けされた型コンストラクタ」であり、「電子レンジ対応」であるかどうかを決定する基準は、高階型クラス（Functorのような）です。「電子レンジ対応」というラベルはボウルに付けられ、その型クラスインスタンスです。そして、温めることができる食べ物の入ったボウルは、型コンストラクタの特殊化を表します。ここでも、他の方法では機能しません。誰もスープのボウルを電子レンジ対応だと認証しません。ラベルはボウルに属し、ボウルの内容に関係なく適用されます。

Higher-Kinded Data

Higher-Kinded Data、略してHKDは、型レベルのものの代わりに、データ型が1つ以上の型コンストラクタをパラメータとして取り、それらを使用してフィールドの一部またはすべてをラップするパターンです。これは「高度」と見なされるかもしれませんが、Higher-Kinded Typesを理解すれば、実際にはかなり簡単です。例を挙げましょう。

-- `f`パラメータは型コンストラクタであり、`Profile`をHigher-Kindedにしています
data Profile (f :: Type -> Type) = Profile
    { age :: f Int
    , name :: f String
    , profession :: f String
    , address :: f String
    }

-- `f = Identity`: すべてのフィールドが存在する必要があります
grace :: Profile Identity
grace = Profile (Identity 37) (Identity "Grace") (Identity "Computer scientist") (Identity "New York")

-- `f = Maybe`: サインアップフォームが半分埋まっているように、任意のフィールドが欠落している可能性があります
draft :: Profile Maybe
draft = Profile Nothing (Just "Grace") Nothing Nothing

-- `f = Const String`: 任意のフィールドは、その型に関係なく`String`を保持します。フォームのラベルのようなものです
labels :: Profile (Const String)
labels = Profile (Const "Age") (Const "Name") (Const "Profession") (Const "Address")

このPRを詳しく見てみましょう。これは私のredis-haskellプロジェクトのもので、コマンドラインオプションとredis.confファイルで宣言されたオプションの両方から取得される型付きRedis設定のサポートを追加しました。

まず、これを実装するために、サポートしたいフィールドを持つRedis設定のデータ型表現が必要でした。

最初につまずいた問題は、重複の問題でした。私の最初のデータ型アイデアはプレーンなレコード型でしたが、2つのわずかに異なるコンテキストをサポートする必要がありました。

• すべてのフィールドが利用可能で、公式のデフォルト値に初期化されるデフォルト設定。
• フィールドがnull許容である必要があるコマンドライン設定とredis.conf設定。

私の最初の方向性は、2つのレコード型を定義することでした。1つはフィールドの型がプレーンであり、もう1つはフィールドがLastでラップされているものです。

data RedisConfig = RedisConfig
    { rdbFileDirPath :: SomeBase Dir
    , rdbFilenamePath :: Path Rel File
    , useRDBCompression :: Bool
    , genRdbChecksum :: Bool
    , port :: Int
    }
    deriving stock (Generic)
    
data PartialRedisConfig = PartialRedisConfig
    { rdbFileDirPath :: Last (SomeBase Dir)
    , rdbFilenamePath :: Last (Path Rel File)
    , useRDBCompression :: Last Bool
    , genRdbChecksum :: Last Bool
    , port :: Last Int
    }
    deriving stock (Generic)

なぜLastなのか

Maybeの<は、オペランドのいずれかがNothingでない限り、それがラップする型のSemigroupセマンティクスに委譲します。さらに、機能するには、ラップされたフィールドのすべての型がSemigroupインスタンスを持つ必要があります。BoolとIntはそれを持っていません。そして、インスタンスを持つ型であっても、<は2つの値を結合して1つを選択するのではなく結合します。Lastは存在する最後の値を保持し、後続のソースが先行する値をオーバーライドできるようにします。

このアプローチは、サポートされている設定フィールド名と型の単一の真実の源（single source of truth）を望んでいたため、気に入らなかったのです。2つのデータ型があると、一方のバリアントを変更しても、もう一方を更新することを忘れる可能性があります。実装方法によっては、型システムが不一致を検出できたかもしれませんが、それは十分ではありませんでした。

1つのオプションは、すべてのフィールドがLastでラップされた単一のRedis設定型を定義することでした。Lastは最も右側のJust値を保持するため、defaults <> confFileOpts <> cliOptsはコマンドラインオプションを優先し、次にredis.confオプション、そしてデフォルト値となります。まさに私たちが望むセマンティクスです。しかし、問題は最終結果でした。すべてのフィールドに値があったことが保証されていたとしても、それは依然としてすべてのフィールドがLastでラップされたレコードでした。結果として、その最終設定を読み取るすべてのサイトは、Nothingになり得ないLast値をアンラップする必要がありました。

また、おそらく疑問に思うでしょう。最終結果専用のプレーンフィールドを持つ別のレコードを定義しないのはなぜか…ああ…。はい。

したがって、再び、設定型の2つのバリエーションが必要でした。マージ用の一部分割されたものと、デフォルト用およびサーバーの残りの部分で使用するための一部分割されていないものです。私が望まなかったのは、2つの定義でした。

これを達成するために、次のような定義に至りました。

data RedisConfigF (f :: Type -> Type) = RedisConfigF
    { rdbFileDirPath :: f (SomeBase Dir)
    , rdbFilenamePath :: f (Path Rel File)
    , useRDBCompression :: f Bool
    , genRdbChecksum :: f Bool
    , port :: f Int
    }
    deriving stock (Generic)

RedisConfigFはHigher-Kinded Data型です。fパラメータがKind Type -> Typeであるため、Higher-Kindedです。これにより、RedisConfigF自体はKind (Type -> Type) -> Typeとなり、これは上記のWrap定義と同じです。これにより、上記で説明した両方のコンテキストに対して単一のデータ型定義が得られました。デフォルトと最終的なマージされた設定ではf = Identity、フィールド値が存在しない可能性のある他のケースではf = Lastです。

マージするために、redis.confオプションとCLIオプションの設定レコードを結合するためにLastのSemigroupインスタンスを活用します。次に、デフォルトでギャップを埋めます。これがマージコードです。

その後、すべてのフィールドが埋め込まれたRedisConfigF Identity型のレコードが得られます。しかし、f = Identityの場合、すべてのフィールドがIdentityでラップされており、アクセス時にアンラップする必要があります。実際のコードはそのアンラップを自動化していますが、その方法はこの記事の範囲を超えています。

いずれにせよ、私たちが歩んできたのは、Higher-Kinded Data型の力と有用性です。私が活用したもう1つの興味深いユースケースは、フィールドパーサーの関連付けにRedisConfigFを使用することでしたここです。f = Const (Text, ReadM PartialRedisConfig)を使用すると、同じレコードが各フィールドのredis.conf名とそのパーサーを保持するため、フィールドを追加して名前とパーサーをそこに指定し忘れた場合、コンパイラが警告してくれます。素晴らしいですね！

Barbies

このようなHigher-Kinded Dataを扱うためのbarbiesライブラリが存在することは知っていますが、この特定のユースケースに必要なものを構築する方が、よりシンプルで教育的だと感じました。

カスタムKind

最後に触れたいのは、カスタムKindです。はい、独自の型を作成できるのと同様に、独自のKindを作成できます。カスタムKindは、型システムに情報を昇格させるのに役立つ、独自の型レベル構造です。例：

{-# LANGUAGE DataKinds #-}

data Person = Person Symbol Symbol Nat

ここで、DataKinds拡張機能によってKindにも昇格されたデータ宣言があります。基本的に、その拡張機能はdata宣言構文のユーティリティを拡張し、データ宣言がデータ型だけでなくKindも定義するようにします。上記のコードスニペットの場合：

• Personは、カスタムデータ型とKindの名前です。
• Person Symbol Symbol Natは、Kindのメンバーである型レベルエンティティの構造/形状の説明です。
• 'Person :: Symbol -> Symbol -> Nat -> Personは、Kind Personの型レベルエンティティを作成するための型コンストラクタです。
• Person :: Symbol -> Symbol -> Nat -> Personは、型Personのデータコンストラクタです。

Kind Personのメンバーは次のようになります。

type Ada = 'Person "Ada" "Lovelace" 21   -- Ada :: Person

引用符とPun

引用符（tick）が'Personに見られるかもしれません。これはPunを曖昧にするためです。このコンテキストでは、Punとは、型とそのコンストラクタが名前を共有する場合（data Person = Person …のような）です。通常、Haskellは型と項を別々の名前空間に保持するため、これは問題ありません。しかし、DataKindsが有効になり、データコンストラクタが昇格されると、両方の名前（型とデータコンストラクタ）が型レベルで使用できるようになります。では、プレーンなPersonが既に型とKindを意味している場合、昇格されたコンストラクタを参照するにはどうすればよいでしょうか？ 引用符は、コンストラクタを明示的に参照できるようにします：'Person。

名前が衝突しない場合（data Person = MkPerson …のような）、引用符はオプションです。GHC 9.4以降、GHCはデフォルトでそれを書くことを推奨しなくなりました（GHC issue #20531）。しかし、私たちのPersonの例では、名前が衝突するため、引用符が必要です。

Personが型とKindの両方として表示されることに注意してください。さて、GHC 8以降、すべてのKindは型としても考慮されます。これは、親であり子でもあるようなものです。親は自分の子供にとって親であり、自分の親にとって子です。Personも同様に機能します。Adaが属するKindであり、Kind Typeに属する型でもあります。

さらに、一部の型は空（uninhabited）である可能性があるため、一部のKindも空です。例えば、Intは型としては値で満たされていますが、Kindとしては型レベルの構造では空です。逆に、Symbolは型としては空ですが、型レベルの文字列リテラルでKindとしては満たされています。実際、この理由から、私たちのPerson型は項レベルでは値を持てませんが（Person型の値を作成するためのSymbol型の値がない）、Kindレベルでは満たされる可能性があります。

Boolは、型としてもKindとしても満たされているため興味深いです。Natも同様で、Naturalのエイリアスです。

この説明はさておき、これをredis-haskellのユースケースに戻しましょう。私のPRでは、RedisConfigF型の各フィールドに2つのデータが必要でした。フィールド名が意味上の理由で実際のconfigキーと異なるフィールド名、およびその型です。当初、次のような別々の型エイリアスを定義しました。

type RDBFileDir = SomeBase Dir
type RDBFileDirConfigFieldName = "dir"

type RDBFilename = Path Rel File
type RDBFilenameConfigFieldName = "dbfilename"
-- フィールドごとにさらに1組

より良いカプセル化のために、型レベルのタプルも試しました。

type RDBFileDir  = '("dir", SomeBase Dir)          -- Kind: (Symbol, Type)
type RDBFilename = '("dbfilename", Path Rel File)

タプルPun

引用符はここでも同じように機能します。タプル構文もPunであり、(a, b)はタプル型とそのコンストラクタの両方を名前付けします。

しかし、それは項/値レベルで匿名積型（anonymous product type）を使用するようなものだったでしょう。(Symbol, Type)のようなものは構造的です。2つのそのようなペアは、意図に関係なく同じKindになります。そのため、代わりに、独自のカスタムKindであるConfigFieldを作成することにしました。これは名目（nominal）で、意味論的で、自己文書化されており、他の(Symbol, Type)ペアと混同することは不可能です。

フィールドが前のコードスニペットから書き直された定義を次に示します。

data ConfigField = ConfigField Symbol Type  -- DataKindsと併用すると、これもKindになります

type RDBFileDir        = 'ConfigField "dir"            (SomeBase Dir)
type RDBFilename       = 'ConfigField "dbfilename"     (Path Rel File)
type UseRDBCompression = 'ConfigField "rdbcompression" Bool
type GenRDBChecksum    = 'ConfigField "rdbchecksum"    Bool
type RedisPort         = 'ConfigField "port"           Int

これで、各フィールドのredis.confキーとそのHaskell型が単一のConfigField内に共存し、他の型レベルメカニズムを使用することで、その情報を項レベルでアクセスできるため、重複する必要がなくなります。これはいくつかの場所でgetConfigFieldNameを使用して行われます。コマンドラインパーサーここでは、各キーはフラグ名（"dir"は--dirになります）としても機能し、redis.confパーサーここでも同様です。

結論

要約すると、値は型にグループ化され、型はKindにグループ化されます。この記事の各パターンはその上に構築されています。Higher-Kinded Typesにより、WrapやComposeのような、他の型コンストラクタを引数として取る型を定義できます。Higher-Kinded Dataパターンにより、部分的または完全な単一の設定レコード型が得られました。そして、カスタムKindにより、各設定フィールドのredis.confキーとその型を保持でき、両者が乖離するのを防ぐことができました。

いつものように、さらにコードを見たい場合は、PRをチェックして、ご意見をお聞かせください。この記事は網羅的なものではありませんでしたが、読者の皆さんにKindに対するまともな直感と正しい方向への一歩を提供できたことを願っています。

次回まで！