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

Question

Proxy从Data.Proxy似乎只是一个单纯的

data Proxy s

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

Answer 1

正如文档所示,我经常Proxy与犯罪伙伴一起使用,以避免不安全地传递虚假参数.Data.Tagged

例如,

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 通常是不受欢迎的,因为如果对该值进行评估,可能会出现问题.考虑以下:

data P = Three
       | Default

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

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

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

编辑

正如卡尔指出的那样,另一个好处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是一个值,它的类型必须是kind *或#.如果我试图undefined在我的例子中使用,我需要类似的东西undefined :: '[Int, Bool, String, Double, Float],这会导致编译错误:

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

有关种类的更多信息,请查看此内容.鉴于错误消息,我希望能够写入undefined :: Int#,但我仍然得到错误Couldn't match kind # against *,所以显然这是一个GHC错误消息,或者我的一个简单错误的情况.