/LugendrePublic/種多相 - Scrapbox Reader

generated at 2/15/2025, 7:06:46 PM
種多相
原文

TypeInType 
 PolyKinds ， DataKinds ， KindSignatures 
8.0.1以降
過去には，この拡張は高度な型レベルのプログラミング手法を可能にするために使用されていた．今では他のいくつかの拡張機能の省略形である．

PolyKinds
 KindSignatures 含む
7.4.1以降
種多相な型を許可する．

この節では，バージョン8.0以降でのGHCの種システムについて説明する．

ここで説明されている種システムは，拡張があってもなくても常に有効だが，標準のHaskellを超えた保守的な拡張である．上記の拡張は単純に構文を有効にし，推論アルゴリズムを微調整してユーザーがGHCの種システムの追加の表現力を利用できるようにする．

種多相の概要
以下の種を推論することを考えてみよう．
 kp1.hsdata App f a = MkApp (f a)
Haskell 98では， App の推論される種は (Type -> Type) -> Type -> Type である．しかしこれは必要以上に具体的である．というのも，なぜならHaskell98(の仕様)に適するもう一つの App の種として ((Type -> Type) -> Type) -> (Type -> Type) -> Type があるからである．ここで a に割り当てられる種は Type -> Type となっている。実際に，種シグネチャ( KindSignatures 拡張)がないと，Haskellコンパイラに2番目の種を推論させるためにダミーのコンストラクタを使う必要がある．種多型( PolyKinds )を使えば，GHCは， App の種として，最も一般的な種である forall k. (k -> Type) -> k -> Type 種を推論する．

したがって，種多相の主な利点は，これらの最も一般的な種を推論し，さまざまな種で App を使えるようにすることである．
 kp2.hsApp Maybe Int   -- `k` is instantiated to Type

data T a = MkT (a Int)    -- `a` is inferred to have kind (Type -> Type)
App T Maybe     -- `k` is instantiated to (Type -> Type)

Type-in-Typeの概要
GHC 8は，型と種が実際にはまったく同じものであると宣言することによって，種の多相性の概念を拡張する．GHCの中では型と種を区別するものは何もない．これについて考えるもう一つの方法は，型 Bool と「昇格された種」 Bool は実際には同一であるということである(項 True は式の中で使われ，型 'True は型の中で使われるので，項 True と型 'True は未だに違うことに注意せよ)．この型と種の区別のなさは，依存型付き言語の特徴である．完全依存型付き言語は式と型の違いをも取り除くが，GHCでそれを行うことはまたの日の話である．

型と種を組み合わせることによって可能になる1つの単純化は，  Type の型が単なる Type であるということである． Type :: Type 公理が非決定性につながる可能性があるのは事実だが，型と式の両方でプログラムを非決定にする方法が他にもあるため，これはGHCでは問題にない．この決定(他にも多数あるが)は，GHCの型システムの表現力にもかかわらず，Haskellで書いた「証明」は反論の余地のない数学的証明ではないことを意味している．GHCは部分的な正当性のみを保証する．あなたのプログラムがコンパイルされて完全に実行されるなら，それらの結果は確かに割り当てられた型を持つ．有限時間内に終了しないプログラムについては何も言わない．

この決定と内部でのGHCの設計についてもっと学びたければ， この種システムをGHC / Haskellに導入した論文を参照せよ．

種推論の原則
一般的に言って， PolyKinds が有効なとき，GHCは宣言での最も一般的な種を推論しようとする．多くの場合(例えば，データ型宣言の中で)，定義は種推論を知らせる右辺を持つ．しかし，必ずしもそうとは限らない．次の例を考えてみよう．
 kp3.hstype family F a
型族宣言には右辺はないが，それでもGHCは F に対して種を推論しなければない．制約がないので， F :: forall k1 k2. k1 -> k2 と推論することもできようが，これは多相的すぎるように見える．そのため，GHCはこれらの全く制約のない種変数の種のデフォルトを Type にし， F :: Type - > Type を得る．種シグネチャを使って， F を種多相に宣言することもできる．
 kp4.hstype family F1 a                -- F1 :: Type -> Type
type family F2 (a :: k)         -- F2 :: forall k. k -> Type
type family F3 a :: k           -- F3 :: forall k. Type -> k
type family F4 (a :: k1) :: k2  -- F4 :: forall k1 k2. k1 -> k2
一般的な原則は以下の通りである．

右辺があるとき，GHCは右辺と整合する最も多相的な種を推論する．例：通常のデータ型とGADT宣言，クラス宣言など．クラス宣言の場合，「右辺」の役割はクラスのメソッドのシグネチャによって行われる．
右辺がないとき，型シグネチャでそうでないと指定されない限り，GHCは引数と結果の種をデフォルトで  Type にする．例：データ族と開いた型族の宣言．

この規則は時折驚くべき結果をもたらす(Trac＃10132を参照)．

 kp5.hsclass C a where    -- Class declarations are generalised
                   -- so C :: forall k. k -> Constraint
  data D1 a        -- No right hand side for these two family
  type F1 a        -- declarations, but the class forces (a :: k)
                   -- so   D1, F1 :: forall k. k -> Type

data D2 a   -- No right-hand side so D2 :: Type -> Type
type F2 a   -- No right-hand side so F2 :: Type -> Type

クラス宣言からの種多相で D1 は種多相になるが， D2 はそうはならない． F1 と F2 についても同様である．

完全なユーザ指定の種シグネチャと多相再帰
型推論と同様に，再帰型の種推論では単相再帰のみ使用できる．次の(わざとらしい)例を考えてみよう．
 kp6.hsdata T m a = MkT (m a) (T Maybe (m a))
-- GHC infers kind  T :: (Type -> Type) -> Type -> Type
Tを再帰的に使用すると，2番目の引数は Type 種に強制される．ただし，型推論の場合と同様に， T に完全なユーザ指定の種シグネチャ(complete user-supplied kind signature, CUSK)を与えることで，多相再帰を実現できる．CUSKとは，推論の必要がない，すべての引数の種と結果の種が分かるようにしたときのことをいう．例えば，
kp7.hsdata T (m :: k -> Type) :: k -> Type where
  MkT :: m a -> T Maybe (m a) -> T m a

完全なユーザ指定の種シグネチャは T の多相的な種を指定し，このシグネチャは再帰的なものも含めて T へのすべての呼び出しに使用される．特に， T の再帰的な使用には Type が使われる．

型コンストラクタの「完全なユーザ指定の種シグネチャ」とは正確には何だろうか？次の形式のことである．
データ型の場合は，すべての型変数に種注釈が付いている必要がある．GADTスタイルの宣言では，(トップレベルの :: がヘッダにある)種シグネチャがあってもよいが，この注釈の有無は，宣言が完全なユーザ指定の種シグネチャを持つかどうかには影響しない(訳注： kp8.hs の例では T1 ,  T2 ,  T3 ,  T5 がトップレベルの種注釈を持っている．しかし，CUSKを持つのは T1  -  T4 なので，注釈の有無とCUSKを持つかどうかは全く関係ないことがわかる)．
kp8.hsdata T1 :: (k -> Type) -> k -> Type       where ...
-- Yes;  T1 :: forall k. (k->Type) -> k -> Type

data T2 (a :: k -> Type) :: k -> Type     where ...
-- Yes;  T2 :: forall k. (k->Type) -> k -> Type

data T3 (a :: k -> Type) (b :: k) :: Type where ...
-- Yes;  T3 :: forall k. (k->Type) -> k -> Type

data T4 (a :: k -> Type) (b :: k)      where ...
-- Yes;  T4 :: forall k. (k->Type) -> k -> Type

data T5 a (b :: k) :: Type             where ...
-- No;  kind is inferred

data T6 a b                         where ...
-- No;  kind is inferred

トップレベルの :: を持つデータ型については， :: の後に導入されたすべての種変数は明示的に量化する必要がある．
kp9.hsdata T1 :: k -> Type            -- No CUSK: `k` is not explicitly quantified
data T2 :: forall k. k -> Type  -- CUSK: `k` is bound explicitly
data T3 :: forall (k :: Type). k -> Type   -- still a CUSK

型クラスの場合は，すべての型変数に種注釈が付いていることが必要である．

型シノニムでは，すべての型変数と結果の型に種注釈を付ける必要がある．
kp10.hstype S1 (a :: k) = (a :: k)    -- Yes   S1 :: forall k. k -> k
type S2 (a :: k) = a           -- No    kind is inferred
type S3 (a :: k) = Proxy a     -- No    kind is inferred

 S2 と S3 においては，右辺の種はかなり明らかであるが，それでも完全なシグネチャを持っているとはみなされない．というのも， シグネチャが検出されるまではいかなる推論もすることができないためである．

関連型を除く開いた型族，またはデータ族の宣言には常にCUSKがある．注釈なしの型変数は， Type 種に初期化される．

kp11.hsdata family D1 a                  -- D1 :: Type -> Type
data family D2 (a :: k)           -- D2 :: forall k. k -> Type
data family D3 (a :: k) :: Type   -- D3 :: forall k. k -> Type
type family S1 a :: k -> Type     -- S1 :: forall k. Type -> k -> Type

関連型またはデータ族の宣言は，それを囲むクラス(訳注：関連型，関連データ族が定義されている型クラスのこと)がCUSKを持っていれば，そしてそのときに限り，CUSKを持つ．

kp12.hsclass C a where                -- no CUSK
  type AT a b                  -- no CUSK, b is defaulted

class D (a :: k) where         -- yes CUSK
  type AT2 a b                 -- yes CUSK, b is defaulted

閉じた型族は，そのすべての型変数に注釈が付けられ，(トップレベル :: を持つ)返り種が指定されている場合，完全なユーザ指定の種シグネチャを持つ．

構文的には(上記の規則によれば)CUSKを持つが，何らかの推論を必要とするデータ型を書くことは可能である．非常にわざとらしい例として，次の例を考えよう．

kp13.hsdata Proxy a           -- Proxy :: forall k. k -> Type
data X (a :: Proxy k)

上記の規則によると， X にはCUSKがある．しかし， k の種は未定である．これは，ゆえに量化され直され， X に forall k1 (k :: k1). Proxy k -> Type という種を与える．


閉じた型族における種推論
すべての開いた型族は完全なユーザ指定の種シグネチャを持つと見なされるが，閉じた型族の場合，(訳注：型インスタンスに対応する部分の)等式上で種推論を行うことができるので，この条件を緩和することができる．GHCは，閉じた型族の引数と結果の型の種を推論する(訳注：等式上で推論できるのは，閉じた型族はあとからインスタンスが追加されないため)．

GHCは，種上の族としても型上の族としても適するような種添字付き型族をサポートする(訳注：種添字付け型族は，定義された族が返すものが型でも種でも整合性をもつということ．これはGHCでは種と型がほぼ同等に扱われているためである)．GHCは，完全なユーザ指定の種類シグネチャがないと，まれに主要ではない型を推論するかもしれないので，この動作を推論しない．確かに，種添字付けは多相再帰の形式として見ることができる．そこでは，型はそれ自身の定義で最も一般的なもの以外の種で使われる．例えば以下の例がある．
(訳注：主要型(principal type)とは，型システムにおける，その条件下で導き出される最も一般的な型のこと．詳しくは型システム入門を読もう！)

kp14.hstype family F1 a where
  F1 True  = False
  F1 False = True
  F1 x     = x
-- F1 fails to compile: kind-indexing is not inferred

type family F2 (a :: k) where
  F2 True  = False
  F2 False = True
  F2 x     = x
-- F2 fails to compile: no complete signature

type family F3 (a :: k) :: k where
  F3 True  = False
  F3 False = True
  F3 x     = x
-- OK

クラスインスタンス宣言における種推論
次の多層的な種付き型クラスとそのインスタンスの例を考えてみよう．
 kp15.hsclass C a where
  type F a

instance C b where
  type F b = b -> b
型クラス宣言では，型 a の種を制限するものは何もないので，多相的な種付き型変数 (a :: k) になる．しかし，インスタンス宣言では，関連型のインスタンスの右辺の b -> b は， b は Type 種でなければならないことを示している．GHCは理論的には，この情報をインスタンス宣言の先頭に伝播し，そのインスタンスの宣言を，任意の種の型とは対照的に， Type 種の型にのみ適用することもできよう．しかし，GHCはこれをしない．

一言で言えば，GHCはクラスインスタンス宣言のメンバからインスタンス宣言の先頭に種の情報を伝播しない．

このような種推論の欠如は，単にGHC内の技術的な問題だが，それを機能させることは推論基盤にかなりの変更を加えることになり，そこまでするほどその見返りに価値があるかは明らかではない．上記のインスタンスで b の種を制限したい場合は，インスタンス宣言先頭に種シグネチャをつけること．

型シグネチャにおける種推論
型の種検査をするとき，GHCはその型の種を一般化する方法を見つけ出すときに，その型に書かれているものだけを考慮する．

例えば，次の定義を考えてみよう( ScopedTypeVariables 拡張を使用している)．
 kp16.hsdata Proxy a    -- Proxy :: forall k. k -> Type
p :: forall a. Proxy a
p = Proxy :: Proxy (a :: Type)
GHCはエラーを吐き， a の種は Type ではなく種変数 k であるべきだと言ってくる．これは，型シグネチャ forall a. Proxy a を見て，GHCは a の種が一般化されるべきで Type 種に制限されるべきではないと見なすからである．そしてその後，関数定義はその型シグネチャよりも具体的であるとして拒否される．

明示的な種の量化
 PolyKinds によって有効になる機能だが，GHCは以下のように明示的な種の量化をサポートする．
 kp17.hsdata Proxy :: forall k. k -> Type
f :: (forall k (a :: k). Proxy a -> ()) -> Int
二つ目の例は， k の種と型変数 a の種 k の両方を束縛している forall があることに注意せよ．一般に，この種の依存関係がどれだけ深くネストされた状態で機能するかの制限はない．ただし，依存関係はwell-scopedでなけらばならない．例えば， forall (a :: k) k . ... はエラーである．

後方互換性のために，型が forall で始まっていても，種変数は明示的に束縛される必要はない．

したがって，より高階の文脈における種の量化の規則はわずかに変更されている．GHC 7では，トップレベル以外の forall で束縛された変数の種の中で，種変数が初めて言及された場合，その種変数もそこで束縛されていた．つまり， f :: (forall (a :: k). ...) -> ...  では， k は a と同じ forall で束縛されていた．しかしGHC 8では，型の中で言及されているすべての種変数は最も外側のレベルで束縛されている．より高階の forall で束縛したいならば，それを明示的に含めなくてはならない．

種添字付きGADT
以下の型を考えてみよう．

kp18.hsdata G (a :: k) where
  GInt    :: G Int
  GMaybe  :: G Maybe

このデータ型 G は，その種と型の両方においてGADTに似ている． a :: k として g :: G a があるとしよう．そして，パターンマッチすることで g が実は GMaybe であったということを発見することによって， k ~ (Type -> Type) であることと a ~ Maybe  であることを知ることになる． G の定義には PolyKinds が有効であることを必要とするが， G に対してパターンマッチするにはGADTを超えた拡張を必要としない．これが機能するのは，実は通常のGADTを単純に拡張したものであり，種と型が同じという事実の結果である．

データ型 G はその本体内で複数の種で使用されていること，そしてその結果として種添字付きGADTは多相再帰の形式を使用していることに留意せよ．したがって，この機能を使用できるのは，データ型に対して完全なユーザー指定の種シグネチャ(完全なユーザー指定の種シグネチャと多相再帰)を指定した場合に限られる．

高ランク種
 RankNTypes と連携して，GHCはより高階の種をサポートする．一例は以下の通りである．

kp19.hs-- Heterogeneous propositional equality
data (a :: k1) :~~: (b :: k2) where
  HRefl :: a :~~: a

class HTestEquality (t :: forall k. k -> Type) where
  hTestEquality :: forall k1 k2 (a :: k1) (b :: k2). t a -> t b -> Maybe (a :~~: b)

 hTestEquality は，型変数 t に適用される型を持つ2つの引数を取り，それらの種が異なることに留意せよ．その型変数は，ゆえに多相的な種である必要がある．従って， HTestEquality (クラス)の種は (forall k. k -> Type) -> Constraint であり，これは高階の種である．

高階の種と高階の型の大きな違いとして，高階の種では forall を移動させることができないというのがある．これは例を示すのが最良の説明である． (:~~:) に対する HTestEquality のインスタンスを作成したいとしよう．

kp20.hsinstance HTestEquality ((:~~:) a) where
  hTestEquality HRefl HRefl = Just HRefl

上記のように (:~~:) を宣言したことにより， (:~~:) は種 forall k1 k2. k1 -> k2 -> Type を得る．ゆえに，型 (:~~:) a は，何らかの k2 に対して，種 k2 -> Type を持つ．そしてその後に(お望みのとおりに)この種を再び一般化して forall k2. k2 -> Type にすることは，GHCにはできない．したがって，インスタンスはill-kindedとして拒否される．

そのようなインスタンスを可能にするためには， (:~~:) を次のように定義する必要があるだろう．

kp21.hsdata (:~~:) :: forall k1. k1 -> forall k2. k2 -> Type where
  HRefl :: a :~~: a

この再定義では， (:~~:) に明示的な種を与え，最初の引数( a )が与えられるまで k2 の選択が延期される．この (:~~:) の宣言では，(訳注：kp20.hsの) HTestEquality のインスタンスが受け入れられる．

高階の種と型の間のもう1つの違いは，推論された型変数およびユーザ指定の型変数の扱いにある．次のプログラムを考えよう．

kp22.hsnewtype Foo (f :: forall k. k -> Type) = MkFoo (f Int)
data Proxy a = Proxy

foo :: Foo Proxy
foo = MkFoo Proxy

 Foo のパラメータの種は forall k. k -> Type だが， Proxy の種は forall {k}. k -> Type である(ここで {k} は，種変数 k は推論されるものであって，ユーザによって指定されるものではないことを表している)(「推論される」と「指定される」の区別の詳細については，Visible type applicationを参照せよ)．GHCは forall k. k -> Type  と  forall {k}. k -> Type を種レベルで同一であるとは考えないため， Foo Proxy をill-kindedとして拒否する．

種における制約
種と型は同じであるため，種には( PolyKinds を使用する場合)型制約を含めることができる．ただし，現在サポートされているのは等価制約のみである．将来的には他の制約も使用できるようになると考えられる．

次は制約付きの種の例である．
 kp23.hstype family IsTypeLit a where
  IsTypeLit Nat    = 'True
  IsTypeLit Symbol = 'True
  IsTypeLit a      = 'False

data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where
  MkNat    :: T 42
  MkSymbol :: T "Don't panic!"
上記の宣言は許される．しかし， MkOther :: T Int を追加すると， Int は型リテラルではないので，等価制約が満たされないというエラーが発生する．ここで， forall a を使用して明示的に量化する必要はないことに注意せよ．

Type種
StarIsType
8.6.1以降
修飾されていない * 型演算子の使用は，nullaryな（引数を取らない）演算子として扱われ， Data.Kind.Type の代用として扱われる．

 Type 種( Data.Kind からインポートされる)は普通の型を分類する．  StarIsType (現在はデフォルトで有効)があれば， * は Type へと脱糖されるが，このレガシー構文を使用することは TypeOperators との衝突を理由に非推奨である．これは★(Unicodeにおける * の変種)にも適用される．

データ型宣言における依存関係の推論
データ型，型クラス，または型族の宣言内の型変数 a が，同じ宣言内の別のそのような変数 k に依存している場合，次の2つの性質が成り立つ必要がある．

宣言の中で， a は k の後に現れなければならない．
 k はその宣言内のなんらかの型変数の種の中で明示的に現れなければならない．

最初の条件は，単に依存関係の範囲が厳密(well-scoped)でなければならないことを意味している．2番目の条件は，依存関係を推論するGHCの能力に関するものである．この依存関係を推論することは困難であり，GHCは現在依存関係を明示的にすることを要求している．つまり， k は型変数の中に現れなければならないということである．例えば，
kp24.hsdata Proxy k (a :: k)            -- OK: dependency is "obvious"
data Proxy2 k a = P (Proxy k a)  -- ERROR: dependency is unclear

2番目の宣言では，GHCは k が従属変数であるべきだとすぐに言うことはできないので，宣言は拒否される．

この制限が将来緩和される可能性はあるが，この状況を取り巻く問題が理論的なものか(この依存関係を推論することは私たちの型システムに主要型がないことを意味する)それとも単なる実用上のものなのか(GHCの実装を考えると，この依存関係を推論するのは難しい)は(この文書が書かれている現在では)明らかでない．故に，GHCは簡単な方法を取り，ユーザからの少しの助けを必要とするのである．

ユーザ記述のforall下での依存関係の推論
プログラマは，新しい量化された型変数を導入するために型内で forall を使用することができる．これらの変数は変数同士が依存していてもよく，同じ forall の中でさえこれは許される．しかし，GHCは，依存関係が forall の本体から推論可能であることを要求する．以下がいくつかの例である．

kp25.hsdata Proxy k (a :: k) = MkProxy   -- just to use below

f :: forall k a. Proxy k a        -- This is just fine. We see that (a :: k).
f = undefined

g :: Proxy k a -> ()              -- This is to use below.
g = undefined

data Sing a
h :: forall k a. Sing k -> Sing a -> ()  -- No obvious relationship between k and a
h _ _ = g (MkProxy :: Proxy k a)  -- This fails. We didn't know that a should have kind k.

最後の例では， a が forall の本体(つまり， Sing k -> Sing a -> （） )から k に依存していることを知ることは不可能である．故にGHCはそのプログラムを拒否する．

PolyKindsを使わない場合の種のデフォルト
 PolyKinds がなければ，GHCは種変数について一般化することを拒否する．したがって，可能であれば，型変数のデフォルトは Type になり，これが不可能な場合は，エラーが出される．

例は以下の通りである．

kp26.hs{-# LANGUAGE PolyKinds #-}
import Data.Kind (Type)
data Proxy a = P   -- inferred kind: Proxy :: k -> Type
data Compose f g x = MkCompose (f (g x))
  -- inferred kind: Compose :: (b -> Type) -> (a -> b) -> a -> Type

-- separate module having imported the first
{-# LANGUAGE NoPolyKinds, DataKinds #-}
z = Proxy :: Proxy 'MkCompose

最後の行では，我々は昇格されたコンストラクタ 'MkCompose を使っている． 'MkCompose の種は次のとおりである．

kp27.hsforall (a :: Type) (b :: Type) (f :: b -> Type) (g :: a -> b) (x :: a).
  f (g x) -> Compose f g x

今度は z の型を推論しなければならない．種変数を一般化せずにそれを行うには， 'MkCompose の種変数をデフォルトする必要がある．簡単に a や b を Type にデフォルトすることができるが， f と g はデフォルトするとill-kindedになってしまう．したがって z の定義はエラーである．

種多相の存在下でのプリティプリンティング
種多相では，Haskellプログラマには見えないかもしれない舞台裏でかなりのことが起こっている．GHCは，エラーメッセージとGHCiプロンプトで型をどのように表示するかを制御するいくつかのフラグをサポートしている．詳細はtype pretty-printingオプションの議論 を参照せよ．もしあなたが種多相を使っていて，なぜGHCがあなたのプログラムを拒絶する(あるいは受け入れる)のかについて混乱しているなら，これらのフラグ，特に -fprint-explicit-kinds を有効にすることを推奨する．