☰

Haskell/GHC の `forall` キーワードは何をしますか? 質問する

tag-icon • tag-icon haskell syntax types ghc forall
Haskell/GHC の `forall` キーワードは何をしますか? 質問する

forall次のようないわゆる「存在型」でキーワードがどのように使用されるかを理解し始めています。

data ShowBox = forall s. Show s => SB s

ただし、これは使用方法のほんの一部に過ぎず、forall次のような場合の使用法はまったく理解できません。

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

あるいは、これらが異なる理由を説明します。

foo :: (forall a. a -> a) -> (Char, Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

それとも全部RankNTypes...

私は、学術的な環境で普通に使われるような言語よりも、明確で専門用語のない英語を好む傾向があります。これについて私が読もうとした説明のほとんど（検索エンジンで見つけられるもの）には、次のような問題があります。

  1. それらは不完全です。それらは、このキーワードの使用法の一部 (「存在型」など) を説明しており、まったく異なる方法 ( runST、fooおよびbar上記など) でそれを使用しているコードを読むまでは満足しています。
  2. そこには、今週人気の離散数学、圏論、抽象代数の分野の最新版を私が読んだという仮定がぎっしり詰まっています。(「実装の詳細については、論文を参照してください」という言葉を二度と読まなければ、それは早すぎるでしょう。)
  3. それらは、単純な概念でさえも、しばしば複雑にねじ曲げられ、断片化された文法と意味論に変わるような書き方で書かれています。

それで...

実際の質問に移ります。forall私が専門用語にどっぷり浸かった数学者だと想定せずに、キーワードを明確で平易な英語で完全に説明できる人はいますか (または、どこかにそのような明確な説明があるなら、私が見逃した説明を指摘してください)?

ベストアンサー1

コード例から始めましょう:

foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b
foob postProcess onNothin onJust mval =
    postProcess val
    where
        val :: b
        val = maybe onNothin onJust mval

このコードは、プレーンな Haskell 98 ではコンパイルされません (構文エラー)。キーワードをサポートするには拡張機能が必要ですforall。

基本的に、キーワードには 3 つの異なる一般的な用途がありforall(少なくともそう思われます)、それぞれに独自の Haskell 拡張機能があります: ScopedTypeVariables、RankNTypes/ Rank2Types、。ExistentialQuantification

上記のコードでは、どちらかが有効になっている場合、構文エラーは発生しませんが、ScopedTypeVariables有効になっている場合は型チェックのみが行われます。

スコープ付き型変数:

whereスコープ付き型変数は、句内のコードの型を指定するのに役立ちます。これにより、 bin がinval :: bと同じになります。bfoob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b

紛らわしい点forall:型から を省略すると、実際には暗黙的に がまだ存在すると聞くかもしれません。(ノーマンの回答から：「通常、これらの言語は多態型から forall を省略します」）。この主張は正しいですが、これは の他の用法について言及しておりforall、ScopedTypeVariablesの使用については言及していません。

ランクNタイプ:

まず、が有効な場合を除いてmayb :: b -> (a -> b) -> Maybe a -> bと同等であることから始めましょう。mayb :: forall a b. b -> (a -> b) -> Maybe a -> bScopedTypeVariables

つまり、あらゆるaおよびに機能しますb。

たとえば、次のようなことをしたいとします。

ghci> let putInList x = [x]
ghci> liftTup putInList (5, "Blah")
([5], ["Blah"])

この の型は何でしょうかliftTup? それは ですliftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)。理由を確認するために、次のようにコーディングしてみましょう。

ghci> let liftTup liftFunc (a, b) = (liftFunc a, liftFunc b)
ghci> liftTup (\x -> [x]) (5, "Hello")
    No instance for (Num [Char])
    ...
ghci> -- huh?
ghci> :t liftTup
liftTup :: (t -> t1) -> (t, t) -> (t1, t1)

「うーん...なぜ GHC はタプルに同じ型が 2 つ含まれていなければならないと推測するのでしょうか? そうである必要はないと伝えましょう」

-- test.hs
liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

ghci> :l test.hs
    Couldnt match expected type 'x' against inferred type 'b'
    ...

うーん。ここでは、 が必要であり、であるため、 GHCliftFuncでは に適用できません。 関数には、あらゆる を受け入れる関数を取得させたいのです。vv :: bliftFuncxx

{-# LANGUAGE RankNTypes #-}
liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

liftTupつまり、それがすべてに機能するわけではなくx、それが得る機能が機能するのです。

存在定量化:

例を見てみましょう:

-- test.hs
{-# LANGUAGE ExistentialQuantification #-}
data EQList = forall a. EQList [a]
eqListLen :: EQList -> Int
eqListLen (EQList x) = length x

ghci> :l test.hs
ghci> eqListLen $ EQList ["Hello", "World"]
2

それはランクNタイプとどう違うのでしょうか?

ghci> :set -XRankNTypes
ghci> length (["Hello", "World"] :: forall a. [a])
    Couldnt match expected type 'a' against inferred type '[Char]'
    ...

Rank-N-Types では、forall a式はすべての可能なas に適合する必要があります。例:

ghci> length ([] :: forall a. [a])
0

空のリストは任意のタイプのリストとして機能します。

したがって、存在量化では、定義forall内の は、data含まれる値が適切な型であればどれでもかまわないことを意味し、すべての適切な型でなければならないという意味ではありません。

おすすめ記事