Об определении «многопараметрических» функций путем частичного применения в Haskell -подобных языках

Question

Итак. Я на самом деле возиться с языком Idris, немного следуя за Type-Driven Development Брейди с Idris . Я не думаю, что я написал здесь , который связан с конкретным c языком программирования (и я не знаю Haskell, если на то пошло). Но я не знаю, где еще я мог бы опубликовать это, учитывая, что у меня нет знаний о частичном применении / карри, типах, лямбдах и всем прочем с точки зрения математика.

Некоторый контекст

Во второй главе книги автор др. aws обратил внимание на следующий сценарий.

Учитывая самообъясняющийся фрагмент

double : Num a => a -> a
double x = x + x

rotate : Shape -> Shape

, где Shape : Type и rotate - это отверстия для типа фигуры и для функции, которая поворачивает Shape на 90 градусов соответственно, за функциями quadruple и turn-around

quadruple : Num a => a -> a
quadruple x = double (double x)

turn_around : Shape -> Shape
turn around x = rotate (rotate x)

* 1022 существует очевидная закономерность * что привело нас к написанию

twice (старшей) функции, способной применять два раза один и тот же оператор.

На мой взгляд, в большинстве случаев есть два способа решения проблемы. Первый - просто следовать коду Брэди

twice : (ty -> ty) -> ty -> ty
twice f x = f (f x)

, где он фактически определяет изображение twice f : ty -> ty функции twice над произвольным f ¹ .

Второй вариант, который мне кажется немного более элегантным, - определить twice с помощью функции composite и / или анонимной функции, немного изменив ее сигнатуру

* 1040. *

Оба подхода приводят к конечному результату

turn_around : Shape -> Shape
turn_around = twice rotate

Вопрос (ы)

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

1. Допустим, у нас есть «многопараметрическая» функция

   f : ty_1 -> ty_2 -> ... -> ty_n
   

   Тогда f - это функция, принимающая x_1 : ty_1 в другая функция f x_1 : ty_1 -> ... -> ty_n. Когда мы должны выбрать определение f, написав

   f x_1 = stuff
   

   вместо

   f x_1 ... x_{n-2} = stuff2
   

2. Может кто-нибудь объяснить мне различия между двумя подходами (Брейди и мой ) сообщалось выше?

---

¹ Да, я учусь на математике ...

Answer 1

Нет жесткого и быстрого «правила», определяющего, когда следует использовать один стиль над другим.

Функция, определенная как

f x = \y => ...

, точно равна функции, определенной как

f x y = ...

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

Для композиции функций вы написали

composite g f = \x => g (f x)

, поскольку композиция обычно рассматривается как 2 -функция Мы могли бы также написать

composite g f x = g (f x)

, но это, хотя и короче, не так ясно, так как это предлагает читателю-человеку рассмотреть composite как 3-арную функцию. Будучи человеком, я также предпочитаю первую форму, но для компьютера не было бы никаких предпочтений.

Если бы я не мог использовать композицию, как вы, я написал бы код Брэди как

twice f = \x => f (f x)

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

---

Наконец, более математическое примечание: с фундаментальной точки зрения нет необходимости в обозначении

f x1 ... xn = stuff

, которое мы обычно используем для определения функции. Чтобы быть чрезвычайно педантичным c, вышеприведенное фактически не определяет f, а только определяет, как f ведет себя применительно к n аргументам. Поскольку мы знаем, что это однозначно идентифицирует f, нас это не волнует. Но если бы мы это сделали, мы бы определили f, как мы определяем что-либо еще, то есть с помощью определяющего уравнения вида

f = something

и, в частности,

f = \x1 .. x2 => stuff

Итак, каждый определение формы f x1 .. xn = ... с n>0 можно рассматривать как syntacti c sugar : обозначение, которое мы можем использовать для программирования, но которое мы можем игнорировать при изучении теории, связанной с языком программирования , Конкретно, если мне нужно математически доказать свойство во всех программах P, мне не нужно рассматривать случаи, когда P использует сахар syntacti c, а только случаи, когда каждое уравнение имеет вид f = ..., возможно, с лямбдами. Это упрощает доказательство, поскольку нам нужно иметь дело с меньшим количеством случаев.

Теперь я не знаю слишком много Идриса, поэтому я не знаю, возможно ли это преобразование в лямбды во всех случаях, в Идрисе , В Агде это было бы невозможно, например, из-за того, как выполняется зависимое исключение. В Coq это было бы возможно. Пока вам не нужны зависимые типы, у вас все будет хорошо.