Dubbio tipizzazione ML

[mosco-votailprof]

ciao a tutti...avrei bisogno che qualcuno mi spieghi come tipizzare correttamente queste tre funzioni:

(fun x y -> x (x y));;

(fun x y -> x (y x));;

let f x y z t = (z x) (t y);;

la prima provando mi viene ('a->'a)->'b->'a ma invece il risultato sarebbe (’a -> ’a) -> ’a -> ’a
non riesco a capire perchè, in questo caso x e y sono due tipi generici ma uguali fra loro

la seconda non riesco proprio a farla

la terza mi viene 'a->'b->('a->'c->'d)->('b->'d)->'d ma il risultato sarebbe 'a -> 'b -> ('a -> 'c -> 'd) -> ('b -> 'c) -> 'd

Grazie per le risposte

[hamming_burst]

Ciao,

"oheila":
(fun x y -> x (x y));;

la prima provando mi viene ('a->'a)->'b->'a ma invece il risultato sarebbe (’a -> ’a) -> ’a -> ’a
non riesco a capire perchè, in questo caso x e y sono due tipi generici ma uguali fra loro

bhe certo perchè:
(x y)
x: a -> b
da questo
y: a

perciò (x y) resituisce un b

nel passo dopo
x (x y))
x: a -> b

si aspetta un a input ma (x y) produce un b
perciò per essere tipabile (x y) non può che produrre un a
x: a -> a

da questo fun x y -> x (x y):

(a -> a) -> a -> a

(fun x y -> x (y x));;
la seconda non riesco proprio a farla

ancora da interno ad esterno e specializzi:

(y x)
y: a -> b
x: a

x (y x)
da qui capisci che x è una funzione e y è una funzione che prende una funzione

y: (a->b) -> a
x (a -> b)

x (y x)
(y x) produce un c ma si capisce che produrra un a perchè x: (a -> b) lo prende in input

(a -> b) -> ((a -> b)->a) -> b

la terza mi viene 'a->'b->('a->'c->'d)->('b->'d)->'d ma il risultato sarebbe 'a -> 'b -> ('a -> 'c -> 'd) -> ('b -> 'c) -> 'd

Grazie per le risposte

[/quote]
la terza se qualcun'altro che passa ed ha voglia di spiegarla, oppure prova te dopo la spiegazione fatta per le altre due.

[apatriarca]

Vediamo allora la terza..

let f x y z t = (z x) (t y);;

Per prima cosa x e y possono avere un tipo qualsiasi perché vengono semplicemente passati come argomenti a due funzioni. Per cui possiamo iniziare a dire che x ha tipo a' e y ha tipo b'. t sarà quindi a questo punto una funzione con tipo b' -> c' e siccome (t y) viene semplicemente passato come argomento alla funzione (z x) il tipo c' è generico. A questo punto (z x) è una funzione di tipo c' -> d' e z ha quindi necessariamente tipo a' -> (c' -> d') (o semplicemente a' -> c' -> d'). f ha infine quindi tipo

a' -> b' -> (a' -> c' -> d') ->(b' -> c') -> d'

Spero che i passaggi siano chiari.

[mosco-votailprof]

grazie mille a entrambi, soprattutto per la tempestività delle risposte oltre che alla chiarezza
finalmente ho capito