Existenzielle Quantifizierung in Funktionsrückgabetypen simulieren

Question

Manchmal komme ich auf die Notwendigkeit, Werte eines existentiell quantifizierten Typs zurückzugeben. Dies passiert am häufigsten, wenn ich mit Phantom-Typen arbeite (zum Beispiel, um die Tiefe eines ausgeglichenen Baumes darzustellen). AFAIK GHC hat keine Art von exists Quantifizierer. Es erlaubt nur existentially quantified data types (entweder direkt oder mit GADTs).

ein Beispiel geben, ich möchte Funktionen wie diese haben:

Bisher habe ich zwei mögliche Lösungen, die ich als Antwort hinzufügen werde, würde ich gerne wissen, wenn jemand etwas besser oder anders weiß.

Answer 1

Die Standardlösung besteht darin, einen existenziell quantifizierten Datentyp zu erstellen. Das Ergebnis wäre so etwas wie

{-# LANGUAGE ExistentialQuantification #-} 

data Exists1 = forall a . (Show a) => Exists1 a 
instance Show Exists1 where 
    showsPrec _ (Exists1 x) = shows x 

somethingPrintable1 :: Int -> Exists1 
somethingPrintable1 x = Exists1 x 

nun sein, kann man frei show (somethingPrintable 42) verwenden. Exists1 kann nicht newtype sein, ich nehme an, es ist, weil es notwendig ist, die bestimmte Implementierung von show in einem versteckten Kontextwörterbuch zu umgehen.

Für typsichere Vektoren, so könnte man fortfahren die gleiche Art und Weise fromList1 Implementierung zu erstellen:

{-# LANGUAGE GADTs #-} 

data Zero 
data Succ n 

data Vec a n where 
    Nil ::     Vec a Zero 
    Cons :: a -> Vec a n -> Vec a (Succ n) 

data Exists1 f where 
    Exists1 :: f a -> Exists1 f 

fromList1 :: [a] -> Exists1 (Vec a) 
fromList1 [] = Exists1 Nil 
fromList1 (x:xs) = case fromList1 xs of 
        Exists1 r -> Exists1 $ Cons x r 

Dieses gut funktioniert, aber der größte Nachteil ich sehe, ist der zusätzliche Konstruktor. Jeder Aufruf an fromList1 führt zu einer Anwendung des Konstruktors, die sofort dekonstruiert wird. Wie zuvor ist newtype nicht möglich für Exists1, aber ich denke, ohne irgendwelche Einschränkungen der Typklasse könnte der Compiler dies erlauben.

---

Ich schuf eine andere Lösung basierend auf Rang-N-Fortsetzungen. Es benötigt den zusätzlichen Konstruktor nicht, aber ich bin mir nicht sicher, ob eine zusätzliche Funktionsanwendung keinen ähnlichen Overhead hinzufügt. Im ersten Fall wäre die Lösung:

{-# LANGUAGE Rank2Types #-} 

somethingPrintable2 :: Int -> ((forall a . (Show a) => a -> r) -> r) 
somethingPrintable2 x = \c -> c x 

jetzt würde man somethingPrintable 42 show verwendet das Ergebnis zu erhalten.

Und für die Vec Datentyp:

-- | A helper function for creating existential values. 
exists3 :: f x -> Exists3 f r 
exists3 x = Exists3 (\c -> c x) 
{-# INLINE exists3 #-} 

-- | A helper function to mimic function application. 
(?$) :: (forall a . f a -> r) -> Exists3 f r -> r 
(?$) f x = unexists3 x f 
{-# INLINE (?$) #-} 

fromList3 :: [a] -> Exists3 (Vec a) r 
fromList3 []  = exists3 Nil 
fromList3 (x:xs) = (exists3 . Cons x) ?$ fromList3 xs 

Die wichtigsten Nachteile ich hier sehen, sind:

{-# LANGUAGE RankNTypes, GADTs #-} 

fromList2 :: [a] -> ((forall n . Vec a n -> r) -> r) 
fromList2 [] c  = c Nil 
fromList2 (x:xs) c = fromList2 xs (c . Cons x) 

-- Or wrapped as a newtype 
-- (this is where we need RankN instead of just Rank2): 
newtype Exists3 f r = Exists3 { unexists3 :: ((forall a . f a -> r) -> r) } 

fromList3 :: [a] -> Exists3 (Vec a) r 
fromList3 []  = Exists3 (\c -> c Nil) 
fromList3 (x:xs) = Exists3 (\c -> unexists3 (fromList3 xs) (c . Cons x)) 

dies kann ein bisschen besser lesbar mit ein paar Hilfsfunktionen vorgenommen werden

1. Mögliche Overhead mit der zusätzlichen Funktion Anwendung (Ich weiß nicht, wie viel der Compiler opt Imize dies).
2. Weniger lesbarer Code (zumindest für Personen, die nicht an Fortsetzungen gewöhnt sind).