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

Question

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

36

Data.Proxy中的Proxy似乎只是一个简单的东西。

data Proxy s

我何时需要这种无人居住的类型，或者说，它能够让我做什么，否则我不能做什么，与其他方法比较简化了什么，以及它在实践中如何使用？

- danom

10

Proxy s 不是一个无人居住类型，它有一个单一的构造函数Proxy。 - Cactus

4

特别地，“Proxy”实际上被定义为“data Proxy s = Proxy”，而不是问题中写的“data Proxy s”。 - Tikhon Jelvis

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- crockeea · Accepted Answer

我经常使用代理（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是一个值，其类型必须具有*或#的种类。如果我尝试在我的示例中使用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 错误消息不够清晰，或者是我的一个简单错误。