Haskell Riscrivi regole e composizione delle funzioni

Question

Perché haskell richiede più regole di riscrittura a seconda della tecnica di composizione della funzione e della lunghezza? c'è un modo per evitarlo?

Ad esempio, dato il seguente codice ...

{-# RULES 
"f/f" forall a. f (f a) = 4*a 
    #-} 
f a = 2 * a 

questo funziona per

test1 = f (f 1) 

però abbiamo bisogno di aggiungere una regola per

test2 = f . f $ 1 

e

test3 = f $ f 1 

lasciandoci con le seguenti regole

{-# RULES 
"f/f1" forall a. f (f a) = 4 * a 
"f/f2" forall a. f . f $ a = 4 * a 
"f/f3" forall a. f $ f $ a = 4 * a 
    #-} 

Tuttavia, quando abbiamo stringa di questi insieme o utilizzare altre forme di composizione delle regole non sparano.

test4 = f . f . f $ 1 
test5 = f $ f $ f $ 1 
test6 = f $ 1 

Perché è questo? Devo scrivere regole di riscrittura per ogni possibile implementazione?

Answer 1

La regola non si attiva in molti casi, poiché la funzione molto semplice f è inline prima della regola avesse la possibilità di sparare. Se si ritarda la messa in linea,

{-# INLINE [1] f #-} 

la regola

{-# RULES "f/f" forall a. f (f a) = 4*a #-} 

dovrebbe sparare per tutti questi casi (lavorato qui con 7.2.2 e 7.4.1).

Il motivo è che il rule matcher non è eccessivamente elaborato, corrisponde solo alle espressioni che hanno la forma sintattica della regola (non interamente vero, anche il corpo della regola subisce qualche normalizzazione). Le espressioni f $ f 3 o f . f $ 4 non corrispondono alla forma sintattica della regola. Affinché la regola corrisponda, alcune riscritture devono aver luogo, ($) e (.) devono essere incorporate prima che la regola corrisponda all'espressione. Ma se non impedisci l'inclinazione dello f nella prima fase del programma di semplificazione, esso viene sostituito dal suo corpo nella stessa esecuzione di ($) e (.) sono in linea, quindi nella prossima iterazione il dispositivo non vede più f, vede solo 2*(2*x), che non corrisponde alla regola.

Answer 2

avrei pensato che questo dovrebbe funzionare per impostazione predefinita, ma è possibile aggiungere altre due regole di riscrittura per rendere ./$ ridotta a lambda/applicazione, in modo che questo sarà sempre corrispondere:

{-# RULES 
"f/f" forall a. f (f a) = 4*a 

"app" forall f x. f $ x = f x 
"comp" forall f g. f . g = (\x -> f (g x)) 
    #-} 

f a = 3 * a -- make this 3*a so can see the difference 

Un test :

main = do 
    print (f . f $ 1) 
    print (f (f 1)) 
    print (f $ f 1) 
    print (f $ f $ 1) 
    print (f $ f $ f $ f $ 1) 
    print (f . f . f . f $ 1) 
    print (f $ f $ f $ 1) 
    print (f . f . f $ 1) 
    print (f $ 1) 

uscita:

4 
4 
4 
4 
16 
16 
12 
12 
3 

Questo sarà anche lavorare in alcuni (ma non tutti) più oscuri c ases, a causa di altre regole di riscrittura. Ad esempio, tutti questi funzionerà:

mapf x = map f $ map f $ [x] 
mapf' x = map (f.f) $ [x] 
mapf'' x = map (\x -> f (f x)) $ [x]