firme/tipi in programmazione funzionale (OCaml)

Question

Ho iniziato a imparare la programmazione funzionale (OCaml), ma non capisco un argomento importante su fp: firme (non sono sicuro che sia un nome proprio). Quando digito qualcosa e compilare con OCaml, ottengo ad esempio:

# let inc x = x + 1 ;; 
val inc : int -> int = <fun> 

Questo è banale, ma io non lo so, perché questo:

let something f g a b = f a (g a b) 

dà un output:

val something : (’a -> ’b -> ’c) -> (’a -> ’d -> ’b) -> ’a -> ’d -> ’c = <fun> 

Suppongo che questo argomento sia assolutamente di base per molti di voi, ma chiedo aiuto qui, perché non ho trovato nulla di su Internet sulle firme in OCaml (ci sono alcuni articoli sulle firme in Haskell, ma non le spiegazioni).

Se questo argomento in qualche modo sopravviverà, vi posto qui diverse funzioni, che le firme mi ha fatto confuso:

# let nie f a b = f b a ;; (* flip *) 
val nie : (’a -> ’b -> ’c) -> ’b -> ’a -> ’c = <fun> 

# let i f g a b = f (g a b) b ;; 
val i : (’a -> ’b -> ’c) -> (’d -> ’b -> ’a) -> ’d -> ’b -> ’c = <fun> 


# let s x y z = x z (y z) ;; 
val s : (’a -> ’b -> ’c) -> (’a -> ’b) -> ’a -> ’c = <fun> 

# let callCC f k = f (fun c d -> k c) k ;; 
val callCC : ((’a -> ’b -> ’c) -> (’a -> ’c) -> ’d) -> (’a -> ’c) -> ’d = <fun> 

Grazie per l'aiuto e la spiegazione.

Answer 1

ci sono un paio di concetti è necessario capire a dare un senso a questa firma tipo e non so quali già fate, quindi ho fatto del mio meglio per spiegare ogni concetto importante:

currying

Come sapete, se si ha il tipo foo -> bar, questo descrive una funzione prendendo un argomento di tipo foo e restituendo un risultato di tipo bar. Poiché -> è associativo corretto, il tipo foo -> bar -> baz corrisponde a foo -> (bar -> baz) e descrive quindi una funzione che accetta un argomento di tipo foo e restituisce un valore di tipo bar -> baz, che significa che il valore di ritorno è una funzione che assume un valore di tipo bar e restituisce un valore di tipo baz.

Tale funzione può essere chiamata come my_function my_foo my_bar, che a causa dell'applicazione funzione viene lasciata associativa, è la stessa (my_function my_foo) my_bar, cioè si applica my_function all'argomento my_foo e poi applica la funzione che viene restituito come risultato all'argomento my_bar.

Perché può essere chiamato in questo modo, una funzione di tipo foo -> bar -> baz viene spesso chiamata "una funzione che accetta due argomenti" e lo farò nel resto di questa risposta.

variabili di tipo

Se si definisce una funzione come let f x = x, avrà il tipo 'a -> 'a. Ma 'a non è in realtà un tipo definito in nessuna parte della libreria standard OCaml, quindi che cos'è?

Qualsiasi tipo che inizia con un ' è una variabile di tipo . Una variabile di tipo può rappresentare qualsiasi tipo possibile. Quindi nell'esempio sopra f può essere chiamato con uno int o uno string o uno list o qualcosa del genere - non importa.

Inoltre, se la stessa variabile di tipo appare in una segnatura di tipo più di una volta, sarà valida per lo stesso tipo. Quindi nell'esempio sopra ciò significa che il tipo restituito di f è uguale al tipo di argomento. Quindi, se f viene chiamato con uno int, restituisce uno int. Se viene chiamato con un string, restituisce un string e così via.

Quindi una funzione di tipo 'a -> 'b -> 'a potrebbe richiedere due argomenti di qualsiasi tipo (che potrebbero non essere dello stesso tipo per il primo e il secondo argomento) e restituisce un valore dello stesso tipo del primo argomento, mentre una funzione di tipo 'a -> 'a -> 'a prenderà due argomenti dello stesso tipo.

Una nota circa l'inferenza del tipo: a meno che non si attribuisca esplicitamente a una funzione una firma del tipo, OCaml dedurrà sempre il tipo più generale possibile. Quindi, a meno che una funzione non usi operazioni che funzionano solo con un determinato tipo (ad esempio +), il tipo dedotto conterrà le variabili di tipo.

Ora per spiegare il tipo di ...

val something : ('a -> 'b -> 'c) -> ('a -> 'd -> 'b) -> 'a -> 'd -> 'c = <fun> 

Questa firma tipo vi dice che something è una funzione di prendere quattro argomenti.

Il tipo del primo argomento è 'a -> 'b -> 'c. Cioè una funzione che prende due argomenti di tipi arbitrari e possibilmente diversi e restituisce un valore di un tipo arbitrario.

Il tipo del secondo argomento è 'a -> 'd -> 'b. Questa è di nuovo una funzione con due argomenti. La cosa importante da notare qui è che il primo argomento della funzione deve avere lo stesso tipo del primo argomento della prima funzione e il valore di ritorno della funzione deve avere lo stesso tipo del secondo argomento della prima funzione.

Il tipo del terzo argomento è 'a, che è anche il tipo dei primi argomenti di entrambe le funzioni.

Infine, il tipo del quarto argomento è 'd, che è il tipo del secondo argomento della seconda funzione.

Il valore restituito sarà di tipo 'c, ovvero il tipo di ritorno della prima funzione.

Answer 2

Se sei veramente interessato all'argomento (e hai accesso a una biblioteca universitaria), leggi l'eccellente "Introduzione alla programmazione funzionale" di Wadler (anche se un po 'datata). Spiega le firme di tipo e l'inferenza del tipo in un modo molto piacevole e leggibile.

Due ulteriori suggerimenti: si noti che la freccia -> è associativa a destra, quindi è possibile raggruppare elementi di destra che a volte aiutano a comprendere le cose, ad esempio a -> b -> c corrisponde a a -> (b -> c). Questo è collegato al secondo suggerimento: funzioni di ordine superiore. Si possono fare cose come

let add x y = x + y 
let inc = add 1 

così di FP, pensando a 'add' come una funzione che deve prendere due parametri numerici e restituisce un valore numerico è generalmente non la cosa giusta da fare: E ' può anche essere una funzione che accetta un argomento numerico e restituisce una funzione con tipo num -> num.

Capire questo ti aiuterà a capire le firme dei tipi, ma puoi farlo senza. Qui, semplice e veloce:

# let s x y z = x z (y z) ;; 
val s : (’a -> ’b -> ’c) -> (’a -> ’b) -> ’a -> ’c = <fun> 

Guarda il lato destro. viene fornito un argomento, quindi è di tipo a -> b dove a è il tipo di z. x ha due argomenti, il primo dei quali è z, quindi il tipo del primo argomento deve essere a. Il tipo di (y z), il secondo argomento, è b e quindi il tipo di x è (a -> b -> c). Ciò consente di dedurre immediatamente il tipo di s.