generated at
字句的スコープを持つ型変数

ScopedTypeVariables
ExplicitForAllを含む
6.8.1以降
forall で明示的に導入された型変数の字句的スコープを有効にする.

Tip
ScopedTypeVariables は,明示的な forall はオプションでありセマンティクスに影響を与えないというGHCの通常の規則を破る.この節の宣言の型シグネチャ (または式の型シグネチャ)の例は,明示的な forall が必要である.(省略した場合,通常,プログラムはコンパイルを通らない.いくつかの場合ではコンパイルされるが,関数が意図しない型シグネチャを持つことになる).これらの ScopedTypeVariables の形式を有効するには, forall はトップレベルシグネチャ(または外部の式)において現れる必要があるが,同じ型変数を参照するネストされたシグネチャに対しては現れる必要はない.
明示的な forall は常に必要というわけではない.詳しくは,この節の例である,[/* pattern-equiv-form とパターンシグネチャの等価性],またはパターン型シグネチャを参照せよ.

GHCは字句的スコープを持つ型変数をサポートしており,それなしでは一部の型シグネチャを書くのが全くもって不可能である.例えば,

ls01.hs
f :: forall a. [a] -> [a] f xs = ys ++ ys where ys :: [a] ys = reverse xs

明示的な forall があるため, f の型シグネチャは型変数 a をスコープに入れる(宣言型シグネチャ). forall によって束縛された型変数は、それに伴う値の宣言の全体をスコープに持つ.この例では,型変数 a は、 f の定義全体をスコープに持ち,特に ys の型シグネチャも a のスコープに入っている.Haskell 98では(訳注:このような f の型変数と a と, ys の型変数 a が全く同じであるというような) ys の型を宣言することはできない.スコープ付き型変数の主な利点は,それが可能になることだ.

この例と同等の形式で,明示的な forall を回避するには,パターン型シグネチャを使用する.

ls02.hs
f :: [a] -> [a] f (xs :: [aa]) = xs ++ ys where ys :: [aa] ys = reverse xs

forall の形式とは異なり, f のシグネチャに由来する型変数 a f の定義を構成する式をスコープに持たない.パターンシグネチャによって束縛された型変数 aa は, f の定義を構成する式の右辺をスコープに持つ(したがって,異なる型変数を使用する必要はない. a を使用しても同等である).

概要
設計は次の原則に従う.

スコープ付き型変数は,型変数を意味するのであって,を意味しない(これはかつてのGHCの設計からの変更点である).
さらに,異なった字句的スコープを持つ型変数は異なった型変数を表す.つまり,プログラマが書いた型シグネチャ(自由スコープの型変数を含むものを含む)はすべてrigidな型を表す.rigidな型というのは,型が型検査器に完全に知られており,推論が行われないもののことである.
プログラムを変更することなく,字句型変数を自由にα-renameすることができる.

字句的スコープを持つ型変数は以下のもので束縛できる.

宣言の型シグネチャ(宣言の型シグネチャ)
式の型シグネチャ(式の型シグネチャ)
パターン型シグネチャ(パターン型シグネチャ)
クラスとインスタンスの宣言(クラスとインスタンスの宣言)

Haskellでは,プログラマが書いた型シグネチャは,その自由な型変数の上で暗黙のうちに量化される(Haskellレポートのセクション4.1.2).字句的スコープを持つ型変数は,この暗黙の量化規則に対して「スコープ内にある型変数は,全称量化されない」という影響を与える.たとえば,型変数 a がスコープ内にある場合,

ls03.hs
(e :: a -> a) は (e :: a -> a) の意味 (e :: b -> b) は (e :: forall b. b->b) の意味 (e :: a -> b) は (e :: forall b. a->b) の意味


宣言の型シグネチャ
( forall を用いて)明示的に量化された宣言型シグネチャは,名前付き関数の定義において,明示的に量化された型変数をスコープに持ってくる.例えば,

ls04.hs
f :: forall a. [a] -> [a] f (x:xs) = xs ++ [ x :: a ]

この forall a f の定義のスコープに型変数 a をもたらす.

これが発生するのは,次の条件を全て(訳注: 原文にないけどたぶん「全て」)満たしている場合のみである.

f の型シグネチャの量化が明示的であること.例えば,
ls05.hs
g :: [a] -> [a] g (x:xs) = xs ++ [ x :: a ]
a g の定義のスコープをもたないため, x :: a はHaskellの通常の暗黙の量化規則に基づいて x :: forall a. a を意味する.ゆえにこのプログラムは拒否される.

型変数が,型シグネチャ内の,単一の,構文上明記された,最も外側の forall によって量化されていること.たとえば,GHCは以下の例をすべて拒否する.
ls06.hs
f1 :: forall a. forall b. a -> [b] -> [b] f1 _ (x:xs) = xs ++ [ x :: b ] f2 :: forall a. a -> forall b. [b] -> [b] f2 _ (x:xs) = xs ++ [ x :: b ] type Foo = forall b. [b] -> [b] f3 :: Foo f3 (x:xs) = xs ++ [ x :: b ]

f1 f2 では、型変数 b は最も外側の forall に量化されているわけではないので、関数の本体のスコープに入らない. forall Foo 型シノニムの下に隠れているので, f3 においても b f3 の本体のスコープにない.

シグネチャが関数束縛または裸の変数束縛に対して型を与えているのであって,パターン束縛に対して与えているのではないこと.例えば,
ls07.hs
f1 :: forall a. [a] -> [a] f1 (x:xs) = xs ++ [ x :: a ] -- OK f2 :: forall a. [a] -> [a] f2 = \(x:xs) -> xs ++ [ x :: a ] -- OK f3 :: forall a. [a] -> [a] Just f3 = Just (\(x:xs) -> xs ++ [ x :: a ]) -- Not OK!

f1 は関数束縛で, f2 は裸の変数を束縛する.両方の場合において,型シグネチャは a をスコープにもたらす.しかし, f3 の束縛はパターン束縛なので, f3 はパターンによってスコープ内に取り込まれた新しい変数であり,トップレベルの f3 とは関係ない.その場合,型変数 a Just f3 = ... の右辺のスコープにない.

式の型シグネチャ
明示的に量化された式( forall を使用)を持つ,式の型シグネチャは,注釈が付いた式の中で明示的に量化された型変数をスコープに入れる.例えば,

ls08.hs
f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool )

ここでは,注釈が付いた式 (op >>= \(x :: STRef s Int) -> g x) では,型シグネチャ forall s. ST s Bool が型変数 s をスコープにもたらす.

パターン型シグネチャ
型シグネチャは任意のパターンで出現することが許される.これをパターン型シグネチャという.例えば,

ls09.hs
-- f and g assume that 'a' is already in scope f = \(x::Int, y::a) -> x g (x::a) = x h ((x,y) :: (Int,Bool)) = (y,x)

パターン型シグネチャのすべての型変数がすでにスコープ内にある(つまり,それを囲む文脈(訳注:おそらく型付け文脈)によって束縛されている)場合,問題は単純だ.シグネチャは,自明な方法でパターンの型を強制するだけである.

式および宣言の型シグネチャとは異なり,パターン型シグネチャは暗黙的に一般化されない.パターン束縛の中のパターンは,すでにスコープ内にある型変数にしか言及できない.例えば,

ls10.hs
f :: forall a. [a] -> (Int, [a]) f xs = (n, zs) where (ys::[a], n) = (reverse xs, length xs) -- OK (zs::[a]) = xs ++ ys -- OK Just (v::b) = ... -- Not OK; b is not in scope

ここで、 ys zs のパターンシグネチャは問題ないが、 v のシグネチャは b がスコープにないため問題がある.

しかし,パターン束縛以外のパターンの中では,パターン型シグネチャは,スコープ内にない型変数に言及できる.この場合,シグネチャはその型変数をスコープに入れる.例えば,

ls11.hs
-- same f and g as above, now assuming that 'a' is not already in scope f = \(x::Int, y::a) -> x -- 'a' is in scope on RHS of -> g (x::a) = x :: a hh (Just (v :: b)) = v :: b

パターン型シグネチャが,式の右辺で型変数を使用可能にする.

型変数をスコープに入れることは,存在量化されたデータコンストラクタにとって特に重要である.例えば,

ls12.hs
data T = forall a. MkT [a] k :: T -> T k (MkT [t::a]) = MkT t3 where (t3::[a]) = [t,t,t]

ここで,パターン型シグネチャ [t :: a] は,まだスコープに含まれていない字句的型変数(訳注:字句的スコープを持つ型変数のこと)について言及している.実際は,それはパターンマッチによって束縛されているので,それがもうスコープ内にあってはいけないのである.パターン型シグネチャの効果は,存在的に束縛された型変数の代わりにそれ(=まだスコープに含まれていない字句型変数)をスコープ内に持ってくることである.

パターン型シグネチャがこのように型変数を束縛するとき,GHCはその型変数がrigidな型変数,別の言い方をすれば,完全に知っている型変数に束縛されることを要求する.つまり,ユーザ定義の型シグネチャは常に完全に既知の型を表す.

存在的に束縛された型変数が既にスコープ内にあってはならないことは奇妙に思える.通常,名前束縛は,同じ名前の外部変数のスコープ内で単にシャドウイング(「穴」を作る)するだけだということと比較してみよう.しかし,そのような型変数をスコープに持ってくるための何らかの方法がなければならない.さもなくばその後の型シグネチャで存在的に束縛された型変数に名前を付けることができないからである(訳注: 「ので,このような奇妙な仕様はしかたないのである.」ということ).

例の f g の2つの(同一の)定義を比較してみよう. a がすでにスコープにあるかどうかにかかわらず,どちらも合法である.相違点は,もし a が既にスコープにあるならば,型シグネチャはパターンを強制するのであって,変数をパターン束縛するのではないという点である.

クラスとインスタンスの宣言
class 宣言または instance 宣言の先頭にある型変数は、 where 部分で定義されているメソッドのスコープ内にある.明示的な forall すら必要ない(とはいえ, instance 宣言では明示的な forall を使用できるが.「明示的な全称量化( forall )」を参照せよ).例えば,
ls13.hs
class C a where op :: [a] -> a op xs = let ys::[a] ys = reverse xs in head ys instance C b => C [b] where op xs = reverse (head (xs :: [[b]]))