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

问题描述

我们习惯于为多态函数使用通用量化的类型.存在量化类型的使用频率要低得多.我们如何使用通用类型量词来表达存在量化类型?

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?

推荐答案

事实证明，存在类型只是 Σ 类型(sigma 类型)的一个特例.它们是什么?

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

正如 Π-types (pi types) 泛化我们的普通函数类型，允许结果类型依赖其参数的值，Σ-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.

在虚构的 Haskell 式语法中，Σ-type 如下所示:

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)

假设* :: *(即不一致的Set : Set)，我们可以定义exists a.一个为:

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'

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

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)

第二个有点棘手.我们不能只是把一个 Show a 类型的类实例放在里面.然而，如果我们得到一个 Show a 字典(ShowDictionary 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

这有点不方便，假设我们有一个 Show 字典，但它可以工作.打包字典实际上是 GHC 在编译存在类型时所做的，所以我们可以定义一个快捷方式来让它更方便，但那是另一回事了.我们很快就会了解到，编码实际上并没有遇到这个问题.

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

GADT 已经为我们提供了将类型类与构造函数一起打包的选项，例如:

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

它的工作方式与上面的 BST 示例非常相似:D :: Dict ctx 上的模式匹配使我们可以访问整个上下文 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 = (+)

<小时>

我们还对存在类型进行了非常自然的概括，这些类型可以量化更多类型变量，例如 exists a b.F a b.

Sigma * (a -> Sigma * ( -> 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 是几乎 ⊥，所以稍微重写一下我们得到:

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

另外，让我们看看 Church-encoded 对的类型.我们得到了一个非常相似的类型:

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

我们只需要表达一个事实，b 可能依赖于 a 的值，我们可以通过使用依赖函数来实现.再次，我们得到相同的类型.

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

特殊情况实际上已经足够简单，以至于它可以在 Haskell 中表达，让我们来看看:

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)

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

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.

还有一些例子:

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

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

showEx someList == "[1]"

请注意，someList 实际上是通过 encode 构造的，但我们删除了 a 参数.那是因为 Haskell 会推断 forall x. 部分中的 x 你实际上是什么意思.

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.

奇怪的是(虽然超出了这个问题的范围)，您可以通过 Σ 类型和常规函数类型对 Π 类型进行编码:

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

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