利用者:Foxtrot/翻訳/Haskell/存在量化された型

Existential types, or 'existentials' for short, are a way of 'squashing' a group of types into one, single type.

存在型 (Existential types もしくは短く existentials) は型の集合をひとつの型へと圧縮する方法である。

Firstly, a note to those of you following along at home: existentials are part of GHC's type system extensions. They aren't part of Haskell98, and as such you'll have to either compile any code that contains them with an extra command-line parameter of -XExistentialQuantification, or put {-# LANGUAGE ExistentialQuantification #-} at the top of your sources that use existentials.

最初に注意してくことがある。 存在型は GHC の 型システム拡張 の一部である。これらは Haskell98 の一部ではなく、-XExistentialQuantification という追加のコマンドライン引数をつけるか、{-# LANGUAGE ExistentialQuantification #-} をソースコードの先頭に置くかして、コンパイルしなければならないだろう。

The forall keyword forall キーワード

The forall keyword is used to explicitly bring type variables into scope. For example, consider something you've innocuously seen written a hundred times so far:

forall キーワードは明示的に型変数をスコープに持ってくるのに使われる。たとえば、これまで次のように書かれているのは何度も飽きるほど見てきただろう。

Example: A polymorphic function 多相関数

map :: (a -> b) -> [a] -> [b]

But what are these a and b? Well, they're type variables, you answer. The compiler sees that they begin with a lowercase letter and as such allows any type to fill that role. Another way of putting this is that those variables are 'universally quantified'. If you've studied formal logic, you will have undoubtedly come across the quantifiers: 'for all' (or $\forall$) and 'exists' (or $\exists$). They 'quantify' whatever comes after them: for example, $\exists x$ means that whatever follows is true for at least one value of x. $\forall x$ means that what follows is true for every x you could imagine. For example, $\forall x,\,x^{2}\geq 0$ and $\exists x,\,x^{3}=27$.

しかし、これらの a と b は何なのだろうか？まあ、これらは型変数だ、とあなたは答えるだろう。コンパイラは、小文字から始まる型名を見ると、その役割を埋めるためにどんな型も許容するものとみなす。これらの変数を '全称量化された' (universally quantified) するという方法もある。もし形式論理を学べば、量化子に出くわすに違いない。'任意の～について' (for all、$\forall$) と '～が存在する' (exists、 $\exists$)である。これらの '量化' はこれらの後に現れる。たとえば、$\exists x$ は続く　少なくともひとつの値 x について続く命題が真であることを意味する。$\forall x$ は想定されうるすべての x について続く命題が真であることを意味する。たとえば、$\forall x,\,x^{2}\geq 0$ や $\exists x,\,x^{3}=27$ だ。

The forall keyword quantifies types in a similar way. We would rewrite map's type as follows:

同じように、forall キーワードは 型 を量化する。map の型を次のように書きなおすことができる。

Example: Explicitly quantifying the type variables 明示的な型変数の量化

map :: forall a b. (a -> b) -> [a] -> [b]

So we see that for any a and b we can imagine, map takes the type (a -> b) -> [a] -> [b]. For example, we might choose a = Int and b = String. Then it's valid to say that map has the type (Int -> String) -> [Int] -> [String]. We are instantiating the general type of map to a more specific type.

そして、我々が考えるどんな a や b についても、map は map (a -> b) -> [a] -> [b] という型をとることがわかる。たとえば、a = Int と b = String という型を選ぶかもしれない。そして、map は型 (Int -> String) -> [Int] -> [String] をもつというのは妥当だ。map の一般化された型をより具体的な型へと インスタンス化 しているのだ。

However, in Haskell, as we know, any use of a lowercase type implicitly begins with a forall keyword, so the two type declarations for map are equivalent, as are the declarations below:

しかしながら、Haskell では、知っての通り、小文字で始まる型は暗黙的に forall を持つことになっており、つぎで宣言されているような、 map の２つの宣言は同じである。

Example: Two equivalent type statements ふたつの同じ型宣言

id :: a -> a
id :: forall a . a -> a

What makes life really interesting is that you can override this default behaviour by explicitly telling Haskell where the forall keyword goes. One use of this is for building existentially quantified types, also known as existential types, or simply existentials. But wait... isn't forall the universal quantifier? How do you get an existential type out of that? We look at this in a later section. However, first, let's dive right into the deep end by seeing an example of the power of existential types in action.

どこに forall キーワードを置くかによって明示的に Haskell に伝え既定の振る舞いを上書きすることができることは、生活を本当に興味深くしてくれる。使い方のひとつは、存在型( existential types )や単に存在 ( existentials ) ともいう 存在量化された型 ( existentially quantified types ) を構築することである。だがちょっと待ってほしい。forall は 全称 量化子ではないのか？どうやってそこから抜けだして存在型にするのだろうか？これについては後の節で検討するが、まずはアクションで存在型の力の例を見ることによって、その深淵に飛び込んでみようではないか。

Example: heterogeneous lists 例: 異なる型が混合されたリスト

The premise behind Haskell's typeclass system is grouping types that all share a common property. So if you know a type instantiates some class C, you know certain things about that type. For example, Int instantiates Eq, so we know that elements of Int can be compared for equality.

Haskell の型クラスシステムの背後の根拠は、すべての共通の性質を共有する型のグルーピングである。つまり、もしなんらかのクラス C をインスタンス化する型を知っているなら、この型についていくらかわかっていることになる。たとえば、Eq をインスタンス化する Int は、Int の要素は等値性を比較できることを知っている。

Suppose we have a group of values, and we don't know if they are all the same type, but we do know they all instantiate some class, i.e. we know all the values have a certain property. It might be useful to throw all these values into a list. We can't do this normally because lists are homogeneous with respect to types: they can only contain a single type. However, existential types allow us to loosen this requirement by defining a 'type hider' or 'type box':

値の集合があるとして、もしこれらが同じ型であるかどうかを知らなければ、 すなわち、すべての値がある性質を持っていることがわかる。このことはこれらすべての値をリストに入れるために役に立つかもしれない。リストは型については単一であり、通常はこのようなことはできない。ただひとつの型を格納することだけができる。しかしながら、'type hider' や 'type box' とも呼ばれるものを定義することによって、この条件を緩めるのを存在型は可能にする。

Example: Constructing a heterogeneous list 統一されていない型を格納するリスト(heterogeneous list)の構築

 data ShowBox = forall s. Show s => SB s
 
 heteroList :: [ShowBox]
 heteroList = [SB (), SB 5, SB True]

We won't explain precisely what we mean by that datatype definition, but its meaning should be clear to your intuition. The important thing is that we're calling the constructor on three values of different types, and we place them all into a list, so we must end up with the same type for each one. Essentially this is because our use of the forall keyword gives our constructor the type SB :: forall s. Show s => s -> ShowBox. If we were now writing a function to which we intend to pass heteroList, we couldn't apply any functions like not to the values inside the SB because they might not be Bools. But we do know something about each of the elements: they can be converted to a string via show. In fact, that's pretty much the only thing we know about them.

このデータ型の定義が何を意味するかを詳しく説明するつもりはないが、この意味は直感的に明らかだろう。重要なのは、３つの異なる型の値に対して構築子を呼び出していて、すべてリストの中に置いていることだ。それぞれが結果的に同じ型になったはずである。本質的に、forall キーワードの使用はこれらの構築子 SB :: forall s. Show s => s -> ShowBox を与えたことになるからである。heteroList を渡すつもりの関数を書いているならば、Bool でないかもしれないので not のようなどんな関数も適用できないだろう。だが、これらの値のそれぞれについてわかっていることがある。show を通じて文字列に変換することができることだ。実際、わかっていることはこれがほとんどすべてである。

Example: Using our heterogeneous list 統一されていない型を格納するリストの使用

 instance Show ShowBox where
  show (SB s) = show s        -- (*) see the comment in the text below
 
 f :: [ShowBox] -> IO ()
 f xs = mapM_ print xs

 main = f heteroList

Let's expand on this a bit more. In the definition of show for ShowBox – the line marked with (*) see the comment in the text below – we don't know the type of s. But as we mentioned, we do know that the type is an instance of Show due to the constraint on the SB constructor. Therefore, it's legal to use the function show on s, as seen in the right-hand side of the function definition.

もうちょっとだけ踏み込んでみよう。ShowBox に対する show の定義――(*) see the comment in the text below とつけられた行――において、s の型はわからない。しかし先ほど述べたとおり、SB 構築子の制約によってその型が Show のインスタンスであることならわかる。それゆえ、この関数定義の右辺にみられるように、s に対して関数 show を使うことは妥当なのである。

As for f, recall the type of print:

f に関しては、print の型を思い出そう。

Example: Types of the functions involved 複雑な関数の型

 print :: Show s => s -> IO () -- print x = putStrLn (show x)
 mapM_ :: (a -> m b) -> [a] -> m ()
 mapM_ print :: Show s => [s] -> IO ()

As we just declared ShowBox an instance of Show, we can print the values in the list.

ShowBox は Show のインスタンスであると定義しただけで、リストの値を出力できる。

Explaining the term existential 存在 という言葉の説明

Let's get back to the question we asked ourselves a couple of sections back. Why are we calling these existential types if forall is the universal quantifier?

先ほどの疑問に戻ろう。forall が全称量化子ならば、なぜ存在型と呼ぶのだろうか？

Firstly, forall really does mean 'for all'. One way of thinking about types is as sets of values with that type, for example, Bool is the set {True, False, ⊥} (remember that bottom, ⊥, is a member of every type!), Integer is the set of integers (and bottom), String is the set of all possible strings (and bottom), and so on. forall serves as an intersection over those sets. For example, forall a. a is the intersection over all types, which must be {⊥}, that is, the type (i.e. set) whose only value (i.e. element) is bottom. Why? Think about it: how many of the elements of Bool appear in, for example, String? Bottom is the only value common to all types.

まず、forall は本当に '任意の～について' (for all) を意味する。型についての考え方として、その型の値の集合だと考えることができる。たとえば、Bool は集合 {True, False, ⊥} (ボトム ⊥ はいかなる型のメンバでもあることを思い出そう！)であり、Integer は整数(とボトム)の集合だし、String は可能なあらゆる文字列(とボトム)の集合などなど。forall はこれらの集合の共通集合を与える。たとえば、forall a. a はすべての型の共通部分であり、{⊥} のはずである。これは値(つまり要素)がボトムだけであるような型(つまり集合だ)である。なぜだろうか？考えてみよう。Bool に現れる要素はいくつだろうか？たとえば文字列は？ボトムはすべての型に共通する唯一の値だ。

A few more examples:

さらにいくつか例を挙げる。

1. [forall a. a] is the type of a list whose elements all have the type forall a. a, i.e. a list of bottoms. [forall a. a] はすべて型 forall a. a を持つ要素のリスト、つまりボトムのリストの型だ。
2. [forall a. Show a => a] is the type of a list whose elements all have the type forall a. Show a => a. The Show class constraint limits the sets you intersect over (here we're only intersecting over instances of Show), but $\perp$ is still the only value common to all these types, so this too is a list of bottoms. [forall a. Show a => a] はすべての要素が型 forall a. Show a => a を持つようなリストの型だ。Show クラス制約は集合を制限する(ここでは Show のインスタンスだけの共通集合である)が、まだこれらすべてに共通する値は $\perp$ だけだ。
3. [forall a. Num a => a]. Again, the list where each element is a member of all types that instantiate Num. This could involve numeric literals, which have the type forall a. Num a => a, as well as bottom. [forall a. Num a => a]。再び、それぞれの要素がすべて Num のインスタンスであるような型の要素のリストである。これが含めるのは型 forall a. Num a => a を持つような数値リテラル、つまりまたボトムだけを含む。
4. forall a. [a] is the type of the list whose elements have some (the same) type a, which can be assumed to be any type at all by a callee (and therefore this too is a list of bottoms). forall a. [a] は、とにかく呼び出し側からみなされうる、なんらかの(同じ)型 a が要素であるリストの型である。

We see that most intersections over types just lead to combinations of bottoms in some ways, because types don't have a lot of values in common.

型は多くの値を共通に持つわけではなく、幾つかの方法でだいたいの型の共通集合が結局はボトムの組み合わせになることがわかった。

Recall that in the last section, we developed a heterogeneous list using a 'type hider'. Ideally, we'd like the type of a heterogeneous list to be [exists a. a], i.e. the list where all elements have type exists a. a. This 'exists' keyword (which isn't present in Haskell) is, as you may guess, a union of types, so that [exists a. a] is the type of a list where all elements could take any type at all (and the types of different elements needn't be the same).

さきほどの節で '型の箱' を使って異なる型を格納するリストを作ったこと思い出そう。理想的には、異なる型を格納するリストは [exists a. a]　という型、すなわちすべての要素が型 exists a. a を持つようなリストであるとよい。この 'exists' キーワード(これは Haskell には存在しない)は推測されるように型の 和集合 であり、そして [exists a. a] はすべての要素がどんな型も取れる(かつ異なる要素は同じ型である必要はない)リストの型なのである。

But we got almost the same behaviour above using datatypes. Let's declare one.

しかし、データ型を使ってほとんど同じ振る舞いを得たのだった。これを定義してみよう。

Example: An existential datatype 存在データ型

 data T = forall a. MkT a

This means that:

これは次のようなものを意味する。

Example: The type of our existential constructor 存在型コンストラクタの型

MkT :: forall a. a -> T

So we can pass any type we want to MkT and it'll convert it into a T. So what happens when we deconstruct a MkT value?

そして、MkT に任意の値を渡すことができ、それは T へ変換されるだろう。では、MkT の値を分解 (deconstruct) するとき、何が起きるのだろうか？

Example: Pattern matching on our existential constructor 存在型コンストラクタにおけるパターンマッチング

 foo (MkT x) = ... -- what is the type of x? x の型は何？

As we've just stated, x could be of any type. That means it's a member of some arbitrary type, so has the type x :: exists a. a. In other words, our declaration for T is isomorphic to the following one:

示したように、x はどんな値でもとれる。これは、それがなんらかの任意の型の要素であることを意味し、型 x :: exists a. a を持つ。言い換えれば、この T の定義は次のように統一された (isomorphic) 型なのである。

Example: An equivalent version of our existential datatype (pseudo-Haskell) この存在型データ型と等価なバージョン(擬似 Haskell)

 data T = MkT (exists a. a)

And suddenly we have existential types. Now we can make a heterogeneous list:

そして突然存在型が現れた。いま、不統一 (heterogeneous) リストを作ることができる。

Example: Constructing the hetereogeneous list 不統一 (heterogeneous) リストの構築

 heteroList = [MkT 5, MkT (), MkT True, MkT map]

Of course, when we pattern match on heteroList we can't do anything with its elements, as all we know is that they have some arbitrary type. However, if we are to introduce class constraints:

もちろん、heteroList をパターンマッチしたとき、知っているのはそれがなんらかの任意の型であることだけなので、その要素に対して何もすることはできない。しかしながら、もしクラス制約を導入すれば、

Example: A new existential datatype, with a class constraint クラス制約を伴う新しい存在型データ型

 data T' = forall a. Show a => MkT' a

Which is isomorphic to:

これ統一された (isomorphic) 型である。

Example: The new datatype, translated into 'true' existential types '真' の存在型へ変換された新しいデータ型

 data T' = MkT' (exists a. Show a => a)

Again the class constraint serves to limit the types we're unioning over, so that now we know the values inside a MkT' are elements of some arbitrary type which instantiates Show. The implication of this is that we can apply show to a value of type exists a. Show a => a. It doesn't matter exactly which type it turns out to be.

再び和集合をとる型を制限をするため、クラス制約を提供する。MkT' の中にある値は、Show のインスタンスである何らかの任意の型の値であることがわかる。これが意味しているのは、型 exists a. Show a => a の値に対して show を適用することができるということだ。どの型なのかわかってもまったく問題はない。

Example: Using our new heterogenous setup 新しい非統一機構の使用

 heteroList' = [MkT' 5, MkT' (), MkT' True, MkT' "Sartre"]
 main = mapM_ (\(MkT' x) -> print x) heteroList'

 {- prints:
 5
 ()
 True
 "Sartre"
 -}

To summarise, the interaction of the universal quantifier with datatypes produces existential types. As most interesting applications of forall-involving types use this interaction, we label such types 'existential'. Whenever you want existential types, you must wrap them up in a datatype constructor, they can't exist "out in the open" like with [exists a. a].

まとめると、データ型を全称量化子の相互作用は存在型を生み出す。forall を含む型の多くの興味深いの適用がこの相互作用を使用することにより、それらの型を存在型とするのである。存在型が欲しい時はいつでもデータ構築子でそれをラップしなければならず、[exists a. a] のように公然と現れることはできないのだ。

Example: runST 例: runST

One monad that you may not have come across so far is the ST monad. This is essentially the State monad on steroids: it has a much more complicated structure and involves some more advanced topics. It was originally written to provide Haskell with IO. As we mentioned in the Understanding monads chapter, IO is basically just a State monad with an environment of all the information about the real world. In fact, inside GHC at least, ST is used, and the environment is a type called RealWorld.

ST モナドはこれまで出くわしたことはないかもしれない。本質的にはこれは State モナドを強化したものだ。これはより複雑な構造を持ち、より高度な話題を含む。これは本来 Haskell に IO を提供するために書かれたものだ。Understanding monads の章で言及したように、IO は基本的には現実世界の情報すべての環境つきのただの State モナドである。実際、GHC 内部では少なくとも、ST が使われており、環境は RealWorld はと呼ばれる型である。

To get out of the State monad, you can use runState. The analogous function for ST is called runST, and it has a rather particular type:

State モナドから外へ出るには、runState を使うことができる。ST における類似した関数は runST と呼ばれており、これは独特な型をもつ。

Example: The runST function runST 関数

runST :: forall a. (forall s. ST s a) -> a

This is actually an example of a more complicated language feature called rank-2 polymorphism, which we don't go into in detail here. It's important to notice that there is no parameter for the initial state. Indeed, ST uses a different notion of state to State; while State allows you to get and put the current state, ST provides an interface to references. You create references, which have type STRef, with newSTRef :: a -> ST s (STRef s a), providing an initial value, then you can use readSTRef :: STRef s a -> ST s a and writeSTRef :: STRef s a -> a -> ST s () to manipulate them. As such, the internal environment of a ST computation is not one specific value, but a mapping from references to values. Therefore, you don't need to provide an initial state to runST, as the initial state is just the empty mapping containing no references.

これはより複雑な rank-2 多相 (polymorphism) と呼ばれる言語機能の実例となっているが、ここでは詳細には立ち入らない。重要なのは初期状態を与える引数は存在しないことに気づくことである。代わりに、ST は State に対して異なる状態の記法を使用する。State は現在の状態を取得 (get) と設定 (put) することを可能にするのに加え、ST 参照 のインターフェイスを提供する。newSTRef :: a -> ST s (STRef s a) によって初期値を与え STRef という型を持つ参照を作ると、これを操作する readSTRef :: STRef s a -> ST s a と writeSTRef :: STRef s a -> a -> ST s () を使うことができる。ST 計算の内部環境はある特定のものではなく、それ自体は参照から値への対応付けである。それゆえ、初期状態は単に参照を含まない空の対応付けなので、runST に初期状態を提供する必要はない。

However, things aren't quite as simple as this. What stops you creating a reference in one ST computation, then using it in another? We don't want to allow this because (for reasons of thread-safety) no ST computation should be allowed to assume that the initial internal environment contains any specific references. More concretely, we want the following code to be invalid:

しかしながら、ことはそれほど単純ではない。ひとつの ST 計算において参照を作り、それが他で使われることを止めにはどうすればよいのだろうか？(スレッド安全性の理由で) ST 計算は初期内部環境はいかなる特定の参照を含むという仮定をも許容すべきではないので、これを許容したくはない。より具体的には、次のようなコードは不正としたい。

Example: Bad ST code 良くない ST コード

 let v = runST (newSTRef True)
 in runST (readSTRef v)

What would prevent this? The effect of the rank-2 polymorphism in runST's type is to constrain the scope of the type variable s to be within the first parameter. In other words, if the type variable s appears in the first parameter it cannot also appear in the second. Let's take a look at how exactly this is done. Say we have some code like the following:

これを防ぐにはどうすればいいのだろうか？runST の型においての rank-2 多相の効果は最初の引数のなかだけに s のスコープを制約する ことだ。言い換えれば、この型変数 s はふたつめの引数には現れないが最初の引数に現れる。どうやってこれをうまくやるのかみていこう。次のコードのようにする。

Example: Briefer bad ST code より簡潔な悪い ST コード

... runST (newSTRef True) ...

The compiler tries to fit the types together:

コンパイラはこの型を一致させようと試みる。

Example: The compiler's typechecking stage コンパイラの型チェック段階

newSTRef True :: forall s. ST s (STRef s Bool)
runST :: forall a. (forall s. ST s a) -> a
together, forall a. (forall s. ST s (STRef s Bool)) -> STRef s Bool

The importance of the forall in the first bracket is that we can change the name of the s. That is, we could write:

最初の括弧の forall の重要性は、その名前 s を変更することができることだ。これは次のようにかける。

Example: A type mismatch! 型の不一致！

together, forall a. (forall s'. ST s' (STRef s' Bool)) -> STRef s Bool

This makes sense: in mathematics, saying $\forall x.x>5$ is precisely the same as saying $\forall y.y>5$; you're just giving the variable a different label. However, we have a problem with our above code. Notice that as the forall does not scope over the return type of runST, we don't rename the s there as well. But suddenly, we've got a type mismatch! The result type of the ST computation in the first parameter must match the result type of runST, but now it doesn't!

$\forall x.x>5$というのは$\forall y.y>5$というのとちょうど同じ、というのは数学的に理にかなっている。変数に別のラベルを与えているだけである。しかしながら、先ほどのコードには問題がある。runST の返り値の型に対しては forall はスコープに含めないので、そこでは s の名前を変えないことに注意しよう。しかし、突如として型の不一致が起きる！最初の引数において、ST 計算の返り値の型は runST の返り値の型と一致しなければならないが、そうなっていない！

The key feature of the existential is that it allows the compiler to generalise the type of the state in the first parameter, and so the result type cannot depend on it. This neatly sidesteps our dependence problems, and 'compartmentalises' each call to runST into its own little heap, with references not being able to be shared between different calls.

この存在性の重要な機能は、最初の引数でコンパイラに状態の型を一般化することを可能にし、返り値の型はそれに依存することはできないことだ。これは　この依存性の問題をうまく回避し、異なる呼び出しの間で参照が共有されることができないことにより、それぞれの runST 呼び出しをそれ自身の小さなヒープ内に '区切る' (compartmentalise)のである。

Quantification as a primitive 組み込み要素としての量化

Universal quantification is useful for defining data types that aren't already defined. Suppose there was no such thing as pairs built into haskell. Quantification could be used to define them.

全称量化はまだ定義されていないデータ型を定義するのに便利である。Haskell に組のような型がなかったとしよう。量化は次のような定義を可能にする。

newtype Pair a b=Pair (forall c.(a->b->c)->c)

Notes

Further reading 参考文献

• GHC's user guide contains useful information on existentials, including the various limitations placed on them (which you should know about). GHC のユーザガイドには、(あなたも知っておくべき)課せられている様々な制限を含む存在量化についての 役に立つ情報 がある。
• Lazy Functional State Threads, by Simon Peyton-Jones and John Launchbury, is a paper which explains more fully the ideas behind ST.　Simon Peyton-Jones および John Launchbury、Lazy Functional State Threads は ST の背後にある更に詳しいアイデアを説明している論文である。

---