type de fonctions d'ordre élevé

Question

si je spécifie le type (je pense) correct pour une fonction d'ordre élevé, le compilateur OCaml rejette l'utilisation seconde de cette fonction.

Le code

let foo():string = 
    let f: ('a -> string) -> 'a -> string = fun g v -> g v 
    in let h = string_of_int 
    in let i = string_of_float 
    in let x = f h 23 
    in let y = f i 23.0 
    in x^y 

conduit au message d'erreur suivant

File "test.ml", line 6, characters 14-15: 
Error: This expression has type float -> string 
     but an expression was expected of type int -> string

La première utilisation de f semble fixer le type de son premier paramètre à int -> string. Je pourrais comprendre ça. Mais ce que je ne comprends pas, c'est que l'omission de la restriction de type sur f résout le problème.

let foo():string = 
    let f g v = g v 
    in let h = string_of_int 
    in let i = string_of_float 
    in let x = f h 23 
    in let y = f i 23.0 
    in x^y

et le déplacement f à portée mondiale résout le problème aussi:

let f: ('a -> string) -> 'a -> string = fun g v -> g v 

let foo():string = 
    let h = string_of_int 
    in let i = string_of_float 
    in let x = f h 23 
    in let y = f i 23.0 
    in x^y

Pourquoi est-ce que le premier exemple ne compile pas tandis que les plus plus tard faire?

Answer 1

Permettez-moi un exemple plus simple qui illustre la question.

# let cons0 (x : 'a) (y : 'a list) = x :: y;; 
val cons0 : 'a -> 'a list -> 'a list = <fun> 
# let cons1 (x : 'a) (y : 'a list) = x :: y in cons1 1 [];; 
- : int list = [1] 
# let cons2 (x : 'a) (y : 'a list) = x :: y in (cons2 1 [], cons2 true []);; 
This expression has type bool but is here used with type int 
# let cons3 x y = x :: y in (cons3 1 [], cons3 true []);; 
- : int list * bool list = ([1], [true]) 

cons0 est une définition de fonction polymorphes, définie à la portée mondiale. C'est juste un emballage trivial à l'opérateur ::. Sans surprise, la définition fonctionne. cons1 est presque le même que cons0, sauf que sa portée est limitée à l'expression dans le corps in. Le changement de portée semble inoffensif, et bien sûr, il typechecks. cons3 est à nouveau la même fonction, sans annotation de type, et nous pouvons l'utiliser de façon polymorphique dans le corps in.

Alors, quel est le problème avec cons2? Le problème est la portée de 'a: c'est la phrase entière de toplevel.La sémantique de la phrase qui définit cons2 est

for some type 'a, (let cons2 (x : 'a) (y : 'a list) = ... in ...) 

Depuis 'a doit être compatible avec int (en raison de cons3 1 []) et bool (en raison de cons3 true [], il n'y a pas instanciation possible de 'a. Par conséquent, l'expression est mal typé.

Si vous aimez penser à taper ML en termes de son algorithme habituel inférence de type, chaque variable explicite de l'utilisateur introduit un ensemble de contraintes dans l'algorithme d'unification. ici, les contraintes sont 'a = "type of the parameter x" et ' = "type of the parameter y". Mais le sco pe de 'a est l'ensemble de la phrase, il n'est pas généralisé dans une portée interne. Ainsi, int et bool finissent tous deux unifiés au non-généralisé 'a.

Versions récentes OCaml introduit des variables de type scoped (comme dans Niki Yoshiuchi's answer). Le même effet aurait pu être atteint avec un module local dans les versions antérieures (de ≥2.0):

let module M = struct 
    let cons2 (x : 'a) (y : 'a list) = x :: y 
    end in 
(M.cons2 1 [], M.cons2 true []);; 

(note standard MLers:. C'est un endroit où OCaml et SML diffèrent)

Answer 2

Ceci est un vrai gratte-tête et je ne serais pas surpris s'il s'agit d'un bug du compilateur. Cela dit, vous pouvez faire ce que vous voulez en nommant explicitement le type:

let f (type t) (g: t->string) (v: t) = g v in 

A partir du manuel: http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#htoc108

Edit:

Cela fonctionne aussi:

let f g v:string = g v in 

qui a la signature de type que vous recherchez: ('a -> string) -> 'a -> string

Étrange que cela ne fonctionne pas lorsque vous annotez le type des arguments.

EDIT:

annotations de type polymorphes ont une syntaxe particulière:

let f: 'a. ('a -> string)-> 'a -> string = fun g v -> g v in 

Et le type est nécessaire pour être polymorphes: http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc79

Answer 3

En tant que point de référence , l'équivalent F #

let foo():string = 
    let f: ('a -> string) -> 'a -> string = fun g v -> g v 
    let h = string 
    let i = string 
    let x = f h 23 
    let y = f i 23.0 
    x^y 

compile.