什么是printtype函数中的"proxy a"?

Joe*_*hoi 6 haskell

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

printtype :: Showtype a => proxy a -> IO ()
Run Code Online (Sandbox Code Playgroud)

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

Jor*_*ano 6

通常,类型的代理a是某些数据类型,Proxy a其值不包含任何信息.因此,该值作为其类型的见证传递(用于类型推断/类型检查目的).在这种情况下proxy,is不是特定的数据类型,而是具有种类的类型变量* -> *.意思是你可以使用任何你想要的代理,但这个想法仍然是一样的.

功能是,

printtype :: Showtype a => proxy a -> IO ()
Run Code Online (Sandbox Code Playgroud)

它应该"打印一个类型",但函数应用于值而不是类型.因此,不是传递一个实际的类型参数,a而是传递某种类型的参数proxy a,其实际值是无关紧要的(通常是不Proxy包含任何信息的数据类型).

查看一个简单类型的实例,例如pair,

instance (Showtype a, Showtype b) => Showtype '(a,b) where
  showtype _ = showtuple' [
    showtype (Proxy :: Proxy a),
    showtype (Proxy :: Proxy b)]
Run Code Online (Sandbox Code Playgroud)

首先注意如何showtype忽略它的论点,

showtype _ = ...
Run Code Online (Sandbox Code Playgroud)

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

showtype (Proxy :: Proxy a)
showtype (Proxy :: Proxy b)
Run Code Online (Sandbox Code Playgroud)

proxy这里选择的是Proxy不包含任何信息的数据类型.在一种情况下,它是类型Proxy a而在另一种情况下Proxy b.函数showtype已定义,因此您也可以使用eg来调用它

showtype ([] :: [a])
showtype ([] :: [b])
Run Code Online (Sandbox Code Playgroud)

不是说,如果你在路过a而不是proxy a,这里你能够构建的唯一值(对于泛型a)将是undefined.如果它的评估被迫,它将破坏你的计划.