Cosa sono skolems?

Question

Eeek! GHCi ha trovato Skolems nel mio codice!

... 
Couldn't match type `k0' with `b' 
    because type variable `b' would escape its scope 
This (rigid, skolem) type variable is bound by 
    the type signature for 
    groupBy :: Ord b => (a -> b) -> Set a -> Set (b, [a]) 
The following variables have types that mention k0 
... 

Cosa sono? Cosa vogliono con il mio programma? E perché stanno cercando di scappare (i piccoli ingrati ingrati)?

Answer 1

Per iniziare, una variabile di tipo "rigida" in un contesto indica una variabile di tipo associata a un quantificatore all'esterno di tale contesto, che pertanto non può essere unificata con altre variabili di tipo.

Questo funziona molto come le variabili vincolate da un lambda: dato un lambda (\x -> ...), dal "fuori" puoi applicarlo a qualsiasi valore tu voglia, naturalmente; ma all'interno, non puoi semplicemente decidere che il valore di x dovrebbe essere un valore particolare. Scegliere un valore per x all'interno della lambda dovrebbe sembrare piuttosto sciocco, ma questo è ciò che gli errori "non possono corrispondere a blah blah, tipo rigido variabile, blah blah" significa.

Si noti che, anche senza utilizzare i quantificatori espliciti forall, qualsiasi firma di tipo di livello superiore ha un valore implicito forall per ogni variabile di tipo menzionata.

Ovviamente, questo non è l'errore che si sta ottenendo. Ciò che una "variabile di tipo escape" significa è ancora più sciocco - è come avere un lambda (\x -> ...) e provare a utilizzare valori specifici di xall'esterno di lambda, indipendentemente dall'applicarlo a un argomento. No, non applicando il lambda a qualcosa e usando il valore del risultato - intendo in realtà usando la variabile stessa al di fuori dell'ambito in cui è definita.

Il motivo per cui questo può accadere con i tipi (senza sembrare ovviamente assurdo come l'esempio con un lambda) è perché ci sono due concetti di "variabili di tipo" che fluttuano: durante l'unificazione, si hanno "variabili" che rappresentano tipi indeterminati, che vengono poi identificati con altre di tali variabili tramite l'inferenza del tipo. D'altra parte, si hanno le variabili di tipo quantificato sopra descritte che sono specificatamente identificate come diverse dai possibili tipi.

Considerare il tipo di espressione lambda (\x -> x). Partendo da un tipo completamente indeterminato a, vediamo che accetta un argomento e lo stringiamo a a -> b, quindi vediamo che deve restituire qualcosa dello stesso tipo del suo argomento, quindi lo restringiamo ulteriormente a a -> a. Ma ora funziona per qualsiasi tipo di a che potresti volere, quindi gli diamo un quantificatore (forall a. a -> a).

Quindi, una variabile di tipo escape si verifica quando si ha un tipo associato da un quantificatore che i dati di GHC devono essere unificati con un tipo indeterminato all'esterno dello l'ambito di tale quantificatore.

---

Quindi a quanto pare ho dimenticato di spiegare in realtà il termine "variabile tipo skolem" qui, heh. Come accennato nei commenti, nel nostro caso è essenzialmente sinonimo di "variabile di tipo rigido", quindi quanto sopra spiega ancora l'idea.

Non sono del tutto sicuro da dove ha avuto origine il termine da, ma direi che coinvolge Skolem normal form e rappresentando esistenziale quantificazione in termini di universale, come si fa in GHC. Una variabile di tipo skolem (o rigida) è quella che, all'interno di un certo ambito, ha un tipo sconosciuto ma specifico per qualche ragione - essendo parte di un tipo polimorfico, proveniente da un tipo di dati esistenziali, & c.

Answer 2

A quanto ho capito, una "variabile Skolem" è una variabile che non corrisponde ad alcuna altra variabile, incluso se stessa.

Questo sembra comparire in Haskell quando si utilizzano funzionalità come trince esplicite, GADT e altre estensioni di sistema di tipo.

Ad esempio, considerare il tipo seguente:

data AnyWidget = forall x. Widget x => AnyWidget x 

cosa dice questo è che si può prendere qualsiasi tipo che implementa la classe Widget, e avvolgerlo in un tipo AnyWidget. Ora, supponiamo che si tenta di unwrap questo:

unwrap (AnyWidget w) = w 

Uhm, no, non è possibile farlo. Perché, in fase di compilazione, non abbiamo idea di cosa sia il tipo w, quindi non c'è modo di scrivere una firma di tipo corretta per questo. Qui il tipo di w ha "escapato" da AnyWidget, che non è consentito.

Come ho capito, GHC internamente fornisce w un tipo che è una variabile Skolem, per rappresentare il fatto che non deve sfuggire. (Questo non è l'unico scenario di questo tipo: ci sono un paio di altri posti in cui un determinato valore non può uscire a causa di problemi di digitazione.)

Answer 3

Il messaggio di errore si apre quando una variabile di tipo cerca di uscire dal suo ambito.

Mi ci è voluto un po 'per capire questo, quindi scriverò un esempio.

{-# LANGUAGE ExistentialQuantification #-} 
data I a = I a deriving (Show) 
data SomeI = forall a. MkSomeI (I a) 

Poi se cerchiamo di scrivere una funzione

unI (MkSomeI i) = i 

GHC rifiuta di tipo-inferire/tipo controllare questa funzione.

---

Perché? Proviamo a dedurre il tipo noi stessi:

• unI è una definizione lambda, quindi è tipo è x -> y per alcuni tipi x e y.
• MkSomeI ha un tipo forall a. I a -> SomeI
  • MkSomeI i ha un tipo SomeI
  • i sulle LHS ha un tipo I z per qualche tipo z. A causa del quantificatore forall, abbiamo dovuto introdurre una nuova variabile di tipo (fresca). Nota che non è universale, poiché è associato all'interno dell'espressione (SomeI i).
  • quindi possiamo unificare la variabile di tipo x con SomeI, questo è ok. Quindi lo unI dovrebbe avere il tipo SomeI -> y.
• i sul RHS hanno quindi tipo I z troppo.
• A questo punto l'unificatore tenta di unificare e I z, ma nota che z viene introdotto nel contesto inferiore. Quindi fallisce.

Altrimenti il ​​tipo per unI avrebbe dovuto tipo forall z. SomeI -> I z, ma quello corretto è exists z. SomeI -> I z. Eppure quel GHC non può rappresentare direttamente.

---

Allo stesso modo, siamo in grado di capire perché

data AnyEq = forall a. Eq a => AE a 
-- reflexive :: AnyEq -> Bool 
reflexive (AE x) = x == x 

opere.

La variabile (esistenziale) all'interno di AE x non sfugge all'ambito esterno, quindi tutto è ok.

---

Inoltre ho incontrato un "feature" in GHC 7.8.4 e 7.10.1 dove RankNTypes su se stesso è ok, ma aggiungendo GADTs genera l'errore

{-# LANGUAGE RankNTypes #-} 
{-# LANGUAGE GADTs #-} 

example :: String -> I a -> String 
example str x = withContext x s 
    where 
    s i = "Foo" ++ str 

withContext :: I a -> (forall b. I b -> c) -> c 
withContext x f = f x 

quindi potrebbe essere niente di sbagliato con il codice . Potrebbe essere GHC, che non è in grado di capire tutto in modo coerente.

MODIFICA: la soluzione è fornire un tipo a s :: forall a. I a -> String.

GADTs accendere MonoLocalBinds, che rende tipo derivato di s avere variabile Skolem, modo che il tipo non è forall a. I a -> String, ma t -> String, erano t ottiene vincolato nel contesto sbagliato. Vedi: https://ghc.haskell.org/trac/ghc/ticket/10644