haskell - 如何使用更高等级（rank-N）类型多态性来表达存在类型？

Question

我们习惯于为多态函数提供普遍量化的类型。存在量化类型的使用频率要低得多。我们如何使用通用类型量词来表达存在量化类型？

Answer 1

Answer 2

我在Jean-Yves Girard、Yves Lafont 和 Paul Taylor 的 Proofs and Types中找到了答案。

想象一下，我们有一些单参数类型并构造了一个适用于某些:t :: * -> *的存在类型。我们可以用这样的类型做什么？为了从中计算出一些东西，我们需要一个可以接受任意值的函数，这意味着一个类型的函数。知道了这一点，我们可以将存在类型简单地编码为一个函数，该函数接受 type 的函数，为它们提供存在值并返回结果：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 思维中解放出来。