如何使用较高等级（等级N）型的多态性表达存在的类型？(How to express existent

我们已经习惯了有普遍量化类型多态函数。存在性量化类型通常少得多使用。我们怎样才能表达使用通用型量词存在性量化类型？

Answer 1:

事实证明，存在类型Σ-类型（SIGMA类型）的一个特例。这些是什么？

西格玛类型

正如Π类型（PI类型）概括我们的普通函数类型，允许所得到的类型依赖于它的参数的值，Σ-类型概括对，允许第二组件的类型依赖于第一个的值。

在一个虚构的哈斯克尔语法类似，Σ型应该是这样的：

data Sigma (a :: *) (b :: a -> *)
    = SigmaIntro
        { fst :: a
        , snd :: b fst
        }

-- special case is a non-dependent pair
type Pair a b = Sigma a (\_ -> b)

假设* :: * （即不一致的Set : Set ），我们可以定义exists a. a exists a. a为：

Sigma * (\a -> a)

第一组分是一种类型的，第二个是该类型的值。一些例子：

foo, bar :: Sigma * (\a -> a)
foo = SigmaIntro Int  4
bar = SigmaIntro Char 'a'

exists a. a exists a. a是相当无用的-我们不知道是什么类型里面，所以只有那些可以使用它的操作是类型无关的功能，如id或const 。让我们来扩展它exists a. F a exists a. F a甚至exists a. Show a => F a exists a. Show a => F a 。鉴于F :: * -> * ，第一种情况是：

Sigma * F   -- or Sigma * (\a -> F a)

第二个是有点棘手。我们不能只取一Show a类类的实例，并把它放在里面。然而，如果我们得到一个Show a字典（类型ShowDictionary a ），我们可以用实际值收拾吧：

Sigma * (\a -> (ShowDictionary a, F a))
-- inside is a pair of "F a" and "Show a" dictionary

这是一个有点不方便继续努力，假设我们有一个Show各地字典，但它的作品。包装词典沿着实际上是存在的编制类型时，GHC做什么，所以我们可以定义一个快捷方式，有它比较方便，但这是另一个故事。正如我们将学习很快，编码实际上并不存在这个问题。

题外话：由于各种约束，有可能物化类型类为具体的数据类型。首先，我们需要一些语言编译指示和一个进口：

{-# LANGUAGE ConstraintKinds, GADTs, KindSignatures  #-}
import GHC.Exts -- for Constraint

GADTs已经给我们收拾型类构造函数，例如沿选项：

data BST a where
    Nil  :: BST a
    Node :: Ord a => a -> BST a -> BST a -> BST a

但是，我们可以更进一步：

data Dict :: Constraint -> * where
    D :: ctx => Dict ctx

它的工作原理很像BST上面的例子：模式匹配D :: Dict ctx使我们能够访问整个上下文ctx ：

show' :: Dict (Show a) -> a -> String
show' D = show

(.+) :: Dict (Num a) -> a -> a -> a
(.+) D = (+)

我们也得到生存类型的量化超多类型变量很自然的概括，如exists a b. F ab exists a b. F ab 。

Sigma * (\a -> Sigma * (\b -> F a b))
-- or we could use Sigma just once
Sigma (*, *) (\(a, b) -> F a b)
-- though this looks a bit strange

编码

现在的问题是：我们可以编码 Σ-类型只Π类型？如果是，则存在类型的编码仅仅是一个特例。在所有的荣耀，我为您呈现实际的编码：

newtype SigmaEncoded (a :: *) (b :: a -> *)
    = SigmaEncoded (forall r. ((x :: a) -> b x -> r) -> r)

还有一些有趣的相似之处。由于依赖对代表存在量词，并从经典逻辑，我们知道：

(∃x)R(x) ⇔ ¬(∀x)¬R(x) ⇔ (∀x)(R(x) → ⊥) → ⊥

forall r. r forall r. r 几乎是⊥ ，所以有位改写我们的得到：

(∀x)(R(x) → r) → r

最后，代表通用量化为的依赖函数：

forall r. ((x :: a) -> R x -> r) -> r

此外，让我们来看看教堂编码对的类型。我们得到一个非常容貌相似类型：

Pair a b  ~  forall r. (a -> b -> r) -> r

我们只是表达一个事实，即b可能取决于价值a ，我们可以利用相关的函数来完成。再次，我们得到了相同的类型。

相应的编码/解码功能是：

encode :: Sigma a b -> SigmaEncoded a b
encode (SigmaIntro a b) = SigmaEncoded (\f -> f a b)

decode :: SigmaEncoded a b -> Sigma a b
decode (SigmaEncoded f) = f SigmaIntro
-- recall that SigmaIntro is a constructor

特殊情况实际上简化的东西，以至于它成为在Haskell表达，让我们一起来看看：

newtype ExistsEncoded (F :: * -> *)
    = ExistsEncoded (forall r. ((x :: *) -> (ShowDictionary x, F x) -> r) -> r)
    -- simplify a bit
    = ExistsEncoded (forall r. (forall x. (ShowDictionary x, F x) -> r) -> r)
    -- curry (ShowDictionary x, F x) -> r
    = ExistsEncoded (forall r. (forall x. ShowDictionary x -> F x -> r) -> r)
    -- and use the actual type class
    = ExistsEncoded (forall r. (forall x. Show x => F x -> r) -> r)

需要注意的是，我们可以查看f :: (x :: *) -> x -> x作为f :: forall x. x -> x f :: forall x. x -> x 。也就是说，有额外的功能*参数表现为多态函数。

而一些例子：

showEx :: ExistsEncoded [] -> String
showEx (ExistsEncoded f) = f show

someList :: ExistsEncoded []
someList = ExistsEncoded $ \f -> f [1]

showEx someList == "[1]"

请注意， someList实际上是通过构建encode ，但我们放弃了a说法。这是因为哈斯克尔会推断出x在forall x. 你实际上意味着部分。

从Π到Σ？

奇怪的是（虽然出了这个问题的范围），你可以通过编码Σ-类型和普通函数类型Π类型：

newtype PiEncoded (a :: *) (b :: a -> *)
    = PiEncoded (forall r. Sigma a (\x -> b x -> r) -> r)
-- \x -> is lambda introduction, b x -> r is a function type
-- a bit confusing, I know

encode :: ((x :: a) -> b x) -> PiEncoded a b
encode f = PiEncoded $ \sigma -> case sigma of
    SigmaIntro a bToR -> bToR (f a)

decode :: PiEncoded a b -> (x :: a) -> b x
decode (PiEncoded f) x = f (SigmaIntro x (\b -> b))

Answer 2:

我发现在前面回答的让-伊夫·吉拉德，伊夫·乐峰和保罗·泰勒证明和类型。

试想一下，我们有一些单参数的类型t :: * -> *并构建一个保存了生存型ta一些a ： exists a. ta exists a. ta 。我们可以做这样的类型是什么？为了计算出来的东西是我们需要一个可以接受的功能ta的任意a ，这意味着类型的函数forall a. ta -> b forall a. ta -> b 。认识到这一点，我们可以简单地编码一个存在类型为采用类型的功能的功能forall a. ta -> b forall a. ta -> b ，所述存在值提供给他们，并返回结果b ：

{-# 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思想解放自己。