In che modo ciò costituisce un errore di tipo rigido Haskell?

Question

Questo funziona:

data Wrapped a = Wrapped a 

alpha :: IO s -> IO() 
alpha x = do 
    rv <- wrapit x 
    return() 
    where  
     wrapit :: IO s -> IO (Wrapped s) 
     wrapit x' = do 
      a <- x' 
      return (Wrapped a) 

Questo non lo fa:

data Wrapped a = Wrapped a 

alpha :: IO s -> IO() 
alpha x = do 
    rv <- wrapit 
    return() 
    where  
     wrapit :: IO (Wrapped s) 
     wrapit = do 
      a <- x 
      return (Wrapped a) 

Perché?

Answer 1

Ciò è dovuto al modo in cui le variabili di tipo vengono esaminate e quantificate in Haskell standard. È possibile effettuare la seconda opera di versione in questo modo:

{-# LANGUAGE RankNTypes, ScopedTypeVariables #-} 

module RigidProblem where 

data Wrapped a = Wrapped a 

alpha :: forall s. IO s -> IO()             
alpha x = do 
    rv <- wrapit 
    return() 
    where  
     wrapit :: IO (Wrapped s) 
     wrapit = do 
      a <- x 
      return (Wrapped a) 

ci sono due cambiamenti: le RankNTypes e estensioni del linguaggio ScopedTypeVariables sono abilitati e l'esplicita forall s viene aggiunto nella firma tipo di alpha. La prima delle due estensioni è ciò che ci consente di introdurre l'esplicito forall s inserendo lo s all'interno del corpo di alpha, mentre il secondo fa in modo che la firma su wrapit non venga presa dal motore di inferenza del tipo per contenere un implicito forall s - invece, lo s in quella firma viene preso come nome di una variabile di tipo che dovrebbe essere inclusa nell'ambito e identificata con esso.

La situazione di default corrente in Haskell, se ho capito bene, è che tutte le variabili di tipo rigido (cioè le variabili di tipo che si verificano nelle firme di tipo esplicitamente previsti dal programmatore) sono implicitamente quantificati e non scope lessicale, in modo che ci sia non c'è modo di riferirsi a una variabile di tipo rigida da un ambito esterno in una firma esplicita fornita in un ambito interno ... (Oh fastidio, sono sicuro che qualcuno potrebbe esprimerlo meglio di questo.) Comunque, dal punto di controllo del tipo di vista, la firma s nella firma alpha e quella nella firma wrapit sono completamente indipendenti e non possono essere unificate, quindi l'errore.

Vedere dai documenti GHC e this page da Haskell Prime wiki per ulteriori informazioni.

Aggiornamento: Ho appena realizzato che non ho mai spiegato perché la prima versione funziona. Per completezza: si noti che con la prima versione, è possibile utilizzare t al posto di s nella firma wrapit e nulla cambierebbe. Puoi anche prendere wrapit dal blocco where e renderlo una funzione di livello superiore separata. Il punto chiave è che si tratta di una funzione polimorfica, in modo che il tipo di wrapit x sia determinato dal tipo di x. Nessuna relazione tra la variabile di tipo utilizzata nella prima versione della firma di wrapit in quella utilizzata nella firma di alpha potrebbe essere utile in questo caso. Con la seconda versione questo è ovviamente diverso ed è necessario ricorrere ai suddetti trucchetti per rendere wrapit's s essere la stessa cosa di alpha di s.

Answer 2

risposta di

Michał Marczyk sopra è corretto, ma vale la pena notare che la seconda versione funziona se si rimuove la firma tipo della funzione wrapit:

data Wrapped a = Wrapped a 

alpha :: IO s -> IO() 
alpha x = do 
    rv <- wrapit 
    return() 
    where 
     -- No type signature here! 
     wrapit = do 
      a <- x 
      return (Wrapped a) 

Cioè, il problema non è con il codice stesso; è che Haskell 98 non ti permette di scrivere una firma di tipo per la funzione wrapit, perché include una variabile di tipo legata al suo contesto (la funzione esterna alpha) e H98 non ha un modo per esprimerlo.Come ha detto Michał, abilitare ScopedTypeVariables consente di farlo.