[Caml] Programmazione funzionale: tipizzare in ocaml

[gidina17]

Ciao a tutti, sto cercando di capire come tipizzare, riporto alcuni esempi che non mi sono del tutto chiari:

let f x y z t = (z x) (t y);; che sarebbe ’a -> ’b -> (’a -> ’c -> ’d) -> (’b -> ’c)-> ’d

let f3 y x = x (y x);; che sarebbe ((’a -> ’b) -> ’a) -> (’a -> ’b) -> ’b

(fun x y z -> (x y z) z);; che sarebbe (’a ->’b ->’b ->’c) -> ’a ->’b ->’c

Questi esempi per quanto riguarda funzioni anonime.

let f g h x = List.filter h (List.map g x);; che sarebbe (’a -> ’b) -> (’b -> bool) -> ’a list -> ’b list

let f1 l c = List.map (fun x -> [x;c]) l;; che sarebbe ’a list -> ’a -> ’a list list

E questi degli esempi con map e filter.

Il problema è che non riesco a un intuire un metodo chiaro per tipizzarle! Il concetto di base si ma poi non riesco!

Qualcuno mi riesce a spiegare in modo chiaro come fare?

[apatriarca]

L'idea principale è quella di suddividere tutto in parti e analizzare ogni parte. Consideriamo il primo esempio esempio.

1. In questo caso hai una funzione che riceve 4 argomenti per cui puoi iniziare ad assegnare ad ognuna un tipo diverso:
'a -> 'b -> 'c -> 'd -> 'e
2. A questo punto osservi che x e y non hanno altri vincoli per quanto riguarda il loro tipo. Vengono infatti solamente passati come argomenti di funzione. Mentre z e t sono funzioni che hanno come primo argomento rispettivamente x e y.
'a -> 'b -> ('a -> ... ) -> ('b -> ...) -> 'e
3. A questo punto osservi che t restituisce un tipo qualsiasi (non ci sono ulteriori vincoli) mentre z restituisce una funzione che riceve come argomento il valore restituito da t. Il valore restituito da z è infine il risultato totale della funzione. Per cui hai a questo punto ottenuto
'a -> 'b -> ('a -> 'c -> 'd) -> ('b -> 'c) -> 'd

Spero sia chiaro. È una specie di puzzle in cui guardi come usi ogni valore e cerchi di comprendere quali restrizioni impone sul tipo. L'esperienza in questo caso aiuta parecchio. Quando inizi a scrivere funzioni e ad usare questi concetti, tutto diventerà molto più semplice.

[gidina17]

ma potrebbe essere anche la forma in cui viene scritto il tutto, vedere scritto la composizione di funzioni in una forma più matematica sicuro mi aiuterebbe di più!

[apatriarca]

Facendo qualche semplificazione, quelle funzioni possono essere tranquillamente riscritte in forma matematica come normali funzioni tra insiemi. Ad ogni tipo corrisponde un insieme di valori e puoi in generale avere insiemi arbitrari (a cui quindi associ un nome fittizio) e insiemi specifici come quello degli interi.

In particolare, la funzione \(f\) del primo esercizio potrebbe essere riscritta nel seguente modo come funzione matematica:
\[ f(x, y, z, t) = z\bigl(x, t(y)\bigr). \]
È qui chiaro che \(x\) e \(y\) possono appartenere ad insiemi qualsiasi, mentre \(z\) è una funzione con due variabili e \(t\) con una. A quel punto associ alle due variabili libere \(x\) e \(y\) tipi qualsiasi 'a e 'b. Prendi quindi in considerazione \(t\) (che a questo punto non dipende da alcun tipo non definito) e osservi che è una funzione la cui immagine può essere arbitraria. Dai quindi il nome 'c a questo insieme arbitrario. Infine osservi che \(z\) prende come argomenti \(x\) e l'immagine di \(y\) attraverso \(t\) per cui avrà tipo 'a -> 'c -> 'd per un insieme 'd arbitrario.

La funzione f3 ha ad esempio la forma
\[ f_3(y, x) = x\bigl(y(x)\bigr). \]
In questo caso hai quindi che \(x\) è una funzione che ha come argomento il valore di ritorno di \(y\) che a sua volta ha come argomento un valore dello stesso tipo di \(x\). Se quindi supponi che \(x\) abbia tipo 'a -> 'b, \(y\) dovrà avere tipo ('a -> 'b) -> 'a. Da qui dovrebbe essere facile ottenere quindi il tipo di f3.

I casi in cui usi List.filter o List.map sono simili. Devi semplicemente ricordarti il tipo di queste funzioni e usarle per capire il tipo totale delle espressioni.

È utile comunque provare a testare queste funzioni in Ocaml direttamente per vedere come si comportano. Per esempio, nel caso di f3 puoi supporre che \(y\) sia ad esempio una funzione che ignora il suo argomento e restituisce un valore costante. f3 restituirà allora il valore di \(x\) per questo valore costante. Se invece y restituisse un valore \(v\) per cui \(x(v)\) assume un massimo, f3 restituirà questo valore massimo. Scrivendo programmi si imparano ad usare con successo funzioni più complicate e diventa quindi poi anche più facile interpretarle.

[gidina17]

Non mi è molto chiaro come hai riscritto la prima e non riesco a capire molto la terza come la si riscrive!

[apatriarca]

In OCaml non esistono funzioni di più variabili, ogni funzione che prende in ingresso più valori è infatti una funzione che restituisce un'altra funzione. Ma è certamente possibile far finta che siano funzioni a più variabili quando si vuole comprendere meglio il loro comportamento. È quello che ho fatto analizzando la prima funzione..

Un'altra osservazione che si può fare è che f x y è sempre equivalente a (f x) y in OCaml. Quando quindi si analizza (z x) (t y) si può prima di tutto osservare che è equivalente a z x (t y). Quindi z è una "funzione in due variabili".

[apatriarca]

Per quanto invece riguarda la terza funzione hai che (x y z) z è equivalente per il discorso precedente a x y z z.. Per cui x è una funzione in quattro variabili in cui i tipi delle prime due variabili sono libere e le altre due hanno tipo qualsiasi ma uguale tra di loro. Per cui x ha tipo 'a -> 'b -> 'c -> 'c -> 'd. A questo punto il tipo dell'intera funzione dovrebbe essere immediato..

[gidina17]

Un pò più chiaro lo è, sto cercando di farne ancora per entrare meglio nell'ottica. Ne approfitto per chiedere un'altra cosa:
se io ho da capire il tipo di questo programma:

let rec f l = function
[] -> true
|x::xs ->
String.length l > x & f l xs;;

Mi è chiaro che l è una stringa perchè c'è String.length ma il matching viene fatto con una string list! Il mio problema è che, se il matching viene fatto con la struttura match .. with .. riesco a capire il tipo, vedendo function ecc mi risulta più difficile! Un modo pratico per capire?