2013-05-06 12 views
16

stavo giocando intorno con lenti van Laarhoven e sono imbattuto in un problema in cui il tipo ortografico rifiuta la forma eta-ridotta di una funzione ben tipato:Come può l'eta-riduzione di una funzione ben tipizzata causare un errore di tipo?

{-# LANGUAGE RankNTypes #-} 

import Control.Applicative 

type Lens c a = forall f . Functor f => (a -> f a) -> (c -> f c) 

getWith :: (a -> b) -> ((a -> Const b a) -> (c -> Const b c)) -> (c -> b) 
getWith f l = getConst . l (Const . f) 

get :: Lens c a -> c -> a 
get lens = getWith id lens 

Le suddette tipo di controlli, ma se io eta- ridurre get a

get :: Lens c a -> c -> a 
get = getWith id 

Poi GHC (7.4.2) si lamenta che

Couldn't match expected type `Lens c a' 
      with actual type `(a0 -> Const b0 a0) -> c0 -> Const b0 c0' 
Expected type: Lens c a -> c -> a 
    Actual type: ((a0 -> Const b0 a0) -> c0 -> Const b0 c0) 
       -> c0 -> b0 
In the return type of a call of `getWith' 
In the expression: getWith id 

posso capire che se la funzione d Se non si dispone di una firma di tipo esplicita, l'eta-riduzione in combinazione con la limitazione del monomorfismo potrebbe confondere l'inferenza di tipo, specialmente quando si tratta di tipi di rango più alti, ma in questo caso non sono sicuro di cosa sta succedendo.

Quali sono le cause per cui GHC rifiuta la forma ridotta in base all'Eta e si tratta di un bug/limitazione in GHC o di qualche problema fondamentale con tipi di rango più alti?

+0

Fa la differenza quando si scrive il tipo 'Lens' espanso? – Ingo

risposta

12

Direi che il motivo non è nella riduzione η, il problema è che con RankNTypes si perde principal types e si immette il tipo.

Il problema di inferenza di tipo con ordine superiore si colloca è quando inferire il tipo di λx.M di obbedire alla regola

 Γ, x:σ |- M:ρ 
---------------------- 
    Γ |- λx:σ.M : σ→ρ 

non sappiamo che tipo σ dovremmo scegliere per x. Nel caso del sistema di tipo Hindley-Milner, ci limitiamo a tipi di tipo quantificatore-libero per x e l'inferenza è possibile, ma non con tipi di classificazione arbitrari.

Quindi, anche con RankNTypes, quando il compilatore incontra un termine senza informazioni di tipo esplicito, ricorre a Hindley-Milner e ne deduce il tipo principale di grado 1. Tuttavia, nel tuo caso il tipo che ti serve per getWith id è rank-2 e quindi il compilatore non può dedurlo da solo.

Il tuo caso esplicito

get lens = getWith id lens 

corrisponde alla situazione in cui il tipo di x è già dato esplicitamente λ(x:σ).Mx.Il compilatore conosce il tipo di lens prima del controllo dei caratteri getWith id lens.

Nel caso ridotta

get = getWith id 

il compilatore deve dedurre il tipo di getWidth id su di essa la propria, quindi si attacca con Hindley-Milner e inferisce l'inadeguata rango-1 tipo.

5

In realtà è piuttosto semplice: GHC deduce i tipi per espressione, quindi inizia a unificarli su =. Funziona sempre bene quando ci sono solo i tipi rank 1, perché viene scelto quello più polimorfico (che è ben definito); quindi qualsiasi unificazione che sia possibile avrà successo.

Ma non sceglierà un rank-2 di tipo più generale anche se ciò sarebbe possibile, quindi getWith id viene considerato come ((a -> Const a a) -> c -> Const a c) -> (c -> a) anziché (forall f . Functor f => (a -> f a) -> c -> f c) -> (c -> a). Suppongo che se GHC facesse tali cose, l'inferenza di tipo rank-1 tradizionale non funzionerebbe più. Oppure non finirebbe mai, perché non esiste un tipo rank-n polimorfo ben definito.

che non spiega il motivo per cui non si può vedere dalla firma get s' che bisogno scegliere rango-2 qui, ma probabilmente c'è una buona ragione per questo pure.