Haskell: foldr vs foldr1

Question

Se ho questa funzione di inserimento:

insert x []  = [x] 
insert x (h:t) 
    | x <= h  = x:(h:t) 
    | otherwise = h:(insert x t) 

questo produce un elenco ordinato:

foldr insert [] [1,19,-2,7,43] 

ma questo:

foldr1 insert [1,19,-2,7,43] 

produce 'non può costruire il tipo infinito: a0 = [a0] '

Sono confuso sul motivo per cui la seconda chiamata non può funzionare.

Ho esaminato le definizioni per foldr e foldr1 e ho tracciato entrambe con semplici funzioni aritmetiche, ma non riesco ancora a trovare una spiegazione chiara del motivo per cui la seconda chiamata fallisce.

Answer 1

Perché foldr1 sta cercando di fare questo:

insert 43 -7 

che fallirà.

Answer 2

Il tipo di foldr1 è (a -> a -> a) -> [a] -> a, vale a dire gli argomenti e il risultato di questa funzione hanno lo stesso tipo. Tuttavia, insert ha tipo Ord a => a -> [a] -> [a]. Per foldr1 insert essere ben digitato, a e [a] devono essere dello stesso tipo.

Ma questo significherebbe che a == [a] == [[a]] == [[[a]]] == ..., ovvero a è un tipo di infinitamente molti elenchi.

Answer 3

Diamo un'occhiata ad alcune firme di tipo.

foldr :: (a -> b -> b) -> b -> [a] -> b 
foldr1 :: (a -> a -> a) ->  [a] -> a 

In entrambi i casi, il primo argomento è una funzione di due argomenti.

• per foldr1, questi due argomenti devono avere lo stesso tipo (e il risultato è questo tipo anche)
• per foldr, questi due argomenti possono avere tipi diversi (e il risultato è lo stesso tipo della seconda argomento)

Qual è il tipo del tuo insert?

Answer 4

Il problema è il seguente:

foldr farebbe in questo modo:

1. set di risultati insert 43 []
2. set di risultati insert 7 result
3. e così via

Questo chiaramente lavori.

Mentre foldr1 avrebbe cercato di effettuare le seguenti operazioni:

1. set di risultati insert 7 43
2. set di risultati insert -2 result
3. ecc

che è sicuramente sbagliato. È possibile vedere, foldr1 richiede che gli argomenti dell'operazione siano dello stesso tipo, che non è il caso di insert.

Answer 5

Mi piacciono le risposte basate sul tipo fornite qui, ma voglio anche dare una spiegazione operativa del perché non vogliamo che questo sia tipografico. Prendiamo la fonte di foldr1 per cominciare:

foldr1   :: (a -> a -> a) -> [a] -> a 
foldr1 _ [x] = x 
foldr1 f (x:xs) = f x (foldr1 f xs) 

Ora, proviamo l'esecuzione del programma.

foldr1 insert [1,19,-2,7,43] 
= { list syntax } 
foldr1 insert (1:[19,-2,7,43]) 
= { definition of foldr1 } 
insert 1 (foldr1 insert [19,-2,7,43]) 
= { three copies of the above two steps } 
insert 1 (insert 19 (insert (-2) (insert 7 (foldr1 insert [43])))) 
= { definition of foldr1 } 
insert 1 (insert 19 (insert (-2) (insert 7 43))) 

... whoops! Che insert 7 43 non funzionerà mai. =)