Почему тип, предполагаемый для моей функции ML, отличается от ожидаемого?

Question

Я сделал функция это имя maptree. А ниже мой код:

datatype 'a tree = LEAF of 'a | NODE of 'a tree * 'a tree; 
fun maptree(f, NODE(X, Y)) = NODE(maptree(f, X), maptree(f, Y)) 
| maptree(f, LEAF(X)) = LEAF(f X); 

Я ожидал maptree иметь тип

('a -> 'a) -> 'a tree -> 'a tree 

, но тип, выведенный с помощью компилятора

('a -> 'b) * 'a tree -> 'b tree 

Почему это происходит?

Answer 1

Алгоритм ввода-вывода Hindley-Milner позволяет получить более общий тип, чем вы ожидали.

Когда алгоритм пытается вывести тип для maptree, он предполагает, что f: 'a -> 'b (из-за того, что вы используете f как функцию). И ничто не ограничивает тип f.

Если вы, например, определить функцию maptree следующим образом (я использовал f дважды в LEAF случае):

fun maptree(f, NODE(X, Y)) = NODE(maptree(f, X), maptree(f, Y)) 
    | maptree(f, LEAF(X)) = LEAF(f (f X)) 

Тогда механизм типа умозаключение бы ограничить тип f для 'a -> 'a (поскольку мы подаем выход функции на ее вход).

Выход SML/NJ для модифицированного случая:

val maptree = fn : ('a -> 'a) * 'a tree -> 'a tree