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

Question

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

Answer 1

事实证明，存在类型只是 Σ 类型(sigma 类型)的一个特例。这些是什么？

西格玛类型

正如 Π 类型(pi 类型)泛化我们的普通函数类型，允许结果类型取决于其参数的值，Σ 类型泛化对，允许第二个组件的类型取决于第一个组件的值。

在一个虚构的类似 Haskell 的语法中，Σ-type 看起来像这样:

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作为:

Sigma * (\a -> a)

第一个组件是一个类型，第二个是该类型的值。一些例子:

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

exists a. a相当没用 - 我们不知道里面是什么类型，所以唯一可以使用它的操作是类型不可知的函数，例如 id或 const .让我们把它扩展到 exists 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

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

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

编码

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

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几乎是 ⊥ ，所以通过一些重写我们得到:

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

最后，将全称量化表示为一个依赖函数:

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

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

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 .也就是说，一个带有额外 * 的函数参数表现为多态函数。

还有一些例子:

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

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

showEx someList == "[1]"

请注意 someList实际上是通过 encode 构建的，但我们删除了 a争论。那是因为 Haskell 会推断出 x在 forall x.你实际上是指的部分。

从 Π 到 Σ？

奇怪的是(尽管超出了这个问题的范围)，您可以通过 Σ-types 和常规函数类型对 Π-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))