Типы ввода OCaml

Я изучаю OCaml, и до сих пор мне трудно понять концепции типов.

Например, если у нас есть следующий код:

# let func x = x;;
val func : 'a -> 'a = <fun>

На официальном сайте мне сообщается, что 'a перед стрелкой — это неизвестный тип ввода, а 'a после стрелки — это вывод.

Однако, когда я пытаюсь использовать композицию функций:

# let composition f x = f(x);;
val composition : ('a -> 'b) -> 'a -> 'b = <fun>

Что означает ('a -> 'b)? 'a связано с f и 'b связано с x?

Другая функциональная композиция, которая меня еще больше запутала:

# let composition2 f x = f(f(x));;
val composition2 : ('a -> 'a) -> 'a -> 'a = <fun>

Я действительно не понимаю, почему у нас нет 'b в этом случае.

Заранее спасибо!


functional-programming ocaml
person hyperbug    schedule 02.03.2021    source источник
comment
Это не композиция, это приложение.   -  person leftaroundabout    schedule 03.03.2021

Ответы (1)


arrow_upward
2
arrow_downward

'a -> 'b — это тип функции, которая принимает один аргумент типа 'a и возвращает значение типа 'b.

val composition : ('a -> 'b) -> 'a -> 'b означает, что composition является функцией двух аргументов:

  1. первый имеет тип ('a -> 'b), поэтому функция, как указано выше
  2. второй типа 'a

Таким образом, эта функция возвращает нечто того же типа, что и возвращаемый тип первого аргумента, 'b. Действительно, он берет функцию и ее аргумент и применяет эту функцию к аргументу.

Во втором случае вы можете работать в обратном направлении от внутреннего вызова. Давайте посмотрим на f(f(x))

  1. x — это что-то любого типа 'b. Мы еще не знаем, что это за тип.
  2. Поскольку у нас есть f(x), f должна быть функцией типа 'b -> 'c. Это 'b, потому что мы знаем, что он принимает x в качестве входных данных, а x имеет тип 'b.
  3. Таким образом, тип composition2 равен ('b -> 'c) -> 'b
  4. Поскольку у нас есть f(f(x)), тип аргумента f должен совпадать с типом возвращаемого значения. Итак, 'b == 'c. Назовите этот тип 'a.
  5. Поскольку x имеет тип 'b, который совпадает с 'a, x должен иметь тип 'a.
  6. Поскольку f имеет тип 'b -> 'c, где 'b == 'a и 'c == 'a, f должен иметь тип 'a -> 'a.
  7. Таким образом, тип composition2 равен ('a -> 'a) -> 'a
person ForceBru    schedule 02.03.2021
comment
Теперь так много смысла. Спасибо за пояснение! - person hyperbug; 03.03.2021