Funzione Haskell che restituisce il tipo esistenziale

Question

È possibile scrivere una funzione Haskell che produce un tipo parametrizzato in cui il parametro del tipo esatto è nascosto? Cioè qualcosa come f :: T -> (exists a. U a)? Il tentativo evidente:

{-# LANGUAGE ExistentialQuantification #-} 

data D a = D a 

data Wrap = forall a. Wrap (D a) 

unwrap :: Wrap -> D a 
unwrap (Wrap d) = d 

fallisce la compilazione con:

Couldn't match type `a1' with `a' 
    `a1' is a rigid type variable bound by 
     a pattern with constructor 
     Wrap :: forall a. D a -> Wrap, 
     in an equation for `unwrap' 
     at test.hs:8:9 
    `a' is a rigid type variable bound by 
     the type signature for unwrap :: Wrap -> D a at test.hs:7:11 
Expected type: D a 
    Actual type: D a1 
In the expression: d 
In an equation for `unwrap': unwrap (Wrap d) = d 

So che questo è un esempio forzato, ma sono curioso di sapere se c'è un modo per convincere GHC che non mi interessa per il tipo esatto con cui è parametrizzato D, senza introdurre un altro tipo di wrapper esistenziale per il risultato di unwrap.

Per chiarire, io voglio la sicurezza di tipo, ma anche vorrebbe essere in grado di applicare una funzione dToString :: D a -> String che non si preoccupa di a (ad esempio perché appena estrae un campo di stringa da D) al risultato di unwrap. Mi rendo conto che ci sono altri modi per raggiungerlo (ad esempio definendo wrapToString (Wrap d) = dToString d) ma sono più interessato a sapere se esiste una ragione fondamentale per cui tale nascondimento sotto esistenza non è permesso.

Answer 1

Sì, è possibile, ma non in modo diretto.

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

data D a = D a 

data Wrap = forall a. Wrap (D a) 

unwrap :: Wrap -> forall r. (forall a. D a -> r) -> r 
unwrap (Wrap x) k = k x 

test :: D a -> IO() 
test (D a) = putStrLn "Got a D something" 

main = unwrap (Wrap (D 5)) test 

Non si può restituire un D something_unknown dalla vostra funzione, ma è possibile estrarre e subito passare ad un'altra funzione che accetta D a, come mostrato.  

Answer 2

Sì, è possibile convincere GHC che non si cura del tipo esatto con cui è parametrizzato D. È un'idea orribile.

{-# LANGUAGE GADTs #-} 

import Unsafe.Coerce 

data D a = D a deriving (Show) 

data Wrap where  -- this GADT is equivalent to your `ExistentialQuantification` version 
    Wrap :: D a -> Wrap 

unwrap :: Wrap -> D a 
unwrap (Wrap (D a)) = D (unsafeCoerce a) 

main = print (unwrap (Wrap $ D "bla") :: D Integer) 

Questo è ciò che accade quando eseguo che semplice programma:

e così via, fino a consumo di memoria porta il sistema.

I tipi sono importanti! Se elimini il sistema di tipi, elimini qualsiasi prevedibilità del tuo programma (ad esempio, qualsiasi cosa può accadere, incluso thermonuclear war o il famoso demons flying out of your nose).

---

Ora, evidentemente avete pensato che i tipi in qualche modo funzionassero in modo diverso. In linguaggi dinamici come Python, e anche in una laurea in linguaggi OO come Java, un tipo è in un certo senso una proprietà che un valore può avere. Quindi, i valori (di riferimento) non portano solo le informazioni necessarie per distinguere i diversi valori di un singolo tipo, ma anche informazioni per distinguere diversi (sotto) tipi. Questo è in molti sensi piuttosto inefficiente. – è una delle ragioni principali per cui Python è così lento e Java ha bisogno di una VM così grande.

In Haskell, i tipi non esistono in fase di esecuzione. Una funzione non sa mai di che tipo hanno i valori con cui sta lavorando. Solo perché il compilatore conosce tutti i tipi che avrà, la funzione non ha bisogno di qualsiasi conoscenza tale – il compilatore lo ha già codificato! (Cioè, a meno che non aggirare con unsafeCoerce, che, come ho dimostrato è come non sicuro come sembra.)

Se si vuole collegare il tipo come un “ proprietà ” ad un valore, è necessario farlo in modo esplicito e questo è ciò per cui ci sono quei wrapper esistenziali. Tuttavia, di solito ci sono modi migliori per farlo in un linguaggio funzionale. Qual è in realtà l'applicazione che volevi?

---

Forse è anche utile ricordare cosa significa una firma con risultato polimorfico. unwrap :: Wrap -> D a non significa “ il risultato è un po 'D a ... e il chiamante meglio non si preoccupa per il utilizzato ”. Questo sarebbe il caso in Java, ma sarebbe piuttosto inutile in Haskell perché non c'è nulla che tu possa fare con un valore di tipo sconosciuto.

Invece significa: per qualsiasi tipoa il chiamante, questa funzione è in grado di fornire un adeguato valore di D a. Ovviamente questo è difficile da fornire – senza ulteriori informazioni è altrettanto impossibile fare qualsiasi cosa con un valore di tipo sconosciuto dato. Ma se ci sono già a valori nei argomenti, o a è in qualche modo vincolata a una classe tipo (ad es fromInteger :: Num a => Integer -> a, allora è del tutto possibile e molto utile.

---

Per ottenere un String campo – indipendente a parametro – si può solo operare direttamente sul valore avvolto:

data D a = D 
    { dLabel :: String 
    , dValue :: a 
    } 

data Wrap where Wrap :: D a -> Wrap 

labelFromWrap :: Wrap -> String 
labelFromWrap (Wrap (D l _)) = l 

Per scrivere tali funzioni su più Wrap genericamente (con qualsiasi accessorio per etichette “ che non interessa a ”), utilizzare il polimorfismo di Rank2 come mostrato nella risposta di n.m.