tipo esistenziale in funzione di ordine superiore

Question

Ho una funzione il cui compito è quello di calcolare un valore ottimale di tipo a WRT qualche funzione valore di tipo a -> v

type OptiF a v = (a -> v) -> a 

poi ho un contenitore che vuole conservare tale una funzione insieme ad un'altra funzione che utilizza i valori valori:

data Container a = forall v. (Ord v) => Cons (OptiF a v) (a -> Int) 

L'idea è che chi implementa una funzione di tipo OptiF a v non deve essere disturbato con i dettagli della v tranne che' s un'istanza di Ord.

Quindi ho scritto una funzione che accetta una funzione di valore e un contenitore. Utilizzando il OptiF a v dovrebbe calcolare il valore WRT ottimale val e collegarlo result la funzione del contenitore:

optimize :: (forall v. (Ord v) => a -> v) -> Container a -> Int 
optimize val (Cons opti result) = result (opti val) 

Fin qui tutto bene, ma non posso chiamare optimize, perché

callOptimize :: Int 
callOptimize = optimize val cont 
    where val = (*3) 
     opti val' = if val' 1 > val' 0 then 100 else -100 
     cont = Cons opti (*2) 

non lo fa compilare:

Could not deduce (v ~ Int) 
from the context (Ord v) 
    bound by a type expected by the context: Ord v => Int -> v 
    at bla.hs:12:16-32 
    `v' is a rigid type variable bound by 
     a type expected by the context: Ord v => Int -> v at bla.hs:12:16 
Expected type: Int 
    Actual type: Int 
Expected type: Int -> v 
    Actual type: Int -> Int 
In the first argument of `optimize', namely `val' 
In the expression: optimize val cont 

dove la linea 12: 16-32 è optimize val cont.

In questo caso, ho frainteso i tipi esistenziali? Il forall v nella dichiarazione di optimize significa che optimize si può aspettare da a -> v qualunque sia lo v desiderato? O significa che optimize non può aspettarsi nulla da a -> v tranne che Ord v?

Quello che voglio è che il OptiF a v non è stato risolto per qualsiasi v, perché voglio inserire alcuni a -> v in seguito. L'unico vincolo che vorrei imporre è Ord v. È anche possibile esprimere qualcosa del genere usando tipi esistenziali (o qualsiasi altra cosa)?

Sono riuscito a farlo con un ulteriore typeclass che fornisce una funzione optimize con una firma simile a OptiF a v, ma per me è molto più brutto che utilizzare le funzioni di ordine superiore.

Answer 1

Questo è qualcosa che è facile sbagliare.

Quello che avete nella firma di optimize è non un esistenziale, ma universale.

... dal esistenziali sono un po 'datato in ogni caso, cerchiamo di riscrivere i dati in forma GADT, il che rende il punto più chiaro come la sintassi è essenzialmente lo stesso per le funzioni polimorfiche:

data Container a where 
    (:/->) :: Ord v =>      -- come on, you can't call this `Cons`! 
    OptiF a v -> (a->Int) -> Container a 

osservare che la Ord vincolo (che implica che questo è il forall v...) si trova al di fuori della firma della funzione con parametrizzazione variabile, ovvero v è un parametro che è possibile dettare dall'esterno quando si desidera costruire un valoreContainer.In altre parole,

Per ogni v in Ordesiste costruttore (:/->) :: OptiF a v -> (a->Int) -> Container a

che è ciò che dà origine al nome "tipo esistenziale". Di nuovo, questo è analogo a una funzione polimorfica ordinaria.

D'altra parte, nella firma

optimize :: (forall v. (Ord v) => a -> v) -> Container a -> Int 

voi hanno un forall all'interno del termine firma stessa, il che significa che ciò che tipo concreto v può assumere sarà determinato dalla callee, optimize, internamente - tutto ciò che abbiamo il controllo dall'esterno è che è in Ord. Niente "esistenziale" a tale proposito, che è il motivo per cui questa firma non sarà effettivamente compilare con XExistentialQuantification o XGADTs da solo:

<interactive>:37:26: 
    Illegal symbol '.' in type 
    Perhaps you intended -XRankNTypes or similar flag 
    to enable explicit-forall syntax: forall <tvs>. <type> 

val = (*3), ovviamente, non soddisfa (forall v. (Ord v) => a -> v), in realtà richiede un'istanza Num cui non tutti i Ord s hanno . Infatti, optimize non dovrebbe avere bisogno del tipo rank2: dovrebbe funzionare per qualsiasi Ord tipo v che il chiamante potrebbe dargli.

optimize :: Ord v => (a -> v) -> Container a -> Int 

nel qual caso l'implementazione non funziona più, però: dal momento che (:/->) è davvero un costruttore esistenziale, deve contenere solo qualsiasiOptiF funzione, ad un certo tipo sconosciuto v1. Quindi chi chiama di ottimizzare ha la libertà di scegliere l'opti-funzione per un particolare tipo di questo tipo e la funzione da ottimizzare per qualsiasi altro tipo fisso - che non può funzionare!

La soluzione che si desidera è questa: Container non deve essere esistenziale, sia! L'opti-function dovrebbe funzionare per qualsiasi tipo che sia in Ord, non solo per un particolare tipo. Beh, come GADT questo sembra più o meno come la firma universalmente quantificata si aveva in origine per optimize:

data Container a where 
    (:/->) :: (forall v. Ord v => OptiF a v) -> (a->Int) -> Container a 

Con che ora, ottimizzare opere

optimize :: Ord v => (a -> v) -> Container a -> Int 
optimize val (opti :/-> result) = result (opti val) 

e può essere utilizzato, come si voleva

callOptimize :: Int 
callOptimize = optimize val cont 
    where val = (*3) 
     opti val' = if val' 1 > val' 0 then 100 else -100 
     cont = opti :/-> (*2)