подписи/типы в функциональном программировании (OCaml)

Question

Я начал изучать функциональное программирование (OCaml), но я не понимаю одну важную тему о подписях fp: (я не уверен, что это собственное имя). Когда я что-то типа и компилировать с OCaml, я получаю, например:

# let inc x = x + 1 ;; 
val inc : int -> int = <fun> 

Это тривиально, но я не знаю, почему это:

let something f g a b = f a (g a b) 

дает выход:

val something : (’a -> ’b -> ’c) -> (’a -> ’d -> ’b) -> ’a -> ’d -> ’c = <fun> 

Я полагаю, что эта тема является абсолютно основами fp для многих из вас, но я прошу о помощи здесь, потому что я не нашел что-нибудь в Интернете о подписях в OCaml (есть некоторые статьи о подписях в Haskell, но не объяснения).

Если эта тема как-то выжить, я выкладываю здесь несколько функций, которые подписи заставили меня путать:

# let nie f a b = f b a ;; (* flip *) 
val nie : (’a -> ’b -> ’c) -> ’b -> ’a -> ’c = <fun> 

# let i f g a b = f (g a b) b ;; 
val i : (’a -> ’b -> ’c) -> (’d -> ’b -> ’a) -> ’d -> ’b -> ’c = <fun> 


# let s x y z = x z (y z) ;; 
val s : (’a -> ’b -> ’c) -> (’a -> ’b) -> ’a -> ’c = <fun> 

# let callCC f k = f (fun c d -> k c) k ;; 
val callCC : ((’a -> ’b -> ’c) -> (’a -> ’c) -> ’d) -> (’a -> ’c) -> ’d = <fun> 

Благодарим Вас за помощь и разъяснения.

Answer 1

Есть несколько понятий, которые вы должны понять смысл этого типа подписи, и я не знаю, какие из них вы уже делаете, так что я старался изо всех сил, чтобы объяснить все важные концепции:

Карринг

Как известно, если у вас есть тип foo -> bar, это описывает функцию, принимающую аргумент типа foo и возвращающий результат типа bar. Так как -> является правильным ассоциативным, тип foo -> bar -> baz совпадает с foo -> (bar -> baz) и поэтому описывает функцию, принимающую аргумент типа foo и возвращающий значение типа bar -> baz, что означает, что возвращаемое значение является функцией, принимающей значение типа bar и возвращающее значение типа baz.

Такая функция может быть названа, как my_function my_foo my_bar, который из-за применение функции лево-ассоциативно, является таким же, как (my_function my_foo) my_bar, т.е. применяется my_function к аргументу my_foo, а затем применяет функцию, которая возвращается в результате к аргументу my_bar.

Поскольку его можно так называть, функцию типа foo -> bar -> baz часто называют «функцией, принимающей два аргумента», и я сделаю это в оставшейся части этого ответа.

Тип переменных

Если определить функцию как let f x = x, он будет иметь тип 'a -> 'a. Но 'a на самом деле не является типом, определенным в стандартной библиотеке OCaml, так что это?

Любой тип, начинающийся с ', является так называемой переменной . Переменная типа может соответствовать любому возможному типу. Таким образом, в приведенном выше примере f можно вызвать с помощью int или string или list или вообще ничего - это не имеет значения.

Кроме того, если переменная того же типа появляется в сигнатуре типа более одного раза, она будет стоять за один и тот же тип. Таким образом, в приведенном выше примере это означает, что возвращаемый тип f совпадает с типом аргумента. Поэтому, если f вызывается с int, он возвращает int. Если он вызывается с string, он возвращает string и так далее.

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

Одна заметка о выводе типа: Если вы явно не указали функцию подписи типа, OCaml всегда будет выводить наиболее общий тип, который вам подходит. Поэтому, если функция не использует какие-либо операции, которые работают только с данным типом (например, +), предполагаемый тип будет содержать переменные типа.

Теперь, чтобы объяснить тип ...

val something : ('a -> 'b -> 'c) -> ('a -> 'd -> 'b) -> 'a -> 'd -> 'c = <fun> 

Этот тип подписи говорит вам, что something функция принимает четыре аргумента.

Тип первого аргумента - 'a -> 'b -> 'c. То есть функция, принимающая два аргумента произвольных и, возможно, разных типов и возвращающих значение произвольного типа.

Тип второго аргумента - 'a -> 'd -> 'b. Это снова функция с двумя аргументами. Здесь важно отметить, что первый аргумент функции должен иметь тот же тип, что и первый аргумент первой функции, а возвращаемое значение функции должно иметь тот же тип, что и второй аргумент первой функции.

Тип третьего аргумента: 'a, который также является типом первых аргументов обеих функций.

И, наконец, тип четвертого аргумента - 'd, который является типом второго аргумента второй функции.

Возвращаемое значение будет иметь тип 'c, то есть тип возврата первой функции.

Answer 2

Если вы действительно заинтересованы в предмете (и имеете доступ к университетской библиотеке), прочитайте превосходный (хотя и несколько устаревший) Wadler «Введение в функциональное программирование». Он объясняет типовые подписи и тип вывода очень приятным и понятным способом.

Другие дополнительные советы: обратите внимание, что стрелка -> является право-ассоциативной, поэтому вы можете скопировать вещи справа, что иногда помогает понять вещи, то есть a -> b -> c - это то же самое, что и a -> (b -> c). Это связано со вторым намеком: функции более высокого порядка. Вы можете делать вещи, как

let add x y = x + y 
let inc = add 1 

так в FP, думая о «добавить» как функцию, которая должна принимать два численных параметров и возвращает численное значение обычно не, что нужно сделать: It также может быть функцией, которая принимает один численный аргумент и возвращает функцию с типом num -> num.

Понимание этого поможет вам понять сигнатуры типов, но вы можете сделать это без него. Здесь быстро и просто:

# let s x y z = x z (y z) ;; 
val s : (’a -> ’b -> ’c) -> (’a -> ’b) -> ’a -> ’c = <fun> 

Посмотрите на правую сторону. y дается один аргумент, поэтому он имеет тип a -> b, где a - тип z. x дается два аргумента, первый из которых - z, поэтому тип первого аргумента должен быть также a. Тип (y z), второй аргумент, равен b, и, следовательно, тип x равен (a -> b -> c). Это позволяет сразу выводить тип s.