Gibt es eine Möglichkeit, die Funktion entpacken auf Showable in GHC Haskell darzustellen?

Question

Ich habe eine Art sendefähiges wie folgt benannt:

{-# LANGUAGE ExistentialQuantification #-} 
    {-# LANGUAGE ExplicitForAll #-} 
    data Showable = forall a . Show a => Showable a 

dann eine Funktion zu machen, die es packt trivial ist. Ich muss nur schreiben:

Es scheint jedoch unmöglich, die Umkehrfunktion zu erstellen, die die Daten von Showable entpacken würde. Wenn ich versuche, einfach umzukehren, was ich für pack geschrieben habe und schreibe:

unpack :: exists a . Show a => Showable -> a 
    unpack (Showable x) = x 

dann bekomme ich einen Fehler von GHC.

Ich habe in den Dokumenten auf GHC Language Erweiterungen nachgesehen und es scheint keine Unterstützung für das Schlüsselwort exists. Ich habe gesehen, dass es in einigen anderen Haskell-Compilern möglich sein könnte, aber ich würde es auch gerne in GHC machen.

Lustigerweise kann ich immer noch Muster auf Showable Muster und extrahieren Sie die Daten aus dem Inneren auf diese Weise. Also könnte ich den Wert auf diese Weise herausholen, aber wenn ich eine Pointfree-Funktion mit Showable machen wollte, dann müsste ich entpacken.

Gibt es also eine Möglichkeit, das Entpacken in GHC's Haskell zu implementieren, vielleicht mit Type Families oder einer anderen arkanen Magie, die GHC-Erweiterungen sind?

Answer 1

Ihre unpack, wie Sie eingegeben haben, kann nicht geschrieben werden. Der Grund dafür ist, dass die existenzielle Variable den Bereich der Musterübereinstimmung "verlässt" und es keine Möglichkeit gibt, dieses Verhalten zu verfolgen. Zitiert die Dokumentation:

data Baz = forall a. Eq a => Baz1 a a 
     | forall b. Show b => Baz2 b (b -> b) 

Wenn Mustervergleich, wobei jede Musterübereinstimmung für jede Existenz Typen Variable einen neuen, eindeutigen, Typen einführt. Diese Typen können nicht mit einem anderen Typ vereinheitlicht werden, noch können sie aus dem Bereich der Musterübereinstimmung entkommen. Zum Beispiel sind diese Fragmente falsch:

f1 (MkFoo a f) = a 

Was ist das "a" in der Ergebnisart? Natürlich meinen wir das nicht:

f1 :: forall a. Foo -> a -- Wrong! 

Das ursprüngliche Programm ist einfach falsch. Hier ist eine andere Art von Fehler

f2 (Baz1 a b) (Baz1 p q) = a==q 

Es ist in Ordnung zu sagen a==b oder p==q, aber a==q falsch ist, weil es die zwei verschiedene Arten die sich aus den beiden Baz1 Konstrukteurs entspricht.

Sie können jedoch schreiben die unpack Typ äquivalent, so dass die existentielle tut nicht Flucht:

{-# LANGUAGE ExistentialQuantification #-} 
{-# LANGUAGE RankNTypes    #-} 

module Lib where 

data Showable = forall a. Show a => Showable a 

pack :: Show a => a -> Showable 
pack = Showable 

unpack :: Showable -> (forall a. Show a => a -> r) -> r 
unpack (Showable a) a2r = a2r a