存储和检索某个类型的对象--有可能吗？如果是，怎么做？

Question

假设我有一些类型类型的Foo和一些数据类型FooInst，这是Foo的实例。

class Foo a where
  foo :: a -> String

data FooInst = FooInst String

instance Foo FooInst where
    foo (FooInst s) = s

现在，我想定义一种数据类型，它存储类型在Foo类型中的对象，并能够从该数据类型内部提取该对象并使用它。

我发现的唯一方法是使用GADT和Rank2Types语言扩展并定义如下数据类型：

data Container where
  Container :: { content :: Foo a => a } -> Container

但是，问题是，我不能使用content选择器从容器中获取内容：

cont :: Container
cont = Container{content = FooInst "foo"}

main :: IO ()
main = do
  let fi = content cont
  putStrLn $ foo fi

编译错误的结果

Cannot use record selector ‘content’ as a function due to escaped type variables
Probable fix: use pattern-matching syntax instead

但是当我将let ...行修改为

let Conainer fi = cont

我犯了一个很有趣的错误

My brain just exploded
I can't handle pattern bindings for existential or GADT data constructors.
Instead, use a case-expression, or do-notation, to unpack the constructor.

如果我再次尝试修改let ...行以使用case表达式

let fi = case cont of
           Container x -> x

我得到了一个不同的错误

Couldn't match expected type ‘t’ with actual type ‘a’
  because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
  a pattern with constructor
    Container :: forall a. (Foo a => a) -> Container,
  in a case alternative
  at test.hs:23:14-24

那么，，我如何存储一个分类的东西并取回它呢？

Answer 1

通过以下方式：

data Container where
    Container :: {content :: Foo a => a} -> Container

类型类约束甚至没有强制执行。那是

void :: Container
void = Container {content = 42 :: Int}

类型检查，即使42 :: Int不是Foo的实例。

但如果你改为：

data Container where
    Container :: Foo a => {content :: a} -> Container

1. 您不再需要Rank2Types语言扩展。
2. 类型类约束是强制的；因此，上面的void示例将不再进行类型检查。
3. 此外，您可以通过模式匹配在内容上调用foo (或任何其他带有签名Foo a => a -> ...的函数)： 容器{content = a} -> foo a的事例

Answer 2

例如

main :: IO ()
main = do
  case cont of
    Container fi -> putStrLn $ foo fi

您需要将存在类型字段fi的使用封装在一个表达式中，该表达式的类型不依赖于fi的类型；在这里，putStrLn $ foo fi具有IO ()类型。

这个示例非常无用，因为您对Container的Container字段所能做的唯一事情就是在它上调用foo，所以您最好在构造容器之前调用foo，并给出字段类型String。但是更有趣的是，如果Foo有像a -> a -> a这样的类型的操作，或者Container有多个包含相同存在量化变量的类型的字段，等等。