なぜ `[1、" a "] :: [forall a。 Show a => a] `は許可されていませんか？二つのリスト次の私（のかもしれない間違った）理解で

Question

は、同等である必要があります。

[1, "a"] :: [forall a. Show a => a] 

data V = forall a. Show a => V a 
[V 1, V "a"] :: [V] 

しかし、最初のものは受け入れられなかったが、第2 1は、（ExistentialQuantificationで）正常に動作します。

最初のリストが存在しない場合は、空白のタイプはmap V :: ??? -> [V]となりますか？どのタイプのメカニズムがラッパーの存在を強制していますか？

Answer 1

あなたの理解は正しくありません。この問題の大きな部分は、使用してきた伝統的な存在量の構文が、それに精通していない人にとってはかなり混乱しているということです。したがって、代わりにGADT構文を使用することを強くお勧めします.GADT構文は厳密に強力です。簡単なことは、{-# LANGUAGE GADTs #-}を有効にすることです。私たちがいる間に、が何を意味するのか不思議に思っていないので、{-# LANGUAGE ScopedTypeVariables #-}をオンにしましょう。

data V where 
    V :: Show a => a -> V 

のでVデータコンストラクタは任意の showableの何かを取る関数である：あなたのV定義は、私たちが好きなら私たちが実際に明示的なforallをドロップすることができ

data V where 
    V :: forall a . Show a => a -> V 

とまったく同じことを意味し、タイプVのものが生成されます。 mapの種類はかなり制限されていますmapに渡されたリストのすべての要素は同じ型を持っている必要が

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

。だから、map Vの種類は、ちょうど

map V :: Show a => [a] -> [V] 

さんはすぐに戻ってあなたの最初の式を取得してみましょうされています

[1, "a"] :: [forall a. Show a => a] 

を今、これは実際に言う[1, "a"]は、その要素のそれぞれがforall a . Show a => a型を持つ、リストであるということです。つまり、Showのインスタンスであるaを指定すると、リストの各要素はその型を持つ必要があります。これは単に真実ではありません。 "a"は、たとえば、タイプがBoolではありません。ここにはもう一つの問題があります。タイプ[forall a . Show a => a]は「批判的」です。私はその意味を理解していませんが、->以外の型コンストラクタの引数にはforallがついています。これは許されません。 GHCはImpredicativeTypes拡張機能を有効にすることを提案しているかもしれませんが、実際にはうまくいきません。存在を定量化したもののリストが必要な場合は、まずそれらを実在するデータ型で囲むか、特殊な実在リスト型を使用する必要があります。普遍的に数量化されたもののリストが必要な場合は、まずそれらを（おそらくnewtypesで）ラップする必要があります。