Типизированный FP: Аргументы Tuple и Curriable Arguments

Question

В статически типизированных функциональных языках программирования, таких как Standard ML, F #, OCaml и Haskell, функция обычно пишется с параметрами, отделенными друг от друга и от имени функции просто пробелами:

let add a b =
    a + b

Типом здесь является "int -> (int -> int)", то есть функция, которая принимает int и возвращает функцию, которая в свою очередь принимает и int и которая, наконец, возвращает int. Таким образом, карри становится возможным.

Также возможно определить аналогичную функцию, которая принимает кортеж в качестве аргумента:

let add(a, b) =
    a + b

В этом случае тип становится "(int * int) -> int".

С точки зрения дизайна языка, есть ли причина, по которой нельзя просто определить эти два типа в алгебре типов? Другими словами, так что «(a * b) -> c» сводится к «a -> (b -> c)», что позволяет одинаково легко каррировать оба варианта.

Я предполагаю, что этот вопрос возник, когда были разработаны языки, подобные четырем, которые я упомянул. Так кто-нибудь знает какую-либо причину или исследование, указывающее, почему все четыре из этих языков решили не «объединять» эти шаблоны двух типов?

Answer 1

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

Почему это так? Стандартный ML - самый старый из этих языков, и когда люди впервые писали компиляторы ML, не было известно, как эффективно обрабатывать аргументы с каррированием. (В корне проблемы лежит тот факт, что любая карри функция могла бы быть частично применена другим кодом, который вы еще не видели, и вы должны скомпилировать его с такой возможностью в виду.) С тех пор, как был разработан Standard ML, компиляторы улучшились, и вы можете прочитать о состоянии дел в превосходной статье Саймона Марлоу и Саймона Пейтона Джонса .

LISP, который является самым старым из всех функциональных языков, имеет конкретный синтаксис, который крайне неприемлем для карри и частичного применения. Hrmph.

Answer 2

По крайней мере, одна из причин не объединять каррированные и нетуристические функциональные типы состоит в том, что было бы очень запутанным, когда кортежи используются в качестве возвращаемых значений (удобный способ в этих типизированных языках для возврата нескольких значений). В системе схожих типов, как функция может оставаться хорошо компонуемой? Будет ли a -> (a * a) также преобразовываться в a -> a -> a? Если да, то (a * a) -> a и a -> (a * a) относятся к одному типу? Если нет, то как бы вы сочинили a -> (a * a) с (a * a) -> a?

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

apply f a b = f a b
vecSum (a1,a2) (b1,b2) = (a1+b1,a2+b2)

Теперь, возможно, ваше решение могло бы понять map (vecSum (1,1)) [(0,1)], но как насчет эквивалента map (apply vecSum (1,1)) [(0,1)]? Это становится сложным! Означает ли ваша самая полная распаковка, что (1,1) распаковывается с аргументами apply a & b apply? Это не намерение ... и в любом случае рассуждение становится сложным.

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

Answer 3

Расширение комментариев под хорошим ответом Намина:

Итак, предположим, что функция имеет тип 'a -> ('a * 'a):

let gimme_tuple(a : int) =
    (a*2, a*3)

Тогда предположим, что функция имеет тип ('a * 'a) -> 'b:

let add(a : int, b) =
    a + b

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

let foo = add(gimme_tuple(5))
// foo gets value 5*2 + 5*3 = 25

Но тогда вы можете представить себе полиморфную функцию, которая занимает место add в последнем фрагменте кода, например, небольшую функцию, которая просто принимает 2-кортеж и составляет список из двух элементов:

let gimme_list(a, b) =
    [a, b]

Это будет иметь тип ('a * 'a) -> ('a list). Состав сейчас будет проблематичным. Рассмотрим:

let bar = gimme_list(gimme_tuple(5))

Будет ли bar иметь значение [10, 15] : int list или будет bar функцией типа (int * int) -> ((int * int) list), которая в конечном итоге выдаст список, заголовком которого будет кортеж (10, 15)? Чтобы это сработало, в комментарии к ответу Намина я указывал, что в системе типов потребуется дополнительное правило, согласно которому привязка фактических к формальным параметрам должна быть «максимально возможной», т. Е. Что система должна предпринимать попытки частичного связывания. сначала и только попробуйте частичное связывание, если полное связывание недостижимо. В нашем примере это будет означать, что мы получим значение [10, 15], поскольку в этом случае возможна полная привязка.

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

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

Answer 4

Кортежи на этих языках отсутствуют просто для использования в качестве параметров функции. Это действительно удобный способ представления структурированных данных, например, 2D-точки (int * int), элемента списка ('a * 'a list) или узла дерева ('a * 'a tree * 'a tree). Помните также, что структуры являются просто синтаксическим сахаром для кортежей. То есть.,

type info = 
  { name : string;
    age : int;
    address : string; }

- это удобный способ обработки (string * int * string) кортежа.

Нет фундаментальной причины, по которой вам нужны кортежи в языке программирования (вы можете создавать кортежи в лямбда-исчислении так же, как вы можете использовать логические и целые числа & mdash; действительно, используя curry *), но они удобны полезно.

* Например,

tuple a b = λf.f a b
fst x     = x (λa.λb.a)
snd x     = x (λa.λb.b)
curry f   = λa.λb.f (λg.g a b)
uncurry f = λx.x f

Answer 5

Возможно, потому что полезно иметь кортеж в качестве отдельного типа, а также полезно хранить разные типы отдельно?

В Хаскеле, по крайней мере, довольно легко перейти от одной формы к другой:

Prelude> let add1 a b = a+b
Prelude> let add2 (a,b) = a+b
Prelude> :t (uncurry add1)
(uncurry add1) :: (Num a) => (a, a) -> a
Prelude> :t (curry add2)
(curry add2) :: (Num a) => a -> a -> a

, поэтому uncurry add1 такое же, как add2, а curry add2 такое же, как add1. Я думаю, что подобные вещи возможны и на других языках. Какую выгоду получит автоматическое каррирование каждой функции, определенной в кортеже? (Так как это то, что вы, кажется, спрашиваете.)