以存在类型解包存在

Question

我试着写了下面的代码：

{-# LANGUAGE GADTs #-}

module V where

data V a where
  V :: (c -> a) -> V a

down :: V (V a) -> V a
down (V f) = V $ \(c,d) -> case f c of
  V f' -> f' d

然后 GHC 回答了 type variable `c' would escape its scope。

我明白为什么它不能编译：它使用 case.

中存在的隐藏类型
但实际上该类型仍被 V隐藏。所以我认为 down 本质上没有问题。

有没有办法编写可编译的down函数？

Answer 1

这是基本问题：f 可以查看 c 并使用 c 的值来确定要在其存在中隐藏哪种类型。例如：

v :: V (V Int)
v = V $ \p -> case p of
     False -> V (id :: Int -> Int)
     True  -> V (fromEnum :: Char -> Int)

所以如果我们调用 down v，d 需要同时是有效的 Int 和有效的 Char！为了能够提供一个如此多变的存在，您需要确保它的参数可以采用它可能需要的所有类型。

newtype Forall = Forall (forall a. a)

down :: V (V a) -> V a
down (V f) = V $ \(c, d_) -> case f c of
    V f' -> case d_ of
        Forall d -> f' d

Answer 2

在 Haskell 中，我找不到使您的代码正常工作的简单方法。

不过我觉得很有趣，您的想法确实适用于具有完全依赖类型的语言，例如 Coq（可能还有 Agda、Idris 等）。

正如 Daniel Wagner 指出的那样，主要的症结在于 f 产生的类型可能取决于 c 的值，因此原始代码中的 (c,d) 对应该是 依赖对.

对于它的价值，下面是我们如何在 Coq 中做到这一点。

请注意，这不涉及像forall a. a这样的无人居住类型。

(* An existential type, under an impredicative encoding *)
Inductive V (A: Type): Type :=
  Vk : forall (B: Type), (B -> A) -> V A
.

(* The usual "identity to equivalence" *)
Definition subst {A B: Type} (p: A = B) (x: A): B :=
   match p with
   | eq_refl => x
   end .

(* The main function.

   Essentially, we want to turn
     Vk B (fun b => Vk C g)
   into
     Vk (B*C) (fun (b,c) => g c)
   but both C and g can depend on (b:B), so (B*C)
   should be a Sigma type {b:B & ty b}.

*)
Definition down (A: Type) (x: V (V A)): V A :=
   match x with
   | Vk B f => let
      ty (z: V A): Type := match z with | Vk C g => C end
      in Vk A {b:B & ty (f b)} (fun w =>
         match w with
         | existT b y =>
            match f b as o return ty (f b) = ty o-> A with
            | Vk C g => fun (h: ty (f b) = C) =>
               g (subst h y)
            end eq_refl
         end )
   end .

Answer 3

感谢 chi 的另一个很好的回答！

我重写了 Agda 的代码，实际上它确实可以编译。作为上述答案的附加说明，我将代码放在这里。

module down where

open import Level
open import Data.Product

data V {ℓ} (A : Set ℓ) : Set (suc ℓ) where
  Vk : {B : Set} → (B → A) → V A

down : ∀ {ℓ} {A : Set ℓ} → V (V A) → V A
down {ℓ} {A} (Vk {B} f) = Vk go where
  ty : V A → Set
  ty (Vk {C} _) = C
  go : Σ B (λ b → ty (f b)) → A
  go (b , c) with f b
  go (b , c) | Vk {C} g = g c

以存在类型解包存在

Unpack Existentials in Existential Type

haskell

types

gadt

existential-type