OCaml, Полиморфные Функции

Question

У меня нет большого опыта работы с OCaml. Мне нужна помощь в понимании полиморфных функций.

Код:

# let h x y z = if x then y else z val h : bool -> 'a -> 'a -> 'a = <fun>

# let i x y z = if x then y else y val i : bool -> 'a -> 'b -> 'a = <fun>

Вопрос:

Можете ли вы объяснить мне, почему вторая функция имеет 'b в качестве второго аргумента, а не' a, как первая функция?

Answer 1

Обе ветви if должны возвращать один и тот же тип. Подумайте, как бы выглядело, если бы оно не было встроенным:

val if : bool -> 'a -> 'a -> 'a

Теперь в вашем первом примере и y, и z используются в том случае, если они таковы, что они одного типа. Во втором примере, хотя z не используется, поэтому ничего не сказано об этом.

Answer 2

Это связано с типами, которые выводятся в ваших выражениях.

                        same type since both branches of an `if` expression must be same type
                        ↓      ↓
let h x y z = if x then y else z
                 ↑  
                 must be `bool` since its in the place of a condition

Итак, мы получаем

val h : bool -> 'a -> 'a -> 'a
        ↑        ↑     ↑     ↑
        x        y     z     return type
                same type

Со вторым выражением его аналогичная только одна из переменных не используется, поэтому его тип может быть любым (не ограничен никакими правилами в определении вашего выражения).

          unused, could be any type
          |             are the same variable, therefore same type
          ↓             ↓      ↓
let i x y z = if x then y else y
                 ↑  
                 must be `bool` since its in the place of a condition

Таким образом, мы получаем

val h : bool -> 'a -> 'b -> 'a
        ↑        ↑     ↑     ↑
        x        y     z     return type

Здесь и 'a, и 'b представляют некоторый произвольный тип, который не обязательно совпадает. Например, 'a может быть любого типа, но все 'a имеют одинаковый тип. То же самое касается 'b.

'a и 'b могут быть одного типа, но они не имеют . z во втором выражении относится к типу b', поскольку не имеет никаких ограничений по типу, поэтому он не обязательно должен быть типа 'a, как в первом выражении.