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

Я сделал функцию, которая называется 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

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

1 ответ

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

    Когда алгоритм пытается определить тип for 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))
    

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

    Выход SML/NJ для измененного случая:

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