Haskell: Warum Proxy verwenden?

Question

In Haskell ist ein Proxy ein Typ-Zeuge-Wert, der es erleichtert, bestimmte Typen zu übergeben

data Proxy a = Proxy

Ein Beispiel dafür findet sich hier in json-schema:

class JSONSchema a where
  schema :: Proxy a -> Schema

so könntest du schema (Proxy :: Proxy (Int,Char)) verwenden, um herauszufinden, wie die JSON-Repräsentation für ein Int-Char-Tupel aussehen würde (wahrscheinlich ein Array).

---

Warum verwenden Leute Proxies? Es scheint mir, dass dasselbe mit

class JSONSchema a where
  schema :: Schema a

erreicht werden könnte, ähnlich wie beim Bounded-Typklasse funktioniert. Ich dachte zuerst, es könnte einfacher sein, das Schema eines bestimmten Werts zu erhalten, wenn man Proxies verwendet, aber das scheint nicht wahr zu sein:

{-# LANGUAGE ScopedTypeVariables #-}

schemaOf :: JSONSchema a => a -> Schema a

schemaOf (v :: x) = schema (Proxy :: Proxy x)  -- Mit proxy

schemaOf (v :: x) = schema :: Schema x         -- Mit `:: a`
schemaOf _ = schema                            -- Noch einfacher mit `:: a`

Außerdem könnte man sich Sorgen machen, ob die Proxy-Werte tatsächlich zur Laufzeit beseitigt werden, was ein Optimierungsproblem darstellt, das nicht vorhanden ist, wenn man den :: a-Ansatz verwendet.

Wenn der :: a-Ansatz, wie von Bounded angewendet, das gleiche Ergebnis mit kürzerem Code und weniger Sorgen um Optimierung erzielt, warum verwenden Leute dann Proxies? Was sind die Vorteile von Proxies?

---

EDIT: Einige Antworten und Kommentatoren wiesen zu Recht darauf hin, dass der :: a-Ansatz den data Schema = ...-Typ mit einem "nutzlosen" Typenparameter befleckt - zumindest aus der Sicht der reinen Datenstruktur selbst, die den a nie verwendet (siehe hier).

Der Vorschlag besteht darin, stattdessen den Phantomtyp Tagged s b zu verwenden, der es ermöglicht, die beiden Aspekte voneinander zu trennen (Tagged a Schema kombiniert den nicht-parametrischen Schema-Typ mit einer Typvariable a), was streng besser ist als der :: a-Ansatz.

Also sollte meine Frage besser lauten Was sind die Vorteile von Proxies gegenüber dem tagged-Ansatz?

Answer 1

Zwei Beispiele, eines, in dem Proxy notwendig ist, und eines, in dem Proxy die Typen grundsätzlich nicht verändert, aber ich neige dazu, es trotzdem zu verwenden.

Proxy notwendig

Proxy oder ein ähnlicher Trick ist notwendig, wenn es einen Zwischentyp gibt, der nicht in der normalen Typsignatur aufgedeckt ist, den Sie dem Verbraucher ermöglichen möchten, anzugeben. Vielleicht ändert der Zwischentyp die Semantik, wie z.B. read . show :: String -> String. Mit aktivierten ScopedTypeVariables würde ich schreiben

f :: forall proxy a. (Read a, Show a) => proxy a -> String -> String
f _ = (show :: a -> String) . read

> f (Proxy :: Proxy Int) "3"
"3"
> f (Proxy :: Proxy Bool) "3"
"*** Exception: Prelude.read: no parse

Der Proxy-Parameter ermöglicht es mir, a als Typparameter freizulegen. show . read ist irgendwie ein dummes Beispiel. Eine bessere Situation könnte sein, wenn ein Algorithmus intern eine generische Sammlung verwendet, bei der der ausgewählte Sammlungstyp bestimmte Leistungseigenschaften hat, die der Verbraucher steuern möchte, ohne (oder ohne) sie zur Verfügung zu stellen oder den Zwischenwert zu empfangen.

Etwas wie das, was fgl Typen verwendet, wo wir den internen Data-Typ nicht freigeben möchten. (Vielleicht kann jemand einen geeigneten Algorithmus für dieses Beispiel vorschlagen?)

f :: Input -> Output
f = g . h
  where
    h :: Gr graph Data => Input -> graph Data
    g :: Gr graph Data => graph Data -> Output

Die Freilegung eines Proxy-Arguments würde es dem Benutzer ermöglichen, zwischen einer Patricia-Baum- und einer normalen Baumgraphimplementierung zu wählen.

Proxy als API- oder Implementierungsbequemlichkeit

Manchmal verwende ich Proxy als Werkzeug, um eine Typklasseninstanz auszuwählen, insbesondere in rekursiven oder induktiven Klasseninstanzen. Betrachten Sie die von mir verfasste MightBeA-Klasse in dieser Antwort über die Verwendung von verschachtelten Eithers:

class MightBeA t a where
  isA   :: proxy t -> a -> Maybe t
  fromA :: t -> a

instance MightBeA t t where
  isA _ = Just
  fromA = id

instance MightBeA t (Either t b) where
  isA _ (Left i) = Just i
  isA _ _ = Nothing
  fromA = Left

instance MightBeA t b => MightBeA t (Either a b) where
  isA p (Right xs) = isA p xs
  isA _ _ = Nothing
  fromA = Right . fromA

Die Idee ist es, ein Maybe Int aus, sagen wir, Either String (Either Bool Int) zu extrahieren. Der Typ von isA ist im Grunde genommen a -> Maybe t. Es gibt zwei Gründe, hier einen Proxy zu verwenden:

Erstens, es eliminiert Typsignaturen für den Verbraucher. Sie können isA (Proxy :: Proxy Int) aufrufen, anstelle von isA :: MightBeA Int a => a -> Maybe Int.

Zweitens ist es für mich einfacher, den induktiven Fall zu durchdenken, indem ich einfach den Proxy hindurchreiche. Mit ScopedTypeVariables könnte die Klasse ohne Proxy-Argument umgeschrieben werden; der induktive Fall würde implementiert als

instance MightBeA' t b => MightBeA' t (Either a b) where
  -- kein Proxy-Argument
  isA' (Right xs) = (isA' :: b -> Maybe t) xs
  isA' _ = Nothing
  fromA' = Right . fromA'

Dies ist in diesem Fall keine große Veränderung; wenn die Typsignatur von isA wesentlich komplexer wäre, wäre die Verwendung des Proxys eine große Verbesserung.

Wenn die Verwendung ausschließlich zur Implementierungsbequemlichkeit erfolgt, exportiere ich normalerweise eine Wrapper-Funktion, damit der Benutzer den Proxy nicht bereitstellen muss.

Proxy vs. Tagged

In all meinen Beispielen fügt der Typparameter aTagged a x zurückgeben würde, würde der Verbraucher es unweigerlich sofort entlaggen. Außerdem müsste der Benutzer den Typ von xdie Möglichkeit haben, _ in Typsignaturen zu verwenden...)

(Ich bin interessiert an anderen Antworten zu dieser Teilerfrage; Ich habe buchstäblich noch nie etwas mit Tagged geschrieben (ohne es in kurzer Zeit mit Proxy umzuschreiben) und frage mich, ob mir etwas entgeht.)

Answer 2

Letztendlich werden sie dieselbe Funktionalität ausführen und du siehst sie in entweder Stil. Manchmal ist es angemessen, deine Werte als Phantom-Tags zu kennzeichnen, manchmal möchtest du sie als untypisiert betrachten.

Die andere Alternative besteht darin, Data.Tagged zu verwenden.

class JSONSchema a where
  schema :: Tagged a Schema

Hier haben wir etwas vom Besten aus beiden Welten, da ein Tagged Schema die Phantomtypinformation enthält, die notwendig ist, um die Instanz aufzulösen, aber wir können diese Information mühelos mit unTagged :: Tagged s b -> b ignorieren.

Ich würde sagen, die ausschlaggebende Frage, in Bezug auf dieses Beispiel formuliert, sollte lauten "Möchte ich typisierte Operationen auf Schemas in Betracht ziehen?". Wenn die Antwort "nein" lautet, wirst du dich wahrscheinlich eher zu den Ansätzen Proxy oder Tagged neigen. Wenn die Antwort "ja" lautet, dann ist Schema a eine großartige Lösung.

Zu guter Letzt kannst du den Proxy-Ansatz (etwas umständlich) ohne jeglichen Import verwenden. Man sieht das manchmal im Stil

class JSONSchema a where
  schema :: proxy a -> Schema

Jetzt, da Proxy nur noch eine suggestiv benannte Typvariable ist, können wir etwas Ähnliches wie Folgendes tun

foo :: Schema
foo = schema ([] :: [X])

und überhaupt nichts importieren müssen. Ich persönlich denke jedoch, dass das eine ziemlich gepfuschte Arbeit ist, die Leser wahrscheinlich verwirren wird.