受控的存在类型

# 拴住的存在类型 来源：https://cdfa.github.io/existentials-on-a-leash/ 在本文中，我将分享一种在 Haskell 中对存在类型进行编码的方法，允许它们以“裸露”的形式出现在类型中，从而免去我们用 GADT 构造函数或高阶函数（CPS 风格）包裹存在类型变量的麻烦。该编码基于线性函数，这些函数消耗一个证明令牌，确保存在类型化值的正确处理。 此外，我分享一种独立的技术，确保函数在其结果中实例化隐藏的（“非裸露的”）存在类型时，与输入类型实例化的类型相同，即它们保留隐藏类型变量的实例化。该技术同样依赖线性类型，但不使用上述编码。我将通过实现一个安全的变体 `unsafePartsOf`（https://hackage-content.haskell.org/package/lens-5.3.6/docs/Control-Lens-Combinators.html#v:unsafePartsOf）`:: Functor f => Traversing (->) f s t a b -> LensLike f s t [a] [b]` 光学组合器来演示。 两种技术都使用了 `unsafeCoerce`。我会解释为什么我认为这些强制转换是安全的，但我没有在形式上证明任何东西。如果你看到我遗漏的漏洞，请尝试破坏这些东西。 虽然我会简要解释什么是线性类型，但本文无意作为这一概念的通用介绍。建议读者熟悉 GADT、线性类型和光学（对于相关章节）。 话虽如此，我尽可能让读者轻松地摆弄代码并交互式学习这些概念，为此我提供了一个预先构建的 GitHub Codespace（https://codespaces.new/cdfa/existentials-on-a-leash?quickstart=1）。点击该链接，你可以在 Haskell Language Server 的支持下摆弄代码，无需安装任何东西（提示：使用“Preview embedded markdown”可以同时查看 .hs 文件及其 Markdown 版本）。这甚至可能是阅读本文的一个不错的方式，因为你可以悬停变量和函数以查看其类型等。 ## 存在类型的当前局限 截至 GHC 9.14，GHC 仅支持两种“存在量化”类型变量的方式： 1. 使用 rank-2 类型：`(forall a. a -> r) -> r`。这对应于 `exists a. (a -> r) -> r`（等价于 `exists a. a`）。 2. 使用 GADT：`data Wrapper where Wrapper :: forall a. a -> Wrapper`。当模式匹配 `Wrapper` 时，`a` 将是存在量化的。 这两种技术实际上并不使用存在量化，而是通过否定的全称量化来编码它们。一个为 GHC 添加一等存在类型的 GHC 提案（https://github.com/goldfirere/ghc-proposals/blob/existentials/proposals/0473-existentials.rst）一段时间前就被写好了，但作者似乎优先处理其他工作。该提案还展示了一个简单例子，说明一个函数不可能用 CPS 风格或 GADT 包裹来编写：惰性 `filter :: (a -> Bool) -> Vec n a -> exists m. Vec m a`。 本文介绍的编码可用于实现 GHC 提案中的许多激励性例子，包括惰性 `filter`。然而，当我开始这个项目时，我使用的是一个外部包中的向量，该包没有导出其构造函数，为了测试惰性 `filter`，我还需要一个惰性函数来创建向量，因此这成了本文的主要例子。我最终并不需要那么多现成的向量函数，因此本文定义了自己的向量，但例子保留了下来。所以，我不展示惰性 `filter` 函数，而是用函数 `lazyVecFromList :: [a] -> Exists m (Vec m a)` 来演示这种编码的好处，该函数惰性地将列表转换为向量。 遗憾的是，这种编码在定义具有存在量化的类型的光学时效果不佳，我继续寻找，发现了一种不同的技术，使得这样的光学成为可能。 但在我们深入这些技术之前，让我们先看看为什么不能使用 CPS 风格或 GADT 包裹来编写惰性 `vecFromList`。我们将推导第二种选择，但首先我们需要启用一些语言扩展并导入一些东西。我还定义了自己的 `(.)`，因为 `linear-base` 中的版本并不像我想要的那么具有多态性。 导入和语言扩展 `` {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE LinearTypes #-} {-# LANGUAGE TypeAbstractions #-} {-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -Wall -Wno-missing-signatures -Wno-unused-top-binds -Wno-orphans #-} {- HLINT ignore "Use first" -} {- cabal: ghc-options: -Wall default-language: GHC2024 build-depends: base, linear-base, lens, mtl, profunctors, kind-apply, -} {- project: with-compiler: ghc-9.12.3 index-state: 2026-03-18T08:38:52Z semaphore: True -} import Control.Functor.Linear (Monad (..)) import Control.Functor.Linear qualified as Control import Control.Lens qualified as Lens import Control.Monad.Except import Control.Monad.State.Lazy qualified as NL import Control.Optics.Linear import Data.Bifunctor.Linear import Data.Char import Data.Functor qualified as NL import Data.Functor.Identity import Data.Functor.Linear import Data.Kind import Data.Maybe import Data.PolyKinded hiding (Nat) import Data.Profunctor.Kleisli.Linear import Data.Type.Equality import Data.Unrestricted.Linear import Prelude.Linear hiding (Any, any, forget, fst, ($), (.)) import Prelude.Linear qualified as L hiding (Any, any) import Unsafe.Coerce (unsafeCoerce) import Unsafe.Linear qualified as Unsafe import Prelude (($)) import Prelude qualified as NL -- Multiplicity polymorphic version of `(.)` which works in most non-linear code as well. (.) :: forall b c a m n. (b %m -> c) %n -> (a %m -> b) %m -> a %m -> c (.) f g x = f (g x) infixr 9 . forget :: (a %1 -> b) %m -> a -> b forget f x = f x (<&>) :: Functor f => f a %1 -> (a %1 -> b) -> f b (<&>) = flip (<$>) main = print $ demo2 @Int `` 需要记住的主要事情是，我们使用 `L` 和 `NL` 来区分线性和非线性函数（在需要时）。来自 `linear-base` 的函数通常不加限定。 现在我们可以定义向量和 `vecFromList`： `` data Nat = Zero | Succ Nat data Vec n a where VNil :: Vec Zero a VCons :: a %1 -> Vec n a %1 -> Vec (Succ n) a data SomeVec a where SomeVec :: forall n a. Vec n a %1 -> SomeVec a vecFromList :: [a] -> SomeVec a vecFromList [] = SomeVec VNil vecFromList (a : as) = vecFromList as & \(SomeVec aVec) -> SomeVec $ VCons a aVec `` 如果你从未见过在 `VCons` 的定义中使用 `%1`，现在可以忽略它们。这将该构造函数的字段标记为线性，稍后会详细解释。 在每次使用 `vecFromList` 的地方模式匹配 `SomeVec aVec` 不仅繁琐，而且使函数在列表的长度上变得严格。然而我们别无选择。`SomeVec $ vecFromList as & \\(SomeVec @n aVec) -> VCons a aVec` 无法被类型化，因为与解包的 `SomeVec` 绑定的 `n` 会逃出其作用域。 CPS 变体出于类似的原因也无济于事：在 `vecFromList` 递归应用之前无法应用 continuation。 正如存在类型提案的作者在 `filter` 函数中指出的，不可能在 GHC 当前的类型系统中定义惰性版本。 *所以我们得绕过它。* ## 把存在类型拴起来 本质上，我们*必须*让向量的长度在 `vecFromList` 的返回类型中可见。GHC 只提供全称量化给这样的类型变量，但不知何故，我们需要让 `vecFromList` 的调用者无法为这个变量选择特定的类型，从而让 `vecFromList` 可以做出这个选择。为了实现这一点，我们从代理类型 `Fresh` 开始，它只能以存在类型作为参数引入。 `` data Fresh0 a = Fresh0 -- consider the constructor hidden unpack0 :: (forall a. Fresh0 a -> r) -> r unpack0 f = f Fresh0 `` 这个代理将作为一个证明见证，表明关联的类型变量在程序中的其他地方被“存在量化”了。`vecFromList` 的类型变成了 `forall n a. [a] -> Fresh n -> Vec n a`，存在量化的负担被推给了调用者。这有效地将存在类型的作用域扩大到调用者（甚至其调用者）决定使用 `unpack0` 引入存在类型的地方。通过将存在量化见证作为参数传递给最终使用它的地方，我们创建了这条牵绳，本文和这种编码也得名于此。 现在，我们需要一种方法让 `vecFromList` 为 `n` 选择一个类型。由于它是一个具体类型（在调用点实例化），我们唯一的选择是 `unsafeCoerce`。 暂时将这种方法的危险放在一边，给定一个类型为 `Fresh n` 的值，我们应该允许将 `n` 强制转换为其他类型 `b`。这可以通过提供类型相等见证（来自 `Data.Type.Equality`）来实现。 我们得到： `` newtype Fresh1 a = Fresh1 (forall b. a :~: b) -- consider the constructor hidden unpack1 :: (forall a. Fresh1 a -> r) -> r unpack1 f = f (Fresh1 $ unsafeCoerce Refl) `` 使用 `Data.Type.Equality.castWith`，我们现在可以对任何拥有 `Fresh a` 的 `a` 实例执行不安全强制转换！现在我们只需要从那个句子中去掉“不安全”这个词。 为了使这安全，我认为确保这样的强制转换总是针对每个 `Fresh` 值指向相同类型就足够了。在我们使用见证之前，不可能有任何类型 `a` 的值存在，因为它已经被存在量化了。由 `a` 参数化的类型 `f` 的值可以存在，但这样的值必须独立于 `a`，原因相同。因此，只要只存在一个 `a ~ b`，用选择的 `b` 替换 `a` 就应该是安全的。 实现这一点的第一步是 (1) 隐藏 `Fresh` 的构造函数，并且 (2) 要求传递给 `unpack1` 的 continuation 线性地使用 `Fresh` 值，像这样： `` newtype Fresh a = Fresh (forall b. a :~: b) -- consider the constructor hidden type Exists a b = Fresh a %1 -> b -- conceptually this should be `forall a. Fresh a %1 -> b`, but that prevents `a` from being used in `b` and defeats the entire point. unpack2 :: (forall a. Exists a r) %1 -> r unpack2 f = f L.$ Fresh $ unsafeCoerce Refl pack :: forall b r a. (a ~ b => r) %1 -> Exists a r pack r (Fresh (Refl :: a :~: b)) = r `` `type Exists a b = Fresh a %1 -> b` 中的 `%1` 要求该函数是线性的。这意味着编译器将验证，如果函数的结果被完全消耗，那么这样的函数将恰好消耗该参数一次。这些注解也可以用在 GADT 构造函数（如 `VCons`）的类型中。在这种情况下，当你在线性函数中匹配该构造函数的模式时，这些字段中的值必须被线性地使用。 函数 `pack` 是必需的，用来替代 `Data.Type.Equality.castWith`，因为用户不能再通过模式匹配 `Fresh` 值来获得 `a :~: b`。 然而，这并不足以确保 `pack` 强制转换总是针对每个 `Fresh` 值指向相同类型。下面的例子展示了这如何被用来生成不正确的类型等式。 `` data GADT a where Int :: GADT Int Char :: GADT Char data Wrapper where Wrapper :: forall a. (Bool -> GADT a) %1 -> Wrapper wrapper :: Wrapper wrapper = unpack2 ( \(fresh :: Fresh a) -> Wrapper @a (\b -> if b then pack @Int Int fresh else pack @Char Char fresh) ) `` `` conflict :: Int :~: Char conflict = wrapper & \(Wrapper @a (f :: Bool -> GADT a)) -> let int = f True :: GADT a char = f False :: GADT a in trans @Int @a @Char -- trans :: (a :~: b) -> (b :~: c) -> a :~: c ( case int of Int -> Refl :: Int :~: a ) ( case char of Char -> Refl :: a :~: Char ) `` 本质上，`Fresh` 值通过 `Wrapper` 逃逸了它的线性作用域。因为 `Wrapper` 在 `unpack` 调用之外不需要被线性地消耗，我们可以两次使用嵌入的函数（从而使用内部捕获的 `Fresh` 值）。我认为防止这种情况的技巧很巧妙：我们必须要求 `unpack` 产生的 `r` *可以*被线性地复制，即它是 `Dupable`（https://hackage-content.haskell.org/package/linear-base-0.7.0/docs/Data-Unrestricted-Linear.html#t:Dupable）的一个实例。 要理解为什么，我们必须意识到三件事： 1. `Fresh` 值只能被*线性*字段捕获（如 `Wrapper` 中的 `(Bool -> GADT a)`）。否则，`Fresh` 值将不会被线性地消耗。 2. 一个类型如果是 `Dupable`，那么只有当该字段也是 `Dupable` 时才能包含一个线性字段，但函数不是（即使它的输入是 `Bounded`，因为找出不同的输出需要多次应用该函数）。 3. `Fresh` 也不是 `Dupable`，因此由于 1 和 2，它不能出现在 `Dupable` 值中。 因此，在由 `unpack` 产生之后复制一个 `Dupable` 值是安全的，于是我们得到了 `unpack` 的最终版本： `` unpack :: Dupable r => (forall a. Exists a r) %1 -> r unpack f = f L.$ Fresh $ unsafeCoerce Refl `` 那么现在这完全安全了吗？嗯，只有当 `Dupable r` 是 `Dupable` 的一个忠实实例时。如果你为一个线性捕获的函数将 `dup` 实现为 `error "this is never used anyway"`，你就能绕过它，并且你仍然可以像之前一样编写 `conflict` 表达式。我们可以让 `unpack` 调用 `dup` 来验证这不会发生，但这会使它变得非常严格，以至于对实现惰性 `vecFromList` 毫无用处。 或者，我们可以定义一个封闭类型族 `ClosedDupable`，它使用类型的泛型表示（如 `GHC.Generics.Rep`）来检查它是否包含线性函数字段。然而，目前 `Rep` 不能为 GADT 定义，所以这将严重限制可以从 `unpack` 逃逸的值。这可以通过使用来自 `kind-generics` 的 `RepK`（https://hackage.haskell.org/package/kind-generics-0.5.0.0/docs/Generics-Kind.html#t:RepK）来解决，但缺点是这需要用户使用模板 Haskell 来派生 `RepK` 或手动定义它，我不认为这是值得的额外安全性。 我考虑的另一个替代方案是利用 `Fresh` 值的属性，即 `Fresh a` 中的 `a` 总是存在的。我们可以通过使用类似的类型族来检查上文提到的泛型表示，从而防止 GADT 捕获它。这可能是当你确实需要在 `r` 中有一个函数作为线性字段时的好方案，但总的来说，我认为这是一个比 `Dupable` 更严格的限制。 总之，我认为 `unpack` 只有在与其他不安全函数（在 `Dupable` 的实现中）结合使用时才不安全。对我而言，这是可以接受的。有一些更安全的替代方案，但它们需要用户付出更多努力，并不值得成本。 现在让我们继续，最终定义一个惰性 `vecFromList`： `` lazyVecFromList0 :: Dupable a => [a] %m -> Exists n (Vec n a) lazyVecFromList0 [] n = pack @Zero VNil n lazyVecFromList0 (a : as) n = -- 这个 `unpack` 实际上解包了递归调用产生的 `Vec`，而不是下面立即打包的那个 unpack -- TypeAbstractions 语法 ( \ @predN predN -> pack @(Succ predN) (VCons a L.$ lazyVecFromList0 as predN) n ) `` 手动的 `pack` 和 `unpack` 增加了显著的冗长，但我认为每次使用都是必要的。`pack` 是必需的，因为 `VNil` 和 `VCons` 都不会产生任意长度的向量，并且我们不能移除 `unpack`，因为我们不能使用同一个 `Fresh` 值来强制转换 `VCons`。 然而，正如你将在下一个代码块中看到的，我们可以抽象掉一些冗长之处： `` repack :: forall f n a. Dupable a => (forall m.