Какова цель "Data.Proxy"?

Когда мне нужен такой необитаемый тип или, вернее, то, что он позволяет, я не мог бы сделать иначе, когда он упрощает вещи по сравнению с другими подходами и как он используется на практике?

Ответ 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 для перехода в тип phantom. Однако использование 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 обеспечивает безопасность типов для типов phantom.

ИЗМЕНИТЬ

Как отметил Карл, еще одним преимуществом Proxy является возможность иметь тип phantom, отличный от *. Например, я возился с списками типов:

{-# 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 или простая ошибка с моей стороны.

Ответы

Ответ 1