haskell - `Data.Proxy` 的目的是什么？

Question

来自Data.Proxy的

代理看起来不过是区区

data Proxy s

我什么时候需要这样一个无人居住的类型，或者更确切地说，它能让我做什么，否则我无法做到，与其他方法相比，它什么时候简化了事情，以及它在实践中如何使用？

Answer 1

我经常使用 Proxy 与其犯罪伙伴 Data.Tagged，如 documentation表示，以避免不安全地传递虚拟参数。

例如，

data Q

class Modulus a where
  value :: Tagged a Int

instance Modulus Q where
  value = Tagged 5

f x y = (x+y) `mod` (proxy value (Proxy::Proxy Q))

没有Tagged的另一种编写方式是

data Q

class Modulus a where
  value :: Proxy a -> Int

instance Modulus Q where
  value _ = 5

f x y = (x+y) `mod` (value (Proxy::Proxy Q))

在这两个示例中，我们还可以删除 Proxy 类型，并仅使用 undefined::Q 传入幻像类型。然而，使用 undefined 是 generally frowned upon因为如果评估该值，可能会随之而来的问题。考虑以下因素:

data P = Three
       | Default

instance Modulus P where
  value Three = 3
  value _ = 5

f x y = (x+y) `mod` (value (undefined :: P))

这是编写实例的有效方法如果我使用默认构造函数，程序会崩溃，因为我正在尝试评估未定义.因此，Proxy 类型为幻像类型提供了类型安全性。

编辑

正如 Carl 指出的，Proxy 的另一个好处是能够拥有 * 之外的幻像类型。例如，我正在搞乱类型列表:

{-# LANGUAGE KindSignatures, DataKinds, TypeOperators, 
    MultiParamTypeClasses, PolyKinds, FlexibleContexts, 
    ScopedTypeVariables #-}

import Data.Tagged
import Data.Proxy

class Foo (a::[*]) b where
  foo:: Tagged a [b]

instance Foo '[] Int where
  foo = Tagged []

instance (Foo xs Int) => Foo (x ': xs) Int where
  foo = Tagged $ 1 : (proxy foo (Proxy :: Proxy xs)) -- xs has kind [*]

toUnary :: [Int]
toUnary = proxy foo (Proxy :: Proxy '[Int, Bool, String, Double, Float])

但是，由于 undefined 是一个值，因此其类型必须具有 * 或 # 类型。如果我尝试在示例中使用 undefined ，我需要类似 undefined::'[Int, Bool, String, Double, Float] 的内容，这会导致编译错误:

Kind mis-match
    Expected kind `OpenKind',
    but '[Int, Bool, String, Double, Float] has kind `[*]'

有关种类的更多信息，请查看 this出去。鉴于错误消息，我希望能够编写 undefined::Int#，但我仍然收到错误 Couldn't match kind # against *，所以显然这是一个糟糕的 GHC 错误消息，或者是我的一个简单错误。