119

私は Haskell にあまり詳しくないので、これは非常に簡単な質問かもしれません。

Rank2Typesはどの言語制限を解決しますか? Haskell の関数はすでに多相引数をサポートしていませんか?

4

5 に答える 5

175

システム Fを直接勉強しない限り、上位ポリモーフィズムを理解するのは困難です。Haskell は単純化のために、その詳細を隠蔽するように設計されているからです。

a -> bしかし基本的には、多相型は実際には Haskell での形式を持っていないというのが大まかな考え方です。実際には、これらは常に明示的な量指定子を使用して、次のようになります。

id :: ∀a.a → a
id = Λt.λx:t.x

「∀」記号がわからない場合は、「for all」と読みます。∀x.dog(x)「すべての x に対して、x は犬である」という意味です。「Λ」は大文字のラムダで、型パラメーターの抽象化に使用されます。2 行目は、 id が type をt受け取る関数であり、その型によってパラメーター化された関数を返すことを示しています。

System F では、そのような関数をすぐに値に適用することはできませんid。まず、値に適用する λ 関数を取得するために、型に Λ 関数を適用する必要があります。たとえば、次のようになります。

(Λt.λx:t.x) Int 5 = (λx:Int.x) 5
                  = 5

標準の Haskell (つまり、Haskell 98 および 2010) は、これらの型量指定子、大文字のラムダ、および型適用を持たないことでこれを単純化しますが、コンパイルのためにプログラムを分析するときに、舞台裏で GHC がそれらを組み込みます。(これはすべてコンパイル時のもので、実行時のオーバーヘッドはないと思います。)

しかし、Haskell がこれを自動的に処理するということは、"∀" が関数 ("→") 型の左側の分岐に現れることは決してないと仮定することを意味します。 Rank2Typesこれらの制限をRankNTypesオフにして、挿入する場所に関する Haskell のデフォルト ルールをオーバーライドできるようにしますforall。

なぜこれをしたいのですか？完全で制限のない System F は非常に強力で、多くの優れた機能を実行できるからです。たとえば、型の隠蔽とモジュール性は、上位の型を使用して実装できます。たとえば、次のランク 1 タイプの単純な古い関数を考えてみましょう (シーンを設定するため)。

f :: ∀r.∀a.((a → r) → a → r) → r

を使用するfには、呼び出し元は最初に と に使用する型を選択しr、a次に結果の型の引数を指定する必要があります。だからあなたは選ぶことができr = Intますa = String：

f Int String :: ((String → Int) → String → Int) → Int

しかし、それを次の上位タイプと比較してください。

f' :: ∀r.(∀a.(a → r) → a → r) → r

このタイプの関数はどのように機能しますか? それを使用するには、まず に使用する型を指定しますr。選ぶとしましょうInt:

f' Int :: (∀a.(a → Int) → a → Int) → Int

しかし、今は∀aが関数アローの内側にあるため、 に使用するタイプを選択することはできませんa。f' Int適切なタイプの Λ 関数に適用する必要があります。これは、 get の実装が、 の呼び出し元ではなく、f'に使用する型を選択af'することを意味します。逆に、上位の型がない場合は、呼び出し元が常に型を選択します。

これは何に役立ちますか？まあ、実際には多くのことですが、これを使用してオブジェクト指向プログラミングなどをモデル化できるという考えがあります。オブジェクト指向プログラミングでは、「オブジェクト」がいくつかの隠しデータを隠しデータで動作するいくつかのメソッドと一緒にバンドルします。たとえば、 を返すメソッドと を返すメソッドの 2 つのメソッドを持つオブジェクトは、Int次のString型で実装できます。

myObject :: ∀r.(∀a.(a → Int, a -> String) → a → r) → r

これはどのように作動しますか？オブジェクトは、隠しタイプの内部データを持つ関数として実装されますa。オブジェクトを実際に使用するために、そのクライアントは、オブジェクトが 2 つのメソッドで呼び出す「コールバック」関数を渡します。例えば：

myObject String (Λa. λ(length, name):(a → Int, a → String). λobjData:a. name objData)

ここでは、基本的に、オブジェクトの 2 番目のメソッドを呼び出しています。これは、タイプがa → Stringunknownのメソッドaです。まあ、myObjectのクライアントには知られていません。しかし、これらのクライアントは署名から、2 つの関数のいずれかをそれに適用して、Intまたは のいずれかを取得できることを知っていStringます。

実際の Haskell の例として、私が独学で書いたコードを以下に示しますRankNTypes。これは、非表示の型の値をそのクラス インスタンスShowBoxと一緒にバンドルする、と呼ばれる型を実装します。Show下部の例ではShowBox、最初の要素が数値から作成され、2 番目の要素が文字列から作成されたリストを作成していることに注意してください。上位の型を使って型を隠しているので、型チェック違反にはなりません。

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}

type ShowBox = forall b. (forall a. Show a => a -> b) -> b

mkShowBox :: Show a => a -> ShowBox
mkShowBox x = \k -> k x

-- | This is the key function for using a 'ShowBox'.  You pass in
-- a function @k@ that will be applied to the contents of the 
-- ShowBox.  But you don't pick the type of @k@'s argument--the 
-- ShowBox does.  However, it's restricted to picking a type that
-- implements @Show@, so you know that whatever type it picks, you
-- can use the 'show' function.
runShowBox :: forall b. (forall a. Show a => a -> b) -> ShowBox -> b
-- Expanded type:
--
--     runShowBox 
--         :: forall b. (forall a. Show a => a -> b) 
--                   -> (forall b. (forall a. Show a => a -> b) -> b)
--                   -> b
--
runShowBox k box = box k


example :: [ShowBox] 
-- example :: [ShowBox] expands to this:
--
--     example :: [forall b. (forall a. Show a => a -> b) -> b]
--
-- Without the annotation the compiler infers the following, which
-- breaks in the definition of 'result' below:
--
--     example :: forall b. [(forall a. Show a => a -> b) -> b]
--
example = [mkShowBox 5, mkShowBox "foo"]

result :: [String]
result = map (runShowBox show) example

追伸: これを読んでいてExistentialTypes、GHC がどのように使用されているのか疑問に思っforallている人のために、その理由は、舞台裏でこの種の手法を使用しているためだと思います。

于 2012-08-20T07:11:44.567 に答える
121

Haskell の関数はすでに多相引数をサポートしていませんか?

They do, but only of rank 1. つまり、この拡張なしで異なる型の引数を取る関数を作成できますが、同じ呼び出しで引数を異なる型として使用する関数を作成することはできません。

たとえば、次の関数はg、 の定義で異なる引数の型で使用されているため、この拡張子なしでは型指定できませんf。

f g = g 1 + g "lala"

多相関数を引数として別の関数に渡すことは完全に可能であることに注意してください。したがって、次のようなものmap id ["a","b","c"]は完全に合法です。ただし、関数はそれを単相としてのみ使用できます。この例では、 type を持っているかのようにmap使用しています。もちろん、 の代わりに、指定された型の単純な単相関数を渡すこともできます。関数は、rank2types がなければ、その引数が多相関数でなければならないことを要求する方法がなく、したがって、それを多相関数として使用する方法もありません。idString -> Stringid

于 2012-08-20T03:14:32.387 に答える
52

Luis Casillas の回答は、ランク 2 のタイプが何を意味するかについて多くの優れた情報を提供しますが、彼がカバーしなかった 1 つのポイントについて説明します。引数がポリモーフィックであることを要求することは、それを複数の型で使用できるようにするだけではありません。また、その関数がその引数でできることと、その結果を生成する方法も制限します。つまり、呼び出し元の柔軟性が低下します。なぜそれをしたいのですか？簡単な例から始めます。

データ型があるとします

data Country = BigEnemy | MediumEnemy | PunyEnemy | TradePartner | Ally | BestAlly

関数を書きたい

f g = launchMissilesAt $ g [BigEnemy, MediumEnemy, PunyEnemy]

IOこれは、指定されたリストの要素の 1 つを選択し、そのターゲットにミサイルを発射するアクションを返す関数を受け取ります。f単純な型を与えることができます:

f :: ([Country] -> Country) -> IO ()

問題は、誤って実行する可能性があることです

f (\_ -> BestAlly)

そして、私たちは大きな問題になるでしょう！fランク 1 のポリモーフィック型を与える

f :: ([a] -> a) -> IO ()

aを呼び出すときにタイプを選択し、fそれを特殊化しCountryて悪意のあるものを再度使用するだけなので、まったく役に立ちません\_ -> BestAlly。解決策は、ランク 2 タイプを使用することです。

f :: (forall a . [a] -> a) -> IO ()

渡す関数はポリモーフィックである必要があるため、\_ -> BestAlly型チェックは行いません! 実際、指定されたリストにない要素を返す関数は型チェックを行いません (ただし、無限ループに入ったり、エラーを生成したために決して返されない一部の関数は型チェックを行います)。

もちろん、上記は不自然ですが、STモナドを安全にするための鍵となるのは、このテクニックのバリエーションです。

于 2014-07-12T21:57:10.160 に答える