Тип в функциональном программировании (OCaml)

Question

Я изучаю функциональное программирование и не понимаю типы в OCaml, и я не нашел ничего по-настоящему полезного.

У меня есть этот код:

let rec map2 f l1 l2 =
          match (l1,l2) with
          ([], _) -> []
        | (_, []) -> []
        | (x::l1s,y::l2s) -> (f x y) :: map2 f l1s l2s;;


let pick n m =
      if n > m then (fun b x -> if b then x+1 else x*2)
      else (fun b x -> if b then x+2 else x*4);;

map2 (pick 7 9) [true;false] [3;4;5;6];;

То, что мне трудно понять, шаги, чтобы узнать тип такого рода функций (map2, pick).

Я немного знаю, как работает подпись, правильное ассоциативное свойство и что символ " '" относится к универсальному типу.

Решение:

pick: 'a -> 'a -> bool -> int -> int = <fun>
map2: ('a->'b->'c) -> 'a list -> 'b list -> 'c list

Я не понимаю, почему bool -> int и почему в карте bool отсутствует в параметре функции.

Любые ссылки на книги, ссылка приветствуется

Answer 1

Если вы посмотрите на pick, то увидите, что он принимает 2 аргумента, а затем возвращает функцию. То, что он возвращает, (то же самое для другого веселья):

(fun b x -> if b then x+1 else x*2)

Конструкция "if" имеет форму if <bool> then <'a> else <'a>. Так что b должно быть bool, в то время как x все еще может быть 'a. Идем глубже - x+1. Таким образом, х должно быть int, а результат тоже int.

Таким образом, вышеуказанная функция имеет значение bool -> int -> int, и шляпа отображается в виде выбора.

Что касается map2: функция map2 может работать с любой функцией вида 'a -> 'b -> 'c в качестве первого аргумента. В вашем примере вы передаете bool -> int -> int, но это не ограничивает map2 этим типом. Ваш код может продолжаться с

let pick_f n m =
      if n > m then (fun b x -> if b then x +. 1. else x *. 2.)
      else (fun b x -> if b then x +. 2. else x *. 4.);;

map2 (pick_f 7 9) [true;false] [3.;4.;5.;6.];;

pick_f: 'a -> 'a -> bool -> float -> float = <fun>

Используется та же функция map2, но здесь с bool -> float -> float в качестве типа первого аргумента. Функция map2 полиморфна (то, что вы назвали универсальной) и может работать со многими типами.

Answer 2

pick: 'a -> 'a -> bool -> int -> int = <fun>
map2: ('a->'b->'c) -> 'a list -> 'b list -> 'c list

То, что вы видите здесь, - это процесс в функциональном программировании, называемый curry . Чтобы понять это, давайте рассмотрим более простой пример. Допустим, у вас есть функция f, которая принимает 2 аргумента X и Y и выводит Z. Как мы обычно пишем это

f(X, Y) = Z

Давайте посмотрим на это по-другому - у нас есть функция f, и если мы дадим ей X, а затем Y, она даст нам Z. Что произойдет, если мы дадим f 1 аргумент X? Давайте проверим это!

let plus a b = a + b;;

Этот код определяет функцию plus, которая принимает 2 аргумента a и b и возвращает их сумму. Если вы введете plus 1 1;; в utop, вы получите 2. Теперь вывод при вводе

plus 1;;

это

- : int -> int = <fun>

Это означает, что plus(1) фактически производит ФУНКЦИЮ, которая принимает int и выводит int! Подождите минуту, изначально у нас есть функция, которая производит целое число, и вдруг эта же функция производит ... FUNCTION? Что происходит?

Ключевой идеей здесь является представление о функции как о процессе, который использует аргументы один за другим . В духе этого, функция plus выше похожа на процесс, который потребляет 2 аргумента: если вы дадите ему только 1 аргумент, он остановится и будет ждать 2 аргумента. И этот остановленный процесс в точности аналогичен процессу, который потребляет 1 аргумент: передайте ему оставшийся ингредиент, и он начнет размолоть, чтобы получить ожидаемый результат.

Чтобы увидеть, как эта перспектива может помочь вам понять неясный способ написания сигнатуры функции в вашем примере, давайте посмотрим на функцию pick:

let pick n m =
  if n > m then (fun b x -> if b then x+1 else x*2)
  else (fun b x -> if b then x+2 else x*4);;

pick принимает 2 аргумента, n и m, и выводит функцию f, которая принимает 2 аргумента b и x. Определение f зависит от сравнения. Если n > m, то выводится функция fun b x, определение которой if b then x+1 else x*2. Иначе, он выводит функцию fun b x, определение которой if b then x+2 else x*4.

Если бы мы написали приблизительную сигнатуру для pick на основе вышеизложенного понимания, это было бы что-то вроде:

pick: (n, m) -> (function f that takes in b and x, and output some number)

В свете нашего понимания карри pick похоже на процесс, который потребляет n, а затем m. Таким образом, подпись также может быть написана так:

pick: n -> m -> (function f that takes in b and x, and output some number)

О, эй, эту функцию f можно также рассматривать как процесс, который потребляет b, а затем x, поэтому мы можем также написать:

pick: n -> m -> (b -> x -> some number)

, который выглядит поразительно похожим на:

pick: 'a -> 'a -> bool -> int -> int = <fun>

Теперь, как, черт возьми, OCaml знает, что b должно быть bool, а x и some number - int, в OCaml есть функция с именем type умозаключение . По сути, компилятор смотрит на операции, которые вы выполняете над переменными, и пытается угадать их типы. Например. Я вижу if b в коде, поэтому b должно быть bool.

В итоге , этот неясный способ написания сигнатуры функции называется curry , и как OCaml узнает, что b является bool, через функцию, называемую вывод типа в OCaml. Это должно облегчить поиск.