Haskell: le variabili di tipo nelle clausole "where" nello stesso spazio dei nomi con i loro genitori?

Question

Nel seguente frammento di codice (ho sottratto tutte le altre parti banali)

data T s = T (s -> s) 

foo :: T s -> s -> s 
foo (T f) x = bar x where 
    bar :: s -> s 
    bar a = f a 

mi sono seguente errore

Couldn't match expected type `s1' with actual type `s' 
    `s1' is a rigid type variable bound by 
     the type signature for bar :: s1 -> s1 at /tmp/test.hs:5:12 
    `s' is a rigid type variable bound by 
     the type signature for foo :: T s -> s -> s at /tmp/test.hs:3:8 
In the return type of a call of `f' 
In the expression: f a 
In an equation for `bar': bar a = f a 

la mia ipotesi è che le variabili di tipo a firma bar s' non condividono la namespace con foo, quindi il compilatore non può dedurre che i due s significhi effettivamente lo stesso tipo.

Quindi ho trovato questa pagina Scoped type variables, che suggerisce che posso utilizzare {-# LANGUAGE ScopedTypeVariables #-}, che non ha aiutato. Ho avuto lo stesso errore.

Answer 1

Le variabili di tipo nelle clausole "where" si trovano nello stesso spazio dei nomi con i relativi genitori?

No *. Questo diventa un po 'più semplice se si pensa a foo :: s -> s in termini di foo :: forall s. s -> s. Dopo tutto, una variabile di tipo indica che la funzione funziona con qualsiasi tipo s. Aggiungiamo quantificazioni espliciti al codice:

{-# LANGUAGE ExplicitForAll #-} 

data T s = T (s -> s) 

foo :: forall s. T s -> s -> s 
foo (T f) x = bar x where 
    bar :: forall s. s -> s 
    bar a = f a 

Come si può vedere, ci sono due forall s. lì. Ma quello in bar è sbagliato. Dopo tutto, non è possibile scegliere qualsiasis lì, ma quello già utilizzato in s. Questo può essere fatto abilitando ScopedTypeVariables:

{-# LANGUAGE ScopedTypeVariables #-} 

data T s = T (s -> s) 

--  vvvvvvvv explicit here 
foo :: forall s. T s -> s -> s 
foo (T f) x = bar x where 
    --  vvvvvv same as above here 
    bar :: s -> s 
    bar a = f a 

Tuttavia, ci sono alcuni trucchi per sbarazzarsi di ScopedTypeVariables. Ad esempio il seguente in questo caso:

data T s = T (s -> s) 

foo :: T s -> s -> s 
foo (T f) x = (bar `asTypeOf` idType x) x where 

    bar a = f a 

    idType :: a -> a -> a 
    idType a _ = a 

-- For completion, definition and type of 'asTypeOf' 
-- asTypeOf :: a -> a -> a 
-- asTypeOf x _ = x 

per qualsiasi x :: s termine idType x ha tipo s -> s e asTypeOf impone sia per avere lo stesso tipo.

A seconda del codice effettivo, qualcosa del genere potrebbe essere più o meno fattibile.

---

^{* Bene, in questo caso, dal momento che è possibile utilizzare ScopedTypeVariables, vedere parte successiva della risposta.}

Answer 2

ScopedTypeVariables sono infatti la soluzione, ma c'è un requisito in più per usarli: Devi mettere espliciti forall s nelle firme di tipo dichiarare le variabili che si desidera campo di applicazione, in questo modo:

foo :: forall s. T s -> s -> s 

questo è così che il significato delle firme nel codice non dipende dal fatto che l'estensione sia abilitata o meno.