haskell - 如何在存在包装器下应用任意函数？

Question

我正在尝试编写一个函数(此处称为 hide)，它可以在存在的包装器中应用足够多态的函数(或提升函数以处理具有隐藏类型的包装器；因此“隐藏”):

{-# LANGUAGE GADTs
           , RankNTypes
  #-}

data Some f
  where Some :: f a -> Some f


hide :: (forall a. f a -> g b) -> Some f -> Some g
hide f (Some x) = Some (f x)


data Phantom a = Phantom

cast :: Phantom a -> Phantom b
cast Phantom = Phantom

works :: Some Phantom -> Some Phantom
works = hide cast


doesn't :: Functor f => Some f -> Some f
doesn't = hide (fmap $ \x -> [x])
{-
foo.hs:23:17:
    Couldn't match type ‘b0’ with ‘[a]’
      because type variable ‘a’ would escape its scope
    This (rigid, skolem) type variable is bound by
      a type expected by the context: f a -> f b0
      at foo.hs:23:11-33
    Expected type: f a -> f b0
      Actual type: f a -> f [a]
    In the first argument of ‘hide’, namely ‘(fmap $ \ x -> [x])’
    In the expression: hide (fmap $ \ x -> [x])
    In an equation for ‘doesn't’: doesn't = hide (fmap $ \ x -> [x])
Failed, modules loaded: none.
-}


but :: Functor f => Some f -> Some f
but = hide' (fmap $ \x -> [x])
  where hide' :: (forall a. f a -> g [a]) -> Some f -> Some g
        hide' f (Some x) = Some (f x)

所以我非常理解为什么会这样； works表明 hide当返回类型与输入类型完全无关时确实有效，但在 doesn't 中我调用hide参数类型为 a -> [a] . hide应该去“选择”类型 a ( RankNTypes )，但 b通常是多态的。当b事实上取决于 a , a可能会泄漏。

但在我实际调用它的上下文中，a实际上并没有泄漏；我立即将其包装在 Some 中.事实上我可以写一个备用 hide'具体接受 a -> [a]功能和工作具有完全相同的实现，只是类型签名不同。

有什么方法可以输入实现 hide f (Some x) = Some (f x)以便它更普遍地工作？我真的对 a -> q a 类型的提升功能很感兴趣, 其中q是一些任意类型的函数；即我希望返回类型取决于 a ，但我不在乎它是如何做到的。可能存在 q a 的用例是一个常量(即返回类型不依赖于 a )，但我想它们会更加罕见。

显然，这个例子很愚蠢。在我的实际用例中，我有一个 GADT Schema a粗略地说代表外部类型系统中的类型； phantom 参数给出了一个 Haskell 类型，可以用来表示外部类型系统中的值。我需要那个幻影参数来保证所有类型的安全，但有时我会构造 Schema s 基于运行时数据，在这种情况下我不知道该参数类型是什么。

所以我似乎需要另一种与类型参数无关的类型。我希望使用像 Some 这样的简单存在性包装器，而不是制作(还)另一种并行类型。从 Schema 构造它, 并且能够提升 forall a. Schema a -> Schema b 类型的函数至 Some Schema -> Some Schema .因此，如果我遇到 XY 问题，我最好使用其他方式来绕过 Schema a对于未知 a ，那也可以解决我的问题。

Answer 1

正如David Young所说，你可以写

hide' :: (forall a. f a -> g (q a)) -> Some f -> Some g
hide' f (Some x) = Some (f x)

does :: Functor f => Some f -> Some f
does = hide' (fmap (:[]))

但不是让 hide 像 fmap 一样，你可以让它像 bind 一样:

hide'' :: (forall a. f a -> Some g) -> Some f -> Some g
hide'' f (Some x) = f x

does :: Functor f => Some f -> Some f
does = hide'' (Some . fmap (:[]))

但这有点样板化。

或者，更一般地

elim :: (forall a. f a -> c) -> Some f -> c
elim f (Some x) = f x