Карри (язык программирования)

Эта статья о языке программирования Curry (названном в честь математика и логика). Информацию о математике и логике см. в Haskell Curry . Чтобы узнать о технике информатики, см. Карринг .

Карри

Парадигма	функциональный , логический , нестрогий, модульный
Разработано	Майкл Ханус, Серджио Антой и др.
Разработчик	Как университет Мюнхенский университет Людвига-Максимилиана Университет Мюнстера Портлендский государственный университет Мадридский университет Комплутенсе Технический университет Мадрида
Впервые появился	1995 год ( 1995 )
Стабильная версия	3.6.0   / (10 ноября 2023 г.)
Дисциплина набора текста	статический , сильный , предполагаемый
Платформа	х86-64
ТЫ	Кроссплатформенность : Linux
Лицензия	BSD 3-пункт
Веб-сайт	карри .страницы .ps .Информатика .uni-подобный .из /карри-ланг .org
Основные реализации
PAKCS ( Prolog цель ), mcc ( C цель ), KiCS2 ( Haskell ) цель
Под влиянием
Хаскель , Пролог

Curry — декларативный язык программирования , реализация парадигмы функционального логического программирования . и основан на языке Haskell . Он объединяет элементы функционального и логического программирования. включая интеграцию программирования в ограничениях .

Это почти расширенный набор Haskell, но он не поддерживает все языковые расширения Haskell. В отличие от Haskell, Curry имеет встроенную поддержку недетерминированных вычислений, включающих поиск.

Основы функционально-логического программирования

Основные понятия

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

double x = x+x

Выражение « двойная 1 » заменяется на 1+1 . Последний можно заменить на 2, если интерпретировать оператор « + » определяется бесконечным набором уравнений, например, 1+1 = 2 , 1+2 = 3 и т. д. Аналогичным образом можно вычислять вложенные выражения (где заменяемые подвыражения заключаются в кавычки):

'double (1+2)' → '(1+2)'+(1+2) → 3+'(1+2)' → '3+3' → 6

Есть и другой порядок вычислений, если заменить аргументы операторов справа налево:

'double (1+2)' → (1+2)+'(1+2)' → '(1+2)'+3 → '3+3' → 6

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

Как и многие функциональные языки, такие как Haskell , Curry поддерживает определение алгебраических типов данных путем перечисления их конструкторов. Например, тип логических значений состоит из конструкторов Правда и False , которые объявляются следующим образом:

 data Bool = True | False

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

 not True = False
 not False = True

Принцип замены равных равными по-прежнему действует при условии, что фактические аргументы имеют требуемую форму, например:

not '(not False)' → 'not True' → False

Более сложные структуры данных можно получить с помощью рекурсивных типов данных . Например, список элементов, где тип элементов произвольный (обозначается переменная типа a ), является либо пустым списком « [] » или непустой список « x:xs », состоящий из первого элемента х и список хз :

 data List a = [] | a : List a

Тип « Список а » обычно записывается как [a] и конечные списки x1 : х2 : ... : хн :[] записываются как [ х1 , х2 , ... , хн ] . Мы можем определять операции над рекурсивными типами с помощью индуктивных определений, где сопоставление с образцом поддерживает удобное разделение различных случаев. Например, операция конкатенации « ++ » в полиморфных списках можно определить следующим образом (необязательное объявление типа в первой строке указывает, что « ++ » принимает на вход два списка и создает выходной список, в котором все элементы списка имеют один и тот же неопределенный тип):

 (++) :: [a] -> [a] -> [a] 
 [] ++ ys = ys 
 (x:xs) ++ ys = x : xs++ys

Помимо применения для различных задач программирования, операция « ++ » также полезен для указания поведения других функций в списках. Например, поведение функции Last, которая возвращает последний элемент списка, можно определить следующим образом: для всех списков xs и элементов e, последний xs = e, если ∃ys : да ++[ и ] = хз.

На основе этой спецификации можно определить функцию, удовлетворяющую этой спецификации, используя функции логического программирования. Подобно логическим языкам, языки функциональной логики обеспечивают поиск решений для экзистенциально кванторных переменных. В отличие от языков чистой логики, они поддерживают решение уравнений над вложенными функциональными выражениями, поэтому уравнение типа ys ++[ и ] = [1,2,3] решается путем создания экземпляра ys в списке [1,2] и e к значению 3 . В Curry можно определить последнюю операцию следующим образом:

 last xs | ys++[e] =:= xs = e where ys,e free

Здесь символ « =:= ” используется для эквациональных ограничений, чтобы обеспечить синтаксическое отличие от определения уравнений. Аналогично, дополнительные переменные (т. е. переменные, не встречающиеся в левой части определяющего уравнения) явно объявляются как « где...бесплатно », чтобы предоставить некоторые возможности для обнаружения ошибок, вызванных опечатками. Условное уравнение вида l | с = r применимо для редукции, если решено его условие c. В отличие от чисто функциональных языков, где условия оцениваются только по логическому значению, языки функциональной логики поддерживают решение условий путем угадывания значений неизвестных в условии. Сужение, как обсуждается в следующем разделе, используется для решения подобных условий.

Сужение

Сужение — это механизм, при котором переменная привязывается к значению, выбранному из альтернатив, налагаемых ограничениями. Каждое возможное значение проверяется в определенном порядке, при этом остальная часть программы вызывается в каждом случае для определения достоверности привязки. Сужение — это расширение логического программирования, поскольку оно выполняет аналогичный поиск, но фактически может генерировать значения как часть поиска, а не ограничиваться их проверкой.

Сужение полезно, поскольку позволяет рассматривать функцию как отношение: ее значение можно вычислить «в обоих направлениях». Примеры Карри из предыдущего раздела иллюстрируют это.

Как отмечалось в предыдущем разделе, сужение можно рассматривать как сокращение графа терминов программы, и часто существует множество различных способов ( стратегий ) сокращения данного графа терминов. Антой и др. В 1990-е годы было доказано, что определенная стратегия сужения ( need сужение ) оптимальна в смысле выполнения ряда сокращений для достижения «нормальной формы», соответствующей решению, которое является минимальным среди надежных и полных стратегий. Необходимое сужение соответствует ленивой стратегии, в отличие от SLD-разрешения стратегии Пролога .

Функциональные шаблоны

Правило, определяющее последний показанный выше факт выражает тот факт, что фактический аргумент должен соответствовать результату сужения выражения ys++[e] . Карри может выразить это свойство также следующим более кратким способом:

 last (ys++[e]) = e

Haskell не допускает такого объявления, поскольку шаблон в левой части содержит определенную функцию ( ++ ). Такой шаблон еще называют функциональным шаблоном . Функциональные шаблоны реализуются благодаря сочетанию функциональных и логических функций Curry и поддерживают краткие определения задач, требующих глубокого сопоставления шаблонов в иерархических структурах данных.

Недетерминизм

Поскольку Карри способен решать уравнения, содержащие вызовы функций с неизвестными значениями, его механизм выполнения основан на недетерминированных вычислениях, аналогично логическому программированию. Этот механизм также поддерживает определение недетерминированных операций , т. е. операций, которые выдают более одного результата для данного ввода. Архетипом недетерминированных операций является предопределенная инфиксная операция. ? , называемый оператором выбора , который возвращает один из своих аргументов. Этот оператор определяется следующими правилами:

 x ? y = x
 x ? y = y

Таким образом, оценка выражения 0 ? 1 возврат 0, а также 1 . Вычисления с недетерминированными операциями и вычисления со свободными переменными путем сужения имеют одинаковую выразительную силу.

Правила, определяющие ? покажем важную особенность Карри: все правила перебираются для того, чтобы оценить какую-то операцию. Следовательно, можно определить по

 insert x ys     = x : ys
 insert x (y:ys) = y : insert x ys

операция вставки элемента в список в неопределенную позицию, чтобы операция Пермь определяется

 perm []     = []
 perm (x:xs) = insert x (perm xs)

возвращает любую перестановку данного входного списка.

Стратегии

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

Внешние ссылки

• Официальный сайт
• Smap — веб-среда выполнения для Curry и Haskell с различными примерами программ.
• Пакеты Curry — коллекция программных пакетов для Curry.
• MCC — компилятор Münster Curry, ориентирован на C
• PAKCS Основная реализация Curry, ориентированная на Пролог.
• KiCS2 Реализация Curry, ориентированная на Haskell.
• Curry2Go Реализация Curry, ориентированная на Go и поддерживающая честный параллельный поиск.
• Список рассылки Карри
• Домашняя страница Михаэля Хануса
• Чисто функциональное ленивое недетерминированное программирование (Фишер, Киселев, Шан, 2009), Преобразование программ функциональной логики в монадические функциональные программы (Брассель, Фишер, Ханус, Рек, 2010) по моделированию ленивого недетерминированного (логического) программирования (например, в Карри) ) на чисто функциональном языке ( Haskell ); такой подход может дать программисту больше гибкости в контроле над стратегиями, которые — в случае Карри — являются встроенными.