19

私たちは、ポリモーフィック関数の全称記号型を持つことに慣れています。存在記号タイプは、それほど頻繁には使用されません。ユニバーサル型数量詞を使用して、存在記号型をどのように表現できますか？

4

2 に答える 2

24
于 2012-11-30T23:27:53.280 に答える
15

ジャン＝イヴ・ジラール、イヴ・ラフォント、ポール・テイラーの「証明と種類」で答えを見つけました。

いくつかの1つの引数型があり、いくつかの：t :: * -> *を保持する実存型を構築するとします。そのようなタイプで何ができるでしょうか？それから何かを計算するには、任意のを受け入れることができる関数が必要です。これは、タイプの関数を意味します。これを知っていると、実存型を単純に型の関数を取り、それらに実存的値を提供して結果を返す関数としてエンコードできます。t aaexists a. t at aaforall a. t a -> bforall a. t a -> bb

{-# LANGUAGE RankNTypes #-}

newtype Exists t = Exists (forall b. (forall a. t a -> b) -> b)

実存的な値の作成が簡単になりました。

exists :: t a -> Exists t
exists x = Exists (\f -> f x)

そして、存在する値を解凍したい場合は、その内容を結果を生成する関数に適用するだけです。

unexists :: (forall a. t a -> b) -> Exists t -> b
unexists f (Exists e) = e f

ただし、純粋に存在するタイプはほとんど役に立ちません。私たちが何も知らない値で合理的なことをすることはできません。多くの場合、型クラス制約のある実存型が必要です。手順はまったく同じですが、の型クラス制約を追加するだけですa。例えば：

newtype ExistsShow t = ExistsShow (forall b. (forall a. Show a => t a -> b) -> b)

existsShow :: Show a => t a -> ExistsShow t
existsShow x = ExistsShow (\f -> f x)

unexistsShow :: (forall a. Show a => t a -> b) -> ExistsShow t -> b
unexistsShow f (ExistsShow e) = e f

注：関数型プログラムで存在記号を使用することは、多くの場合、コードの臭いと見なされます。それは、私たちがOO思考から自分自身を解放していないことを示している可能性があります。

于 2012-11-30T21:35:07.993 に答える