Gibt es einen solchen "universellen" Haskell-Typ?

Question

Ich Suche eine Haskell Typ A mit der folgenden Eigenschaft (mit exotischen GHC Erweiterungen ist in Ordnung mit mir ...): Für alle verfahrbaren t die folgenden beiden Typen sind isomorph:

forall a. C a => t a -> a 

und

t A -> A. 

In meinem speziellen Fall, C die folgende Klasse:

class Floating a => C a where 
    fromDouble :: Double -> a 

Mit anderen Worten, ich würde irgendwie mag die universelle Quantifizierung über alle Arten ein in Klasse C in den Typen A ziehen, so dass eine Funktion t A -> A gibt mir alle eine Funktion für zurück a. Also ich denke, ich bin für eine „universelle“ Instanz der Klasse C in einem gewissen Sinn suchen ...

Ich habe alle Arten von fancy Definitionen gelten für A, entlang der Linien von

newtype A = A (forall b. C b => b) 

oder

data A = forall b. C b => A b 

oder

newtype A = A (forall t b. (Traversable t, C b) => t b -> b), 

oder

data A = FromDouble Double | Plus A A | Tanh A | ... 

oder sogar

data A = A (forall t. Traversable t => t A -> A), 

und sie alle leicht Instanzen der Klasse C hergestellt werden können, aber sie haben nicht die Eigenschaft, ich brauche (oder zumindest ich sehe nicht, wie man diese Eigenschaft aus einer meiner obigen Definitionen).

an ungeraden Tagen ich überzeugt bin Typ A existiert einfach nicht, an geraden Tagen ich vom Gegenteil überzeugt bin ...

... so wäre jede Hilfe sehr geschätzt!

---

Um eine gewisse Motivation für meine Frage zu geben: Ich auf Edward Kmett's ad library für meine neural networks library stark bin Neigung, und in meinem ersten Versuch war ich für die automatische Differenzierung und Backpropagation seine Numeric.AD.Rank1.Kahn-Typ. Dies führte zu einer netten API, aber war weniger effizient als sein Reverse-Modus, der leider eine Quantifizierung wie in meiner Frage verwendet, um differenzierbare Funktionen zu kodieren.

Ich hatte gehofft, dass ich das Beste aus beiden Welten haben könnte - eine spezifische (abstrakte) Art plus Reverse-Modus-Effizienz.

Answer 1

Nehmen wir an, ein solcher "universeller" Typ A existiert.

Const() verfahrbar ist, damit wir einen Isomorphismus zwischen

forall a. C a => Const() a -> a 
-- and 
Const() A -> A 

dh bekommen zwischen (seit Const() a isomorph zu () und () -> b isomorph zu b)

forall a. C a => a 
-- and 
A 

Also, wenn jede A existiert, muss es isomorph zu forall a. C a => a sein.

Beachten Sie, dass dies der erste Versuch einer Lösung war - wenn das die Anforderungen nicht erfüllt, dann wird nichts.

---

nun in Ihrem speziellen Fall

forall a. C a => a 

grob Mittel, durch Definition von C (*) [Anmerkung: hier bin ich falsch "vergessen" die Floating a Super, Magin das ganze Argument viel mehr zerbrechlich]

forall a. (Double -> a) -> a 

, die isomorph zu Double:

iso :: Double -> forall a. (Double -> a) -> a 
iso x f = f x 
osi :: (forall a. (Double -> a) -> a) -> Double 
osi f = f id 

Der Beweis, dass das Obige wirklich ein Isomorphismus ist, ist nicht-trivial - ich denke, dass es einige Parameter wie in "Recursive types for free!" erfordert. (Folge von Yoneda? ... Kommentare willkommen!)

Also - wenn es eine Lösung gibt, für Ihre C, muss es A ~ Double sein, bis zu Isomorphie.

(*) Ich dehne die Dinge ein bisschen hier. Ich weiß nicht genau, wie man Haskells beschränkte Quantifizierung genau handhaben soll, deshalb nehme ich mir vor, das Wörterbuch explizit zu machen, auch wenn ich denke, es ist nicht genau dasselbe.