Perché è necessaria questa espansione eta?

Question

Qualcuno può aiutarmi a capire questo/indicarmi dei materiali di lettura? Le seguenti opere di bene:

type F a b = Functor f => f a -> f b 
fComp :: F b c -> F a b -> F a c 
fComp f f' = f . f' 

Ma se scrivo fComp = (.) invece, il tipo di controllo si lamenta:

Couldn't match type ‘b0 -> f c’ 
       with ‘forall (f1 :: * -> *). Functor f1 => f1 b -> f1 c’ 

(Questo esempio specifico non è particolarmente utile, sto solo cercando di ridurre un esempio che si avvicinò mentre studiavo gli obiettivi.)

Answer 1

fComp ha un tipo più elevato e l'inferenza di tipo per i tipi di rango più alto è molto limitata. Potrebbe essere un po 'più facile da capire (ma molto più a lungo!) Se espandiamo il tipo sinonimo:

fComp :: forall f a b c. Functor f => 
       (forall f1. Functor f1 => f1 b -> f1 c) -> 
       (forall f2. Functor f2 => f2 a -> f2 b) -> 
       (f a -> f c) 

Più alto rango tipi di f e f' sono specificati esplicitamente in questa firma tipo. Ciò consente all'inferenza di tipo di iniziare già conoscendo i tipi di f e f' e quindi in grado di unificarli con il tipo di ..

Tuttavia, se si elimina f e f', il tipo che . deve prendere non è noto. Sfortunatamente, il sistema non può inferire tipi di rango superiore come questo, quindi si ottiene un errore di tipo.

In sostanza, il compilatore non può creare tipi di alto rango per riempire incognite durante inferenza e deve fare affidamento su annotazioni programmatore e abbiamo bisogno sia il nome (f e f') e il tipo di firma per ottenere quelle annotazioni.

Un esempio facile da capire sarebbe una funzione di alto rango id:

myId :: (forall a. a) -> (forall b. b) 

La definizione myId x = id x compila, ma myId = id dà il seguente errore:

/home/tikhon/Documents/so/eta-expansion-needed.hs:11:8: 
    Couldn't match type ‘b’ with ‘forall a. a’ 
     ‘b’ is a rigid type variable bound by 
      the type signature for myId :: (forall a. a) -> b 
      at /home/tikhon/Documents/so/eta-expansion-needed.hs:11:1 
    Expected type: (forall a. a) -> b 
     Actual type: b -> b 
    In the expression: id 
    In an equation for ‘myId’: myId = id 
Failed, modules loaded: none. 

(Tenete a mente che forall b. (forall a. a) -> b è uguale a (forall a. a) -> (forall b. b).)

Answer 2

Lasciami riscrivere la e xample usando una notazione simile a System-F, in cui passiamo anche i tipi. Sotto, \\ sta per tipo-astrazione (grande lambda), così come l'astrazione del dizionario. Inoltre, @ sta per tipo/applicazione dizionario.

Prima di farlo, richiamare il tipo di (.):

(.) :: forall a b c . (b -> a) -> (c -> b) -> (c -> a) 

Ecco il codice annotato (attenzione, non per i deboli di cuore):

fComp :: F b c -> F a b -> F a c 
fComp (f :: forall f1. Functor f1 => f1 b -> f1 c) 
     (f':: forall f2. Functor f2 => f2 a -> f2 b) 
    = \\ ff :: (* -> *) -> 
    \\ ffD :: Functor ff -> 
    ((.) @ (ff c) @ (ff b) @ (ff a)) -- instantiated composition 
    (f @ ff @ ffD)     -- first argument of (.) 
    (f' @ ff @ ffD)     -- second argument of (.) 

(Sopra ho fatto finta a, b , c sono costanti di tipo per evitare ulteriori lambda di tipo di livello.)

Le parti importanti:

• f e f' vengono utilizzati a tipi specifici. Vale a dire che vengono applicati agli argomenti a livello di codice prima di essere inviati a (.).
• (.) viene applicata a livello di tipo di tipi (ff c, ecc) che non sono i politipi di f e f'

Come potete vedere, il codice originale è ben lungi dall'essere banale. L'inferenza di tipo è in grado di aggiungere i lambda e le applicazioni necessari a livello di tipo. Dopo che questi sono stati aggiunti, non possiamo più semplicemente stipulare il contratto fComp.

Nella variante senza punti, l'inferenza di tipo avrebbe dovuto fare di più rispetto al caso. Mentre il primo argomento di fComp è di tipo F a b, il primo argomento di (.) deve essere del formato x -> y, che non unifica per F a b = forall g . .... In effetti, non c'è modo per risolvere con successo il tentativo di digitazione di seguito:

fComp :: F b c -> F a b -> F a c 
fComp 
    = \\ ff :: (* -> *) -> 
    \\ ffD :: Functor ff -> 
    ((.) @ ???a @ ???b @ ???c) 

Sopra non c'è ???a, ... che possono portare al tipo desiderato.

L'unica possibilità sarebbe quella di istanziare le forall variabili -quantified nascosti nelle F x y tipi, ma per farlo abbiamo bisogno di un punto di . Il compilatore potrebbe eta-espandere quel codice per te in modo che i punti appaiano e così possano essere istanziati, teoricamente parlando, ma in pratica no.

(Inoltre, l'espansione eta non è sempre valida in Haskell: ad esempio seq (undefined::()->()) 3 loop mentre seq (\x->(undefined::()->()) x) 3 restituisce 3).