在函数返回类型中模拟存在量词

Question

有时我需要返回存在量化类型的值。这通常发生在我使用幻象类型时（例如表示平衡树的深度）。据我所知，GHC没有任何类型的exists量词。它只允许存在量化数据类型（直接或使用GADTs）。

举个例子，我想要像这样的函数：

-- 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)

到目前为止，我有两个可能的解决方案，将它们添加为答案，如果有人知道更好或不同的方法，我会很高兴知道。

- Petr

Answer 1

标准解决方案是创建一个存在量化的数据类型。结果将类似于

{-# 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 都会产生一个构造器的应用，然后立即解构。与之前一样，Exists1 不能使用 newtype，但我猜想，在没有任何类型类限制的情况下，编译器可以允许它。

---

我基于 rank-N continuation 创建了另一种解决方案。它不需要额外的构造器，但我不确定是否额外的函数应用会增加类似的开销。在第一种情况下，解决方案如下:

{-# 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. 代码可读性减少（至少对于不习惯continuations的人来说）。

- Petr