7

存在記号型の値を返す必要がある場合があります。これは、ファントムタイプ（たとえば、バランスの取れた木の深さを表す）で作業しているときに最も頻繁に発生します。AFAIKGHCには数量詞はありませんexists。存在記号のデータ型のみを許可します（直接またはGADTを使用）。

例を挙げると、次のような関数が必要です。

-- return something that can be shown
somethingPrintable :: Int -> (exists a . (Show a) => a)
-- return a type-safe vector of an unknown length
fromList :: [a] -> (exists n . Vec a n)

これまでのところ、答えとして追加する2つの可能な解決策があります。誰かがより良いまたは異なることを知っているかどうかを知りたいと思います。

4

1 に答える 1

10

標準的な解決策は、存在記号化されたデータ型を作成することです。結果は次のようになります

{-# LANGUAGE ExistentialQuantification #-}

data Exists1 = forall a . (Show a) => Exists1 a
instance Show Exists1 where
    showsPrec _ (Exists1 x) = shows x

somethingPrintable1 :: Int -> Exists1
somethingPrintable1 x = Exists1 x

これで、を自由に使用できますshow (somethingPrintable 42)。Exists1することはできません、それは隠されたコンテキスト辞書でnewtypeの特定の実装を渡す必要があるためだと思います。show

タイプセーフなベクターの場合、同じ方法でfromList1実装を作成できます。

{-# LANGUAGE GADTs #-}

data Zero
data Succ n

data Vec a n where
    Nil  ::                 Vec a Zero   
    Cons :: a -> Vec a n -> Vec a (Succ n)

data Exists1 f where
    Exists1 :: f a -> Exists1 f

fromList1 :: [a] -> Exists1 (Vec a)
fromList1 [] = Exists1 Nil
fromList1 (x:xs) = case fromList1 xs of
                    Exists1 r -> Exists1 $ Cons x r

これはうまく機能しますが、私が見る主な欠点は追加のコンストラクターです。を呼び出すたびfromList1に、コンストラクターが適用され、すぐに分解されます。以前のように、newtypeは不可能Exists1ですが、型クラスの制約がなければ、コンパイラーはそれを許可できると思います。

ランクNの継続に基づいて別のソリューションを作成しました。追加のコンストラクターは必要ありませんが、追加の関数適用が同様のオーバーヘッドを追加しないかどうかはわかりません。最初のケースでは、解決策は次のようになります。

{-# LANGUAGE Rank2Types #-}

somethingPrintable2 :: Int -> ((forall a . (Show a) => a -> r) -> r)
somethingPrintable2 x = \c -> c x

これで、結果を取得するために使用somethingPrintable 42 showします。

そして、Vecデータ型の場合：

{-# LANGUAGE RankNTypes, GADTs #-}

fromList2 :: [a] -> ((forall n . Vec a n -> r) -> r)
fromList2 [] c      = c Nil
fromList2 (x:xs) c  = fromList2 xs (c . Cons x)

-- Or wrapped as a newtype
-- (this is where we need RankN instead of just Rank2):
newtype Exists3 f r = Exists3 { unexists3 :: ((forall a . f a -> r) -> r) }

fromList3 :: [a] -> Exists3 (Vec a) r
fromList3 []     = Exists3 (\c -> c Nil)
fromList3 (x:xs) = Exists3 (\c -> unexists3 (fromList3 xs) (c . Cons x))

これは、いくつかのヘルパー関数を使用してもう少し読みやすくすることができます。

-- | A helper function for creating existential values.
exists3 :: f x -> Exists3 f r
exists3 x = Exists3 (\c -> c x)
{-# INLINE exists3 #-}

-- | A helper function to mimic function application.
(?$) :: (forall a . f a -> r) -> Exists3 f r -> r
(?$) f x = unexists3 x f
{-# INLINE (?$) #-}

fromList3 :: [a] -> Exists3 (Vec a) r
fromList3 []     = exists3 Nil
fromList3 (x:xs) = (exists3 . Cons x) ?$ fromList3 xs

ここで見られる主な欠点は次のとおりです。

  1. 追加の関数適用で発生する可能性のあるオーバーヘッド（コンパイラーがこれをどれだけ最適化できるかはわかりません）。
  2. 読みにくいコード（少なくとも継続に慣れていない人にとって）。
于 2012-08-24T09:57:31.757 に答える