如何使用更高级别(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在编译存在类型时所做的事情,因此我们可以定义一个快捷方式以使其更方便,但这是另一个故事.正如我们将很快学到的,编码实际上并没有遇到这个问题.

Digression:由于约束种类,可以将类型类重新定义为具体的数据类型.首先,我们需要一些语言编译指示和一个导入:

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

另外,让我们来看看教会编码对的类型.我们得到一个非常相似的外观类型:

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参数.这是因为哈斯克尔会推断出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

我找到了Jean-Yves Girard,Yves Lafont和Paul Taylor的Proofs and Types的答案.

想象一下,我们有一些单参数类型,t :: * -> *并构造一个适用t a于某些人的存在类型a:exists a. t a.我们可以用这种类型做什么？为了计算出某些东西,我们需要一个可以接受t a任意a的函数,这意味着一个类型的函数forall a. t a -> b.知道了这一点,我们可以将存在类型编码为一个函数,它接受类型函数,forall a. t a -> 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思想中解放出来.