Come si ottiene e si utilizza il tipo dipendente da una classe di caratteri con dipendenze funzionali?

Question

Come si ottiene e si utilizza il tipo dipendente da una classe di caratteri con dipendenze funzionali?

Per chiarire e dare un esempio del mio ultimo tentativo (minimizzati da codice vero e stavo scrivendo):

class Identifiable a b | a -> b where -- if you know a, you know b 
    idOf :: a -> b 

instance Identifiable Int Int where 
    idOf a = a 

f :: Identifiable Int b => Int -> [b] -- Does ghc infer b from the functional dependency used in Identifiable, and the instance? 
f a = [5 :: Int] 

Ma ghc non implica B, a quanto pare, come esso stampa questo errore:

Couldn't match expected type ‘b’ with actual type ‘Int’ 
    ‘b’ is a rigid type variable bound by 
     the type signature for f :: Identifiable Int b => Int -> [b] 
     at src/main.hs:57:6 
Relevant bindings include 
    f :: Int -> [b] (bound at src/main.hs:58:1) 
In the expression: 5 :: Int 
In the expression: [5 :: Int] 
In an equation for ‘f’: f a = [5 :: Int] 

per il contesto, ecco un esempio meno minimizzato:

data Graph a where 
    Graph :: (Identifiable a b) => GraphImpl b -> Graph a 

getImpl :: Identifiable a b => Graph a -> GraphImpl b 
getImpl (Graph impl) = impl 

La soluzione qui sarebbe da aggiungere b come tipo arg a Graph:

data Graph a b | a -> b where 
    Graph :: (Identifiable a b) => GraphImpl b -> Graph a 

Il contesto completo: Ho una Graph di soggetti che hanno ciascuno un id, ogni entità è assegnato al nodo 1. Puoi cercare un nodo per entità. Ho anche un Graph' che consiste di nodi (a cui è possibile assegnare un'entità) e per cercare un nodo è necessario fornire l'id del nodo, che è un Int. Graph utilizza Graph' internamente. Ho uno IdMap che associa gli ID delle entità agli ID dei nodi in Graph'. Questo è il mio Graph definizione:

data Graph a where 
    Graph :: (Identifiable a b) => { 
    _idMap :: IdMap b, 
    _nextVertexId :: Int, 
    _graph :: Graph' a 
} -> Graph a 

---

Risposta: Usare le famiglie tipo, vedere Daniel Wagner's answer. Per la storia completa, vedi Reid Barton's answer.

Answer 1

In effetti sembra un po 'strano che GHC si lamenta del minimo f che hai postato in cima. Ma sembra funzionare bene con le famiglie tipo:

{-# LANGUAGE TypeFamilies #-} 
class Identifiable a where 
    type IdOf a 
    idOf :: a -> IdOf a 

instance Identifiable Int where 
    type IdOf Int = Int 
    idOf a = a 

f :: a -> [IdOf Int] 
f _ = [5 :: Int] 

Forse si può adattare questa idea per il vostro esempio più esaustivo.

Answer 2

Nell'implementazione di GHC, le dipendenze funzionali possono limitare i valori delle variabili di tipo che altrimenti risulterebbero ambigue (nel senso show . read). Non possono essere usati per dimostrare che due tipi sono uguali, nel modo in cui i vincoli di uguaglianza possono. La mia comprensione è che le dipendenze funzionali precedono l'aggiunta di coercizioni al linguaggio intermedio Core di GHC, e queste coercizioni sono necessarie in generale per tradurre il tipo di programmi che si prevede di lavorare in programmi core ben tipizzati.

(Questa situazione è probabilmente la migliore, dal momento che GHC non applica realmente la condizione di dipendenza funzionale a livello globale e sarebbe facile interrompere la sicurezza del tipo se fossero accettati programmi come il primo. fare un lavoro migliore per far rispettare la coerenza globale delle istanze)

La versione breve di questo è che la logica del correttore di tipi attorno alle dipendenze funzionali non è così forte come ci si potrebbe aspettare, specialmente in combinazione con funzionalità di sistema di tipo più recente come GADT. Raccomando invece di usare famiglie di tipi in queste situazioni, come esemplificato dalla risposta di Daniel Wagner.

https://ghc.haskell.org/trac/ghc/ticket/345 è un vecchio ticket su un tema simile, quindi è possibile vedere che si tratta di un problema noto di lunga data con dipendenze funzionali e che l'utilizzo di famiglie di tipi è invece la soluzione consigliata ufficialmente.

Se si desidera mantenere lo stile in cui Identifiable ha due argomenti di tipo, è anche possibile impostare il programma in forma

type family IdOf a 
class (b ~ IdOf a) => Identifiable a b where 
    idOf :: a -> b 

type instance IdOf Int = Int 
instance Identifiable Int Int where 
    idOf a = a 

f :: Identifiable Int b => Int -> [b] 
f a = [5 :: Int]