haskell - 以存在类型解包存在

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。

我明白为什么它不能编译:它使用隐藏类型的存在 out of 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)

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

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