字句的スコープを持つ型変数
ScopedTypeVariables
ExplicitForAllを含む
6.8.1以降
forallで明示的に導入された型変数の字句的スコープを有効にする.
Tip
ScopedTypeVariablesは,明示的な forallはオプションでありセマンティクスに影響を与えないというGHCの通常の規則を破る.この節の宣言の型シグネチャ (または式の型シグネチャ)の例は,明示的なforallが必要である.(省略した場合,通常,プログラムはコンパイルを通らない.いくつかの場合ではコンパイルされるが,関数が意図しない型シグネチャを持つことになる).これらのScopedTypeVariablesの形式を有効するには, forallはトップレベルシグネチャ(または外部の式)において現れる必要があるが,同じ型変数を参照するネストされたシグネチャに対しては現れる必要はない. 明示的なforallは常に必要というわけではない.詳しくは,この節の例である,[/* pattern-equiv-formとパターンシグネチャの等価性],またはパターン型シグネチャを参照せよ. GHCは字句的スコープを持つ型変数をサポートしており,それなしでは一部の型シグネチャを書くのが全くもって不可能である.例えば,
code:ls01.hs
f xs = ys ++ ys
where
ys = reverse xs
明示的なforallがあるため,fの型シグネチャは型変数aをスコープに入れる(宣言型シグネチャ).forallによって束縛された型変数は、それに伴う値の宣言の全体をスコープに持つ.この例では,型変数aは、fの定義全体をスコープに持ち,特にysの型シグネチャもaのスコープに入っている.Haskell 98では(訳注:このようなfの型変数とaと,ysの型変数aが全く同じであるというような)ysの型を宣言することはできない.スコープ付き型変数の主な利点は,それが可能になることだ.
code:ls02.hs
where
ys = reverse xs
forallの形式とは異なり,fのシグネチャに由来する型変数aはfの定義を構成する式をスコープに持たない.パターンシグネチャによって束縛された型変数aaは,fの定義を構成する式の右辺をスコープに持つ(したがって,異なる型変数を使用する必要はない.aを使用しても同等である).
概要
設計は次の原則に従う.
スコープ付き型変数は,型変数を意味するのであって,型を意味しない(これはかつてのGHCの設計からの変更点である).
さらに,異なった字句的スコープを持つ型変数は異なった型変数を表す.つまり,プログラマが書いた型シグネチャ(自由スコープの型変数を含むものを含む)はすべてrigidな型を表す.rigidな型というのは,型が型検査器に完全に知られており,推論が行われないもののことである.
プログラムを変更することなく,字句型変数を自由にα-renameすることができる.
字句的スコープを持つ型変数は以下のもので束縛できる.
Haskellでは,プログラマが書いた型シグネチャは,その自由な型変数の上で暗黙のうちに量化される(Haskellレポートのセクション4.1.2).字句的スコープを持つ型変数は,この暗黙の量化規則に対して「スコープ内にある型変数は,全称量化されない」という影響を与える.たとえば,型変数aがスコープ内にある場合,
code: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を用いて)明示的に量化された宣言型シグネチャは,名前付き関数の定義において,明示的に量化された型変数をスコープに持ってくる.例えば,
code:ls04.hs
このforall aはfの定義のスコープに型変数aをもたらす.
これが発生するのは,次の条件を全て(訳注: 原文にないけどたぶん「全て」)満たしている場合のみである.
fの型シグネチャの量化が明示的であること.例えば,
code:ls05.hs
aはgの定義のスコープをもたないため,x :: aはHaskellの通常の暗黙の量化規則に基づいてx :: forall a. aを意味する.ゆえにこのプログラムは拒否される.
型変数が,型シグネチャ内の,単一の,構文上明記された,最も外側のforallによって量化されていること.たとえば,GHCは以下の例をすべて拒否する.
code:ls06.hs
f1 :: forall a. forall b. a -> b -> b f2 :: forall a. a -> forall b. b -> b type Foo = forall b. b -> b f3 :: Foo
f1とf2では、型変数bは最も外側のforallに量化されているわけではないので、関数の本体のスコープに入らない.forallがFoo型シノニムの下に隠れているので,f3においてもbはf3の本体のスコープにない.
シグネチャが関数束縛または裸の変数束縛に対して型を与えているのであって,パターン束縛に対して与えているのではないこと.例えば,
code:ls07.hs
f1 (x:xs) = xs ++ x :: a -- OK f2 = \(x:xs) -> xs ++ x :: a -- OK Just f3 = Just (\(x:xs) -> xs ++ x :: a ) -- Not OK! f1は関数束縛で, f2は裸の変数を束縛する.両方の場合において,型シグネチャはaをスコープにもたらす.しかし,f3の束縛はパターン束縛なので, f3はパターンによってスコープ内に取り込まれた新しい変数であり,トップレベルのf3とは関係ない.その場合,型変数aは Just f3 = ...の右辺のスコープにない.
式の型シグネチャ
明示的に量化された式(forallを使用)を持つ,式の型シグネチャは,注釈が付いた式の中で明示的に量化された型変数をスコープに入れる.例えば,
code: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をスコープにもたらす.
パターン型シグネチャ
型シグネチャは任意のパターンで出現することが許される.これをパターン型シグネチャという.例えば,
code: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)
パターン型シグネチャのすべての型変数がすでにスコープ内にある(つまり,それを囲む文脈(訳注:おそらく型付け文脈)によって束縛されている)場合,問題は単純だ.シグネチャは,自明な方法でパターンの型を強制するだけである.
式および宣言の型シグネチャとは異なり,パターン型シグネチャは暗黙的に一般化されない.パターン束縛の中のパターンは,すでにスコープ内にある型変数にしか言及できない.例えば,
code:ls10.hs
f :: forall a. a -> (Int, a) f xs = (n, zs)
where
(ys::a, n) = (reverse xs, length xs) -- OK Just (v::b) = ... -- Not OK; b is not in scope
ここで、ysとzsのパターンシグネチャは問題ないが、vのシグネチャはbがスコープにないため問題がある.
しかし,パターン束縛以外のパターンの中では,パターン型シグネチャは,スコープ内にない型変数に言及できる.この場合,シグネチャはその型変数をスコープに入れる.例えば,
code: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
パターン型シグネチャが,式の右辺で型変数を使用可能にする.
型変数をスコープに入れることは,存在量化されたデータコンストラクタにとって特に重要である.例えば,
code:ls12.hs
k :: T -> T
MkT t3
where
ここで,パターン型シグネチャ[t :: a]は,まだスコープに含まれていない字句的型変数(訳注:字句的スコープを持つ型変数のこと)について言及している.実際は,それはパターンマッチによって束縛されているので,それがもうスコープ内にあってはいけないのである.パターン型シグネチャの効果は,存在的に束縛された型変数の代わりにそれ(=まだスコープに含まれていない字句型変数)をスコープ内に持ってくることである.
パターン型シグネチャがこのように型変数を束縛するとき,GHCはその型変数がrigidな型変数,別の言い方をすれば,完全に知っている型変数に束縛されることを要求する.つまり,ユーザ定義の型シグネチャは常に完全に既知の型を表す.
存在的に束縛された型変数が既にスコープ内にあってはならないことは奇妙に思える.通常,名前束縛は,同じ名前の外部変数のスコープ内で単にシャドウイング(「穴」を作る)するだけだということと比較してみよう.しかし,そのような型変数をスコープに持ってくるための何らかの方法がなければならない.さもなくばその後の型シグネチャで存在的に束縛された型変数に名前を付けることができないからである(訳注: 「ので,このような奇妙な仕様はしかたないのである.」ということ).
例のfとgの2つの(同一の)定義を比較してみよう.aがすでにスコープにあるかどうかにかかわらず,どちらも合法である.相違点は,もしaが既にスコープにあるならば,型シグネチャはパターンを強制するのであって,変数をパターン束縛するのではないという点である.
クラスとインスタンスの宣言
class宣言またはinstance宣言の先頭にある型変数は、where部分で定義されているメソッドのスコープ内にある.明示的なforallすら必要ない(とはいえ,instance宣言では明示的なforallを使用できるが.「明示的な全称量化(forall)」を参照せよ).例えば,
code:ls13.hs
class C a where
ys = reverse xs
in
head ys
instance C b => C b where op xs = reverse (head (xs :: b))