haskell - printtype函数中的 "proxy a"是什么？

Question

当我尝试使用 Type.Showtype 中的 printtype 函数时。我发现 printtype 的类型签名是:

printtype :: Showtype a => proxy a -> IO ()

这里令人困惑的是proxy a的类型，它似乎来自Data.Proxy ，但是我找不到 proxy 的任何定义，很明显它与 Proxy 不同，因为 proxy 的第一个字母是小写的。而且我知道 Haskell 中数据类型的第一个字母不能是小写，所以 proxy a 不是类型，但为什么它可以出现在类型签名中？

Answer 1

一般来说，类型a的代理是某种数据类型Proxy a，其值不携带任何信息。因此，该值被传递作为其类型的见证(用于类型推断/类型检查目的)。在这种情况下，proxy 不是特定的数据类型，而是类型为 * -> * 的类型变量。这意味着您可以使用任何您想要的东西作为代理，但想法保持不变。

函数是，

printtype :: Showtype a => proxy a -> IO ()

它应该“打印类型”，但函数应用于值而不是类型。因此，您不是传递 a 类型的实际参数，而是传递某种类型 proxy a 的参数，其实际值是不相关的(通常是数据类型 >代理不包含任何信息)。

查看简单类型的实例，例如对，

instance (Showtype a, Showtype b) => Showtype '(a,b) where
  showtype _ = showtuple' [
    showtype (Proxy :: Proxy a),
    showtype (Proxy :: Proxy b)]

首先注意 showtype 如何忽略其参数，

showtype _ = ...

代理的值无关紧要，重要的是我们正在打印类型(a,b)。然后我们调用 showtuple'，它用于打印给定列表的类型元组(任意长度)，并打印每个组件的类型。对于我们拥有的每个组件，

showtype (Proxy :: Proxy a)
showtype (Proxy :: Proxy b)

此处选择的代理是数据类型Proxy，不包含任何信息。在一种情况下，它的类型为Proxy a，而在另一种情况下，它的类型为Proxy b。定义了函数 showtype ，以便您也可以使用例如调用它

showtype ([] :: [a])
showtype ([] :: [b])

并不是说，如果您传递 a 而不是 代理 a，这里是您能够构造的唯一值(对于通用 a) 将是未定义。如果它的评估被强制，它会破坏你的程序。