试图抽象出类型类，但类型变量转义

Question

我有一些类和它们的实例。该示例显示了一些无意义的类。它们的确切性质并不重要。

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}


class Foo a where
   foo :: a -> Int
class Bar a where
   bar :: a -> String

instance Foo Int where
   foo x = x
instance Foo String where
   foo x = length x

instance Bar Int where
   bar x = show x
instance Bar String where
   bar x = x

好的，现在我想创建一些存在类型，将这些类隐藏在某些数据类型外观后面，这样我就不必处理约束了。（我知道存在类型被认为是一种反模式，请不要向我解释这一点）。

data TFoo = forall a. Foo a => TFoo a
instance Foo TFoo where
  foo (TFoo x) = foo x
data TBar = forall a. Bar a => TBar a
instance Bar TBar where
  bar (TBar x) = bar x

显然那里有一些样板。我想把它抽象出来。

{-# LANGUAGE ConstraintKinds #-}
data Obj cls = forall o. (cls o) => Obj o

因此，我只有一种，由类型类参数化，而不是几种存在类型。到现在为止还挺好。

现在我如何执行操作Obj a？明显的尝试

op f (Obj a) = f a

失败，因为类型变量可能会转义。

existential.hs:31:18: error:
    • Couldn't match expected type ‘o -> p1’ with actual type ‘p’
        because type variable ‘o’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a pattern with constructor:
          Obj :: forall (cls :: * -> Constraint) o. cls o => o -> Obj cls,
        in an equation for ‘call’
        at existential.hs:31:9-13
    • In the expression: f k
      In an equation for ‘call’: call f (Obj k) = f k
    • Relevant bindings include
        k :: o (bound at existential.hs:31:13)
        f :: p (bound at existential.hs:31:6)
        call :: p -> Obj cls -> p1 (bound at existential.hs:31:1)
   |
31 | call f (Obj k) = f k
   |                  ^^^
Failed, no modules loaded.

我有点明白为什么会发生这种情况。但是对于像call foo和call bar类型变量这样的真正调用，它不会逃脱。我能说服编译器吗？也许我可以以某种方式表达类型u -> v where v does not mention u（这真的应该是 的类型f）？如果没有，还有什么其他方法可以处理这种情况？我想我可以用 TemplateHaskell 生成一些东西，但我仍然无法理解它。

Answer 1

你的代码工作正常；编译器只需要一些有关其类型的帮助。

Obj隐藏其内容的类型，这意味着它op的参数f必须是多态的（也就是说，它不能仔细检查它的参数）。打开RankNTypes：

op :: (forall a. cls a => a -> r) -> Obj cls -> r
op f (Obj x) = f x

您必须提供完整的类型签名，因为 GHC 无法推断更高级别的类型。

对这样的类进行存在性量化通常不是设计给定程序的最佳方式。