如何使用更高级别（rank-N）类型多态表达存在类型？ [英] How to express existential types using higher rank (rank-N) type polymorphism?

问题描述

我们习惯于对多态函数进行普遍量化的类型。存在量化类型的使用要少得多。我们如何使用通用类型量词表达存在量化类型？

解决方案

事实证明，存在类型只是Σ - 类型（西格玛类型）。它们是什么？

西格玛类型

正如Π类型（pi类型）泛化我们的普通函数类型，允许结果类型取决于其参数值Σ-types generalize pairs，允许第二个组件的类型取决于第一个组件的值。

在类似于Haskell的语法中，Σ-type看起来像这样：

 数据Sigma（a :: *）（b :: a  - > *）
 = SigmaIntro 
 {fst :: a 
，snd :: b fst 
} 
 
  - 特例是一个非依赖对
类型Pair ab = Sigma a（\_-> b）
  * :: * （即不一致的 Set ：设置），我们可以定义存在a。 a 为： 
 
 
  Sigma *（\ a  - > a）
  
第一个组件是类型，第二个是该类型的值。一些例子：
 
 $ p $ f $ bar $ Sigma $（$ a $ a $ b $ f foo = SigmaIntro Int 4 
 bar = SigmaIntro Char'a'
  

存在a 。一个是相当无用的 - 我们不知道里面是什么类型，所以可以使用的唯一操作是类型无关的函数，比如 id 或 const 。让我们将它扩展为 exists a。 F a 甚至存在a。显示a => F a 。给定 F :: * - > * ，第一种情况是：

  Sigma * F  - 或Sigma *（\ a - > F a）
  

第二个有点棘手。我们不能只取一个显示一个类型的实例，并将它放在里面的某个地方。但是，如果我们给出一个显示一个字典（类型为 ShowDictionary a ），我们可以将它与实际值：

 西格玛*（\-  - >（ShowDictionary a，F a））
  - 里面是一对F a和显示字典
  

这样做有点不方便with并假定我们有一个 Show 字典，但它可以工作。包装字典实际上是GHC在编译存在类型时所做的，所以我们可以定义一个捷径来让它更方便，但那是另一回事。由于我们将很快学会，编码实际上并没有受到这个问题的影响。

---

移动：感谢约束种类，可以将类型类型化为具体的数据类型。首先，我们需要一些语言编译指示和一个导入：

  { - ＃LANGUAGE Con​​straintKinds，GADTs，KindSignatures＃ - } 
 import GHC.Exts  -  for Constraint 
  

GADT已经给我们提供了将类型类打包的选项例如：

 数据BST a其中
 Nil :: BST a 
节点： ：Ord a => a  - > BST a  - > BST a  - > BST a 
  

然而，我们可以更进一步：

  data Dict :: Constraint  - > *其中
 D :: ctx => Dict ctx 
  

它与 BST 上面的例子：在 D :: Dict ctx 上的模式匹配使我们能够访问整个上下文 ctx ：

  show':: Dict（显示a） - > a  - > String 
 show'D = show 
 
（。+）:: Dict（Num a） - > a  - > a  - > a 
（。+）D =（+）
  

---

我们也对存在类型进行了相当自然的推广，这些类型量化了更多的类型变量，如存在a b。 F ab 。

  Sigma *（\a-→Sigma Sigma *（\ b  - > F ab））
  - 或者我们可以使用Sigma一次
 Sigma（*，*）（\（a，b） - > F ab）
  - 尽管这看起来有点奇怪
  

编码

现在，问题是：我们可以用Π类型对Σ-型进行编码吗？如果是，那么存在型编码只是一个特例。在所有荣耀中，我向你展示了实际编码：

  newtype SigmaEncoded（a :: *）（b :: a  - > ; *）
 = SigmaEncoded（forall r。（（x :: a） - > bx  - > r） - > r）
  

有一些有趣的相似之处。由于从属对代表存在性量化，并且从经典逻辑中我们知道：

$ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $（$）$（$）R（x）⇔¬（∀ x）¬R（x）⇔（∀x）（R（x）→⊥）→⊥

forall r。 r 几乎是 ⊥，所以稍微改写一下就可以得到：

 （∀x）（R（x）→r）→r 
  

最后，将通用量化表示为相关函数：

  forall r。 （（x :: a）→R x→r）→> r 
  

另外，让我们来看看Church编码对的类型。我们得到一个非常相似的类型：

 配对b〜forall r。 （a  - > b  - > r） - > r 
  

我们只需表达一个事实，即 b 可能取决于 a 的值，我们可以通过使用依赖函数来完成。

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

$ pre> encode :: Sigma ab - > SigmaEncoded一个b
编码（SigmaIntro a b）= SigmaEncoded（\ f - > f a b）

decode :: SigmaEncoded a b - > Sigma Ab
解码（SigmaEncoded f）= f SigmaIntro
- 回忆SigmaIntro是一个构造函数


特殊情况实际上已经简化了足够的东西，它可以在Haskell中表现出来，让我们来看看：

  newtype ExistsEncoded （F :: *  - > *）
 = ExistsEncoded（forall r。（（x :: *） - >（ShowDictionary x，F x） - > r） - > r）
  - 简化一点
 = 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）
  - 并使用实际的类型类
 = ExistsEncoded （forall r。（forall x。Show x => F x  - > r） - > r）
  

请注意，我们可以查看 f ::（x :: *） - > x - > x 作为 f :: forall x。 x - > X 。也就是说，一个带有额外的 * 参数的函数表现为一个多态函数。

还有一些例子：

  showEx :: ExistsEncoded []  - >字符串
 showEx（ExistsEncoded f）= f show 
 
 someList :: ExistsEncoded [] 
 someList = ExistsEncoded $ \f  - > f [1] 
 
 showEx someList ==[1]
  

请注意， someList 实际上是通过 encode 构造的，但我们放弃了 a 参数。这是因为Haskell会推断出 x 部分中的 x 实际上的含义。

从Π到Σ？

奇怪的是（虽然超出了这个问题的范围），您可以通过Σ-类型和常规函数类型：

  newtype PiEncoded（a :: *）（b :: a  - > *）
 = PiEncoded（全部为Sigma a（\ x→bx→r）→r）
  -  \ x  - >是lambda导入，b x  - > r是一个函数类型
  - 有点令人困惑，我知道
 
 encode ::（（x :: a） - > b x） - > PiEncoded a b 
编码f = PiEncoded $ \sigma  - > 
的情况西格玛SigmaIntro a bToR  - > bToR（f a）
 
 decode :: PiEncoded a b  - > （x :: a） - > b x 
 decode（PiEncoded f）x = f（SigmaIntro x（\ b  - > b））
  

We're used to having universally quantified types for polymorphic functions. Existentially quantified types are used much less often. How can we express existentially quantified types using universal type quantifiers?

解决方案

It turns out that existential types are just a special case of Σ-types (sigma types). What are they?

Sigma types

Just as Π-types (pi types) generalise our ordinary function types, allowing the resulting type to depend on the value of its argument, Σ-types generalise pairs, allowing the type of second component to depend on the value of the first one.

In a made-up Haskell-like syntax, Σ-type would look like this:

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)

Assuming * :: * (i.e. the inconsistent Set : Set), we can define exists a. a as:

Sigma * (\a -> a)

The first component is a type and the second one is a value of that type. Some examples:

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

exists a. a is fairly useless - we have no idea what type is inside, so the only operations that can work with it are type-agnostic functions such as id or const. Let's extend it to exists a. F a or even exists a. Show a => F a. Given F :: * -> *, the first case is:

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

The second one is a bit trickier. We cannot just take a Show a type class instance and put it somewhere inside. However, if we are given a Show a dictionary (of type ShowDictionary a), we can pack it with the actual value:

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

This is a bit inconvenient to work with and assumes that we have a Show dictionary around, but it works. Packing the dictionary along is actually what GHC does when compiling existential types, so we could define a shortcut to have it more convenient, but that's another story. As we will learn soon enough, the encoding doesn't actually suffer from this problem.

---

Digression: thanks to constraint kinds, it's possible to reify the type class into concrete data type. First, we need some language pragmas and one import:

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

GADTs already give us the option to pack a type class along with the constructor, for example:

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

However, we can go one step further:

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

It works much like the BST example above: pattern matching on D :: Dict ctx gives us access to the whole context ctx:

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

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

---

We also get quite natural generalisation for existential types that quantify over more type variables, such as exists a b. F a b.

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

The encoding

Now, the question is: can we encode Σ-types with just Π-types? If yes, then the existential type encoding is just a special case. In all glory, I present you the actual encoding:

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

There are some interesting parallels. Since dependent pairs represent existential quantification and from classical logic we know that:

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

forall r. r is almost ⊥, so with a bit of rewriting we get:

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

And finally, representing universal quantification as a dependent function:

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

Also, let's take a look at the type of Church-encoded pairs. We get a very similar looking type:

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

We just have to express the fact that b may depend on the value of a, which we can do by using dependent function. And again, we get the same type.

The corresponding encoding/decoding functions are:

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

The special case actually simplifies things enough that it becomes expressible in Haskell, let's take a look:

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)

Note that we can view f :: (x :: *) -> x -> x as f :: forall x. x -> x. That is, a function with extra * argument behaves as a polymorphic function.

And some examples:

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

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

showEx someList == "[1]"

Notice that someList is actually constructed via encode, but we dropped the a argument. That's because Haskell will infer what x in the forall x. part you actually mean.

From Π to Σ?

Strangely enough (although out of the scope of this question), you can encode Π-types via Σ-types and regular function types:

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

这篇关于如何使用更高级别（rank-N）类型多态表达存在类型？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！