Perché la funzione (+) corrisponde al tipo (a -> b -> b)? Funzione

Question

duplice:

fold :: b -> (a -> b -> b) -> [a] -> b 
fold z f []  = z 
fold z f (x:xs) = f x (fold z f xs) 

tratto da http://www.seas.upenn.edu/~cis194/spring13/lectures/04-higher-order.html

Prelude> :t (+) 
(+) :: Num a => a -> a -> a 

*Main> fold (0) (+) [1,2,3] 
6 

Ciò che tipo (a -> b -> b) match con tipo a -> a -> a per (+) funzione?

Poiché la definizione di piega accetta il tipo di funzione (a -> b -> b), ciò significa che i primi 2 parametri (a -> b) devono essere di tipi diversi?

Answer 1

No, tutto ciò che significa è che a e bpuò essere diverso, ma non è obbligatorio per essere diverso. Nel tuo caso, è lo stesso.

Un esempio molto più semplice per trasmettere il punto:

data SomeType a b = Test a b deriving (Show) 

Ora in ghci:

Answer 2

Stai pensando in direzione inversa. Non è necessario controllare se + è identico o fiammiferi a -> b -> b, si desidera che il tipo di + di essere una specializzazione di a -> b -> b e per verificare questo è necessario unificare i tipi.

Unificazione significa che si vuole vedere se il tipo di + e il tipo a -> b -> b possono essere resi uguali da rinominando le variabili di tipo.

Quindi + ha tipo Num x => x -> x -> x. Ignoriamo il vincolo della classe per ora, e vediamo se possiamo abbinare i tipi funzionali. I tipi diventano x -> x -> x e a -> b -> b. In effetti è meglio guardarli come realmente, senza usare l'associatività: x -> (x -> x) e a -> (b -> b).

Il -> è un costruttore di tipo . Cioè è una funzione che associa un certo numero di tipi a un tipo diverso. In questo caso il costruttore -> associa due tipi t_1 e t_2 al tipo funzionale (->) t_1 t_2 (che di solito è indicato da t_1 -> t_2).

Così il tipo x -> (x -> x) è in realtà (->) x ((->) x x) che è il tipo di costruzione -> applicato a x e al tipo di costruttore di -> applicato a x e x. L'altro tipo è (->) a ((->) b b).

Durante l'unificazione si considera il costruttore di tipo più esterno per i due tipi (-> per entrambi in questo caso). Se questo non corrisponde, non puoi unificare. Altrimenti devi unificare gli argomenti del costruttore.

Quindi dobbiamo unificare x con a. Sono entrambe variabili di tipo, quindi possiamo rinominare uno di loro. Diciamo che rinominiamo a con x. Quindi ora applichiamo la ridenominazione ai tipi, ottenendo: (->) x ((->) x x) e (->) x ((->) b b) e vedete che x e x ora corrispondono.

Consideriamo il secondo argomento. Non è una variabile di tipo quindi dobbiamo corrispondere al costruttore del tipo, e questo è nuovamente -> per entrambi. Quindi procediamo ricorsivamente sugli argomenti.

Vogliamo corrispondere a x e b. Sono entrambe variabili di tipo, quindi possiamo rinominarne una. Supponiamo di rinominare x in b. Applichiamo questa sostituzione ai tipi, ottenendo: (->) b ((->) b b) e (->) b ((->) b b). Ora il tutto corrisponde. Quindi i due tipi unificano.

Per quanto riguarda il vincolo di classe, quando abbiamo rinominiamo x con b abbiamo applicato la sostituzione al vincolo troppo così Num x divenne Num b ei due tipi finali sono entrambi Num b => b -> b -> b.

Spero che questo ti abbia aiutato a capire meglio come funzionano i tipi e come vengono controllati i tipi.

---

Nota a margine: questo è ciò che haskell esegue quando si esegue l'inferenza di tipo. Assegna prima a una funzione sconosciuta una nuova variabile di tipo t. Quindi utilizza l'unificazione per ottenere il tipo dell'espressione che lo definisce e controlla quale tipo è stato associato a t e questo è il tipo di funzione.