捕获类型类字典

Question

下面是可以愉快编译的代码（添加constraints包后）。Foo1和Foo2是 的两个替代定义Foo，我可以合理地编写f1它们f2。

不过我觉得 Foo3也有道理。但我不知道怎么写f3。在我看来，Haskell 应该在Foo3构造函数内存储一个指向类型类字典的指针，用于创建a时传递的任何内容Foo3，所以我应该能够调用silly. 由于silly只是返回String，现在是否已被删除并不重要a，我应该能够愉快地调用silly构造函数中存储的字典所指向的Foo3。

我的推理正确吗？如果是这样，我该怎么写f3。或者，我是否错过了一些东西，是否有充分的理由为什么我需要其中一个或Dict这里Proxy，因为没有它们我就没有足够的信息？

{-# LANGUAGE ScopedTypeVariables #-}

import Data.Constraint (Dict(Dict), withDict)
import Data.Proxy (Proxy)

data Alice

class C a where
    silly :: String

instance C Alice where
    silly = "Silly Alice"

data Foo1 where
    Foo1 :: Dict (C a) -> Foo1

f1 :: Foo1 -> String
f1 (Foo1 (dict :: Dict (C a))) = withDict dict $ silly @a

data Foo2 where
    Foo2 :: C a => Proxy a -> Foo2

f2 :: Foo2 -> String
f2 (Foo2 (_ :: Proxy a)) = silly @a

data Foo3 where 
    Foo3 :: C a => Foo3

mkFoo3 :: forall a. C a => Foo3
mkFoo3 = Foo3 @a 

f3 :: Foo3 -> String
f3 = undefined

Answer 1

打开足够的扩展，并且有足够新的 GHC（9.2 在这里似乎足够新，也许稍微旧的也可以工作），以下工作：

f3 (Foo3 @_ @a) = silly @a

@_你问那是什么？有一个隐含的类型参数，a我们想要忽略的类型。或者，您可以使用NoPolyKinds扩展名并删除@_.