普遍的に量化された型変数と、存在的に量化されたデータ型があります。しかし、exists a. Int -> a概念を説明するために形式の疑似コードが提供されることがあるにもかかわらず、実際に関心のあるコンパイラ拡張のようには思えません。これは単に「これを追加することにあまり価値がない」という類のものなのでしょうか (私には価値があるように思えるため)、それとも決定不能性などの問題があり、本当に不可能なのでしょうか。
編集: viorior さんの回答を正解としてマークしました。おそらくこれが、これが含まれていなかった実際の理由であるように思われるからです。ただし、誰かがこれをさらに明確にしたい場合に備えて、追加のコメントを追加したいと思います。
コメントでリクエストがあったので、なぜこれが便利だと思うかの例を挙げてみます。次のようなデータ型があるとします。
data Person a = Person
{ age: Int
, height: Double
, weight: Int
, name: a
}
aしたがって、命名規則である ではなく、パラメータ化 を選択します(この例ではNamingConvention、アメリカ人の「first,middle,last」、ヒスパニックの「name,paternal name,maternal name」などに適したデータ コンストラクターを使用して ADT を作成する方がおそらく理にかなっていることはわかっています。しかし、今のところは、これで進めます)。
そのため、Personがパラメータ化されている型を基本的に無視する関数がいくつかあります。例は次のとおりです。
age :: Person a -> Int
height :: Person a -> Double
weight :: Person a -> Int
そして、これらの上に構築された関数も同様にa型を無視できます。例:
atRiskForDiabetes :: Person a -> Bool
atRiskForDiabetes p = age p + weight p > 200
--Clearly, I am not actually a doctor
さて、異種の人々のリスト（型[exists a. Person a]）がある場合、リストに対していくつかの関数をマッピングできるようにしたいとします。もちろん、マッピングするのに役に立たない方法がいくつかあります。
heteroList :: [exists a. Person a]
heteroList = [Person 20 30.0 170 "Bob Jones", Person 50 32.0 140 3451115332]
extractedNames = map name heteroList
この例では、extractedNamesは型 であるため、もちろん役に立ちません[exists a. a]。ただし、他の関数を使用する場合は、次のようになります。
totalWeight :: [exists a. Person a] -> Int
totalWeight = sum . map age
numberAtRisk :: [exists a. Person a] -> Int
numberAtRisk = length . filter id . map atRiskForDiabetes
これで、異種コレクションに対して操作できる便利なものができました (しかも、型クラスも使用していません)。既存の関数を再利用できることに注目してください。存在データ型を使用すると、次のようになります。
data SomePerson = forall a. SomePerson (Person a) --fixed, thanks viorior
しかし、ageと をどのように使用すればよいのでしょうかatRiskForDiabetes? できません。次のようにする必要があると思います。
someAge :: SomePerson -> Int
someAge (SomePerson p) = age p
これは、新しい型のためにすべてのコンビネータを書き直す必要があるため、非常に面倒です。複数の型変数にパラメータ化されたデータ型でこれを行う場合は、さらに状況が悪くなります。次の状況を想像してください。
somewhatHeteroPipeList :: forall a b. [exists c d. Pipe a b c d]
この考え方についてはこれ以上説明しませんが、存在データ型だけを使用してこのようなことを行うには、多くのコンビネータを書き直す必要があることに注意してください。
そうは言っても、これが役に立つかもしれないという説得力のある使い方を少しでも示せたことを願っています。役に立たないように思える場合 (または例が不自然すぎると思われる場合) は、遠慮なくお知らせください。また、私はもともとプログラマーであり、型理論の訓練を受けていないため、ここで Skolem の定理 (viorior によって投稿) をどのように使用するかが少しわかりにくいです。私がPerson a示した例にそれをどのように適用するかを教えていただけると大変助かります。ありがとうございます。
ベストアンサー1
それは不要です。
スコーレムの定理により、存在量指定子を高位の型を持つ全称量指定子に変換できます。
(∃b. F(b)) -> Int <===> ∀b. (F(b) -> Int)
ランクn+1の存在量化型はすべて、ランクnの普遍量化型としてエンコードできる。