字句的スコープを持つ型変数
ScopedTypeVariables
ExplicitForAllを含む
6.8.1以降
forall
で明示的に導入された型変数の字句的スコープを有効にする.
Tip
ScopedTypeVariables
は,明示的な
forall
はオプションでありセマンティクスに影響を与えないというGHCの通常の規則を破る.この節の
宣言の型シグネチャ (または
式の型シグネチャ)の例は,明示的な
forall
が必要である.(省略した場合,通常,プログラムはコンパイルを通らない.いくつかの場合ではコンパイルされるが,関数が意図しない型シグネチャを持つことになる).これらの
ScopedTypeVariables
の形式を有効するには,
forall
はトップレベルシグネチャ(または外部の式)において現れる必要があるが,同じ型変数を参照するネストされたシグネチャに対しては現れる必要はない.
明示的な
forall
は常に必要というわけではない.詳しくは,この節の例である,[/*
pattern-equiv-form
とパターンシグネチャの等価性],または
パターン型シグネチャを参照せよ.
GHCは字句的スコープを持つ型変数をサポートしており,それなしでは一部の型シグネチャを書くのが全くもって不可能である.例えば,
ls01.hsf :: 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
の型を宣言することはできない.スコープ付き型変数の主な利点は,それが可能になることだ.
ls02.hsf :: [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.hsf :: forall a. [a] -> [a]
f (x:xs) = xs ++ [ x :: a ]
この forall a
は f
の定義のスコープに型変数 a
をもたらす.
これが発生するのは,次の条件を全て(訳注: 原文にないけどたぶん「全て」)満たしている場合のみである.
f
の型シグネチャの量化が明示的であること.例えば,
ls05.hsg :: [a] -> [a]
g (x:xs) = xs ++ [ x :: a ]
a
は g
の定義のスコープをもたないため, x :: a
はHaskellの通常の暗黙の量化規則に基づいて x :: forall a. a
を意味する.ゆえにこのプログラムは拒否される.
型変数が,型シグネチャ内の,単一の,構文上明記された,最も外側の forall
によって量化されていること.たとえば,GHCは以下の例をすべて拒否する.
ls06.hsf1 :: 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.hsf1 :: 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.hsf = 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.hsf :: 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.hsdata 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.hsclass 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]]))