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

Материал из Национальной библиотеки им. Н. Э. Баумана
Последнее изменение этой страницы: 20:17, 1 июня 2016.
Hope
Парадигма процедурный
Спроектировано Кафедра компьютерных технологий Эдинбургского университет, Шотландия
Первый   появившийся 1970-1980
Печать дисциплины Сильная, динамическая
Под влиянием
LISP, NPL, ISWIM, PROLOG

Hope – функциональный язык программирования разработанный в 1970-х годах в Эдинбургском университете.

Краткий обзор

В данной статье описан и рассмотрен аппликативный язык под названием Hope. Основная цель разработки была создание очень простого языка программирования, который позволит составлять четкие и модернизируемые программы. Язык Hope не включает в себя оператор присваивания, что является важным его упрощением. Пользователь может свободно задавать свои собственные типы данных без потребности разрабатывать некое сложное кодирование с точки зрения типов низкого уровня. Язык очень сильно типизирован, он обеспечивает выполнение проверки типов, например обрабатывает полиморфные типы и перегруженные операторы. Функции определены рядом рекурсивных уравнений; левая сторона каждого уравнения включает в себя шаблон, который используется для того, чтобы определить какое уравнение необходимо использовать для данного аргумента. Наличие произвольных типов высшего порядка позволяет собирать функции в рекурсивные пакеты. Лениво-оцененные списки обеспечивают возможность использовать бесконечные списки, которые могут использоваться для обеспечения интерактивного ввод/вывод и параллелизма. Язык Hope также включает простое средство для модуляризации, которое может использоваться для защиты реализации абстрактного типа данных.

Введение

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

В данной статье, в первую очередь, перечислены некоторые аспекты языков программирования, которые способствуют точности и гибкости. Проиллюстрируем их, описывая разработанный и внедрённый аппликативный язык, названный hope. Приведем в пример программу, написанную на языке hope. И наконец, обсудим достоинства и недостатки языка Hope.

Концепции языка программирования Hope

Следующие аспекты играют важную роль в языке для написания правильных и гибких программ. Они перечислены кратко, однако они будут проиллюстрированы более подробно далее в описании языка hope.

Никаких присвоений: прозрачность ссылок

Аппликативные языки, которые работают с точки зрения выражений и их значений и используют рекурсию вместо циклов, кажутся намного более ясными и менее подверженные ошибкам. Выражения «прозрачны» в том смысле, что их значение зависит только от их текстового контекста, а не от некоторой вычислительной истории. Значение каждой переменной задаётся только однажды, при объявлении. Присвоения, которые изменяют структуру данных, особенно склонны приводить к ошибкам; отказ от их использования значительно упрощает язык, хотя это действительно замедляет выполнение программы.

Максимальное использование пользовательских типов

Пользователь должен задавать свои собственные типы каждый раз, когда это возможно; например тип 'age', вместо типа 'integer’. Машина должна проверить эти типы. Язык должен позволять полиморфные типы так, чтобы код мог быть максимально общим; например, list of alphas, а не определенный list of numbers, где alpha - переменная, которая может быть приведена к любому типу. Предполагаем, что большое количество ошибок вызваны осложнениями, созданными при кодировке данных обычными типами низкого уровня; создание простого и сильного средства для определения типов должно значительно упростить задачу программиста.

Перегруженные операторы

Удобно использовать общие операционные символы, такие как «+» или «eval» с различными значениями, согласно типу аргументов. Реализация должена быть в состоянии устранить неоднозначность таких перегруженных операторов (это требует некоторой тонкости для полиморфных типов).

Исчерпывающий анализ случая

У каждого типа данных будет ряд несвязных подтипов, каждый с различной функцией конструктором; например, в списки созданные с cons или nil не должно вызывать трудностей сделать анализ случая использования этих конструкторов и компилятор должен с легкостью проверить, исчерпывающий ли это анализ. Это позволяет избежать такой ошибки, как, например, остутствие проверки на пустой список.

Предотвращение ненужных имен

Не должен быть необходим ввод большого количество различных имён функций, чтобы создать структуру данных (например, cons), чтобы проверить, какой это подтип (например, указатель предиката null), или чтобы выбрать компоненты (например, car и cdr). Мы можем использовать только имя конструктора, а путем сопоставления синтаксиса с шаблоном позволит программе выполнить проверку и подобрать подходящее так, как это предписывает контекст.

Отмена явной рекурсии в максимально возможной степени

Учитывая, что мы хотим иметь язык без операции присваивания, мы будем использовать рекурсию вместо циклов. Однако неконтролируемое и неправильное использование рекурсии не желательно. Намного лучше использовать стандартные конструкции, связанные со структурами данных; например, {x2 : x ∈ S} как в математике (и SETL [12]) вместо рекурсии элемента S. В языке, который допускает функции высшего порядка (то есть, процедуры, использующие процедуры в качестве параметров), мы можем легко определить полезные функции высшего порядка, которые обёртывают рекурсию спасая от её явного написания. Пример - mapcar в LISP.

Превращение последовательностей в объекты данных

В традиционном стиле программирования последовательности иногда представляются как последовательные значения переменной; таким образом последовательность целых чисел представлена как значение переменной целого числа. Также возможно представлять их с помощью массива или списка, но тогда возникает недостаток, что все элементы последовательности должны находиться в памяти одновременно. Идея, которая была названа 'ленивая оценка' (lazy evaluation) Хендерсоном и Моррисом (Handerson&Morris) (первоначально благодаря Уодсуорт (Wadsworth)), позволяет нам иметь дело с такими последовательностями, как списки, но оценивая один элемент за раз по мере необходимости. Среди других вещей это позволяет достигнуть такого эффекта как сопрограмма на императивном языке программирования, но более проницательным способом, передавая «ленивый» список как результат функции. Это также позволяет обращаться с интерактивным вводом/выводом и параллелизмом в императивном языке.

Модульность и абстракция данных

Главная уловка в написании больших программ без ошибок состоит в их составлении из небольших отдельно написанных частей, каждая из которых максимально самостоятельна, с частями взаимодействующими друг с другом. Важной техникой достижения вышеизложенного служит абстракция данных. Это было исследовано как помощь хорошему стилю программирования на таких недавних языках как ALPHARD, CLU и ADA , который может быть рассмотрен, как развитие одного аспекта понятия класса SIMULA.

Абстрактный тип данных, такой, как 'set' или 'queue', определен рядом процедур, которые создают элементы типа и воздействуют на них. Внедрения этих процедур и представление самого типа скрыты от пользователя; его код полагается исключительно на указанные свойства абстрактного типа.

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

Описание языка Hope

Язык программирования hope, который иллюстрирует упомянутые выше концепции, был разработан и внедрен в Эдинбургском университете.

Цель состояла в том, чтобы разработать язык программирования, который был бы очень простым и ясным, а программы легко модифицируемы. Большое влияние на создание языка Hope оказали язык LISP и язык Лэндина ISWIM. Мы не пытались быть оригинальными; мы стремились подобрать разумный выбор известных и понятных идеи. Hope представляет собой некоторую смесь LISP, сильной типизации и модульности. Присутствует некоторое сходство со многими другими языками, такими как PROLOG, ML, SASL, OBJ, SCRATCHPAD, и языками, написанными Буржом (Burge lang.) и Бэкусом (Backus lang.).

Hope (в его существующем виде) – это эксперимент конструирования языка и одновременно средство тестирования определенных идей методологии программирования, а вовсе не окончательный язык программирования. Он все еще является незавершенным и ему не хватает «разумных» средств ввода/вывода.

Объявление данных

Концептуально, все данные в языке Hope представлены в качестве терм, состоящих из конструктора данных применительно к ряду субтерм, каждая из которых, в свою очередь представляет еще один пункт данных. Верхушки этого дерева являются нульарные конструкторы данных или функциональные объекты. Пример - Succ (suce (0)), в котором suec - унарный конструктор, и 0 - нульместным (т.е., константа). Функции конструкторов не интерпретируются; они просто выполняются.

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

data num == 0 ++ succ (num)

Объявляем тип данных num с помощью конструктора данных "0" и "succ". Таким образом элементы num следующие: 0, succ (0), succ (succ (0)), …; соответственно 0, 1, 2 … .

Что бы определить тип «tree-of-numbers» мы можем использовать:

data numtree == empty ++ tip (num)
  				      ++ node (numtree # numtree)

(символ # дает декартово произведение типов)

Одним из элементов numtree выступает:

node (tip(succ(0)),
	node (tip(succ(succ(0))), tip (0)))

Однако мы можем захотеть получить дерево листьев или, например, дерево деревьев не объявляя каждый элемент по отдельности. Объявим тип переменной typevar alpha , которая при использовании в выражениях может обозначать любой тип (включая второй и типы высшего порядка). Общее определение tree как параметрического типа теперь будет выглядить так:

data tree (alpha) == empty ++ tip (alpha)
                  ++ node (tree (alpha) # tree (alpha))

Теперь tree не является типом, а унарным конструктором типов – можем обойтись без numtree в пользу tree (num)

Другой пример объявления данных:

Data graph == mkg(set vertex 
		# (vertex#vertex->truval))

Это говорит, что graph (применен конструктор данных mkg) это комбинация вершин вместе с бинарным отношением, которое говорит, есть ли край (грань) между какими-либо двумя вершинами.

Язык hope легко сочетается с такими типами данных как: num, truval, char, list и set .

Выражения

Самыми простыми выражениями в языке hope служат - константы (т.е., конструкторы данных и функции - 'обычное' понятие константы - простой класс нульарных функций и конструкторов данных), и переменные.

Приложение может быть создано простым сочетанием двух выражений:

factorial 6

Для функций состоящих из нескольких параметров мы используем кортеж, сформированный с помощью запятых; таким образом 3,4 это 2-кортеж. Круглые скобки используются для группировки, например:

g (3,4)

В выражении:

(f x) y

подвыражение f x должно было бы произвести функцию; таким образом типы были бы : f : T1 -> T2 -> T3 with x : T1 and y : T3.

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

infix +, - : 8

Подобная форма также используется, чтобы присвоить приоритет префиксному символу.

Некоторые удобные обозначения были реализованы для встроенных типов; таким образом e1:: (e2:: …. :: nil) сокращенно [e1, e2 ...], ['a', 'b', …] и "ab...", и наборы записаны {e1, e2 ... }. Обратите внимание на то, что мы пишем cons как инфикс ::.

Есть две эквивалентные формы условного выражения:

 ; Вариант 1

e1 if c else e2

 ; Вариант 2

c  then e1 else e2

Во многих языках пишется так: if c then e1 else e2

Локальные переменные могут быть объявлены и связаны со значениями при использование любой из эквивалентных форм:

e1 where p == e2 

 ; или

let p == e2 in e1

где p – это выражение, сформированное путём применения конструктора данных по отношению ко многим отличным переменным (это называют шаблон (паттерн)). Например:

a+b where a:: (b:: l) == f (t)

После оценки f (t), скорее всего приведет к значению, которое 'соответствует' образцу a:: (b:: l). Тогда соответствующие субтермы в значении f (t) связаны с a, b, и 1 при оценке a+b.

Определение функций

Прежде чем функция будет определена, должен быть объявлен ее тип. Например:

dec reverse : list (alpha) -> list (alpha)

Язык hope – это язык с очень строгим контролем типов, и система языка включает полиморфный typechecker, который в состоянии обнаружить все ошибки типа во время компиляции. Функциональные символы могут быть перегружены. Когда это сделано, typechecker в состоянии определить, какое функциональное определение принадлежит конкретному функциональному символу.

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

--- reverse (nil ) <= nil 				       //   (1)
--- reverse (a : : l) <= reverse (l ) <> [a]   // 	(2)

символ <> является добавленным инфиксом. Это определяет (верхнего уровня) реверс списка; например:

reverse (1 : : (2 : : nil ) ) = reverse (2 : : nil ) <> [1]
                           = (reverse (nil ) <> [2] ) <> [1]
                           = (nil <> [2] ) <> [1]

Так reverse [1, 2] = [2,1] (с помощью двух приложений уравнения 2 сопровождаемое одним приложением уравнения 1). Образцы левой стороны обычно будут непересекающимися и будут связываться со структурой определения типа:

 data list alpha == nil ++ alpha :: list alpha

Система уравнений, определяющая функцию, должна исчерпать возможности, предоставленных оператором data, который вводит типы параметра.

Например, определение Чисел Фибоначчи:

dec fib : hum -> num
--- fib (0 ) <= 1
--- fib (succ (0 ) ) <= 1
--- fib (succ (succ (n ) ) ) <= fib (succ (n ) ) + fib (n )

В этом случае эти три модели 0, succ (0) и succ (succ (n)) исчерпывают набор значений, принадлежащих num. Модель 1 может быть использована в качестве сокращения для succ (0).

Нульарные 'функции' также могут быть определены; например:

dec pi : rational
--- pi <= mkrational (22,7)

предполагается, что тип rational был определен.

Лямбда-выражения определяются таким же образов. Например, для того чтобы функции вычислить соединение двух значений истинности ( уже доступный как функция and):

lambda true, p => p
I false, p => false

Другой пример лямбда-выражения можно наблюдать при определении функционального композиции:

typevar alpha,beta,tau
dec compose : (alpha->beta)#(beta -> tau ) 
-> (alpha ->  tau ) 
--- compose  (f, g) <= lambda x => f (g (x ) )

Модули

Любая последовательность операторов может быть превращена в модуль, путем окружения его операторами:

module name
    and
end

Типы данных, объявленные в модуле, могут обращаться к функциям вне модуля, только если оператор pubtype tname содержится в модуле.

Точно так же константы (включая конструкторы данных) могут ссылаться только если содержится оператор pubconst cname.

В модуле нельзя ссылаться на что-либо объявленное вне самого модуля, если модуль не содержит оператор uses mname.

В этом случае все типы и константы, объявленные как общедоступные к обозначенному модулю, доступны. Кроме того, определенные глобальные типы и константы (num, truval, char, list и set вместе с некоторыми примитивными операциями), могут быть использованы в любом модуле.

Это эффективный инструмент для инкапсуляции абстракции данных; если примитивные конструкторы и низкоуровневые операции объявления данных не объявлены общедоступными, то реализация абстракции скрыта от остальной части программы.

Отложенные вычисления ввод/вывод

Отложенные вычисления были упомянуты выше; там мы описывали их как одну из концепций языка. До сих пор в языке Hope отложенные вычисления были реализованы только для списков, которые делают доступным большую часть силы механизма. Отложные списки создаются при помощи специальных знаков конструктора вместо обычного : :. Этот конструктор создает список, который идентичен нормальному списку (в частности a: : l будет соответствовать lcons (c, d) ) за исключением того, что параметры lcons остаются необъявленными до тех пор пока их значения не потребуются во время использования списка.

Рассмотрим функцию, которая производит (потенциально) бесконечный список, состоящий из числа и всех его наследников:

dec allsuccs :num -> list num
--- allsuccs (n ) <= lcons (n, allsuccs (n+1 ) )

Теперь, если мы определяем 'отложенную mapcar' функцию:

Typevar alpha, beta 
dec <*> : ( alpha-> beta)#list alpha -> list beta
 infix <*> : 6 

--- f <*> nil <= nil
--- f <*> (a::al) <= lcons (f (a ), (f <*> al ) )

тогда бесконечный список квадратов всех чисел всего лишь:

square <*> allsuccs (0)

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

data device == tty ++ file(list(char)) ++ ...

Специальный символ (control/Z) сигнализирует конец ввода, и следовательно конец отложенного списка. Вывод - функция типа device->( list (alpha)->void) . Задавая список, output (dev) оценивает каждый элемент и производит его, как выведено на обозначенном устройстве.

Например, вот программа, считывающая число из терминала, после выводящая его квадрат, и затем повторяющая (пока control/Z не введен):

output ("tty") (square <*> input("tty"))

Так как input ("tty") в этом выражении имеет тип list (num), то телетайп примет как ввод только выражения типа num.

Это - специальный пример общей проблемы связи наследников процессов. Отложенные списки обеспечивают средство реализации каналов передачи, но в настоящее время нотация языка hope может определить произвольную сеть коммуникационных процессов. Мы не сильно задумывались об этой проблеме; однако, нотации существуют и они достаточно подробны и могли бы быть адаптированы в наших целях.

Примечания по реализации

Система языка hope состоит из компилятора (начиная от программ hope до кодировки для абстрактной стековой машины) и имплементации целевой машины. Система написана в POP 2, и в настоящее время работает приблизительно с 55K словами (плюс 15K общий сегмент) на DEC KI-IO. Скомпилированный код должен быть достаточно переносимым, поскольку абстрактное средство моделирования машины может легко быть записано для новой машины. Сам компилятор менее переносим, так как он требует доступности POP-2.

Предварительные испытания показали, что программа, написанная на hope, работает приблизительно в 9 раз медленнее, чем тот же алгоритм, кодированный в LISP, работающий под интерпретатором Rutgers/UCI (и в 23 раза медленнее, чем компилирует LISP). Большая программа, выполненная недавно, работала медленнее по-видимому из-за перегрузки страницы. Реализация машинного кода интерпретатора должна работать намного быстрее.

Примеры

Пример полной программы на языке hope продемонстрирован далее. Это иллюстрирует, как мы можем использовать данный язык для того чтобы реализовать типы данных (упорядоченные деревья), и затем как этот тип может быть использован в программе для treesort (сортировки деревьев).

Упорядоченные деревья

В первом модуле содержится реализация упорядоченного дерева абстрактного типа чисел (в программе тип данных otree). Otree задан для того чтобы быть либо пустым, либо tip (содержащий число), либо node, т.е. содержащим два otrees и число. Специальное свойство otree – это то, что для любого node (t1, n, t2), все числа, содержавшиеся в t1 будут меньше, чем n, который в свою очередь меньше или равен всем числам, содержавшимся в t2.

Мы определяем три общедоступные константы:

  • Empty – пустой otree
  • Insert – добавляет число к otree, сохраняя порядок otree
  • Flatten – беспорядочное пересечение otree

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

Обратите внимание на то, что конструктора данных node не общедоступен. Следовательно, единственные функции, доступные 'внешнему миру' для построения и изменения otrees будут empty и insert. Обе сохраняют свойства otrees, таким образом, что гарантируется целостность выполнения. Однако insert это не конструктор данных, и следовательно не может использоваться в шаблонах.

Пример полной программы:

Module ordered_trees
   pubtype otree
   pubconst empty, insert, flatten 

   date otree == empty ++ tip(num)
             ++ node(otree#num#otree) 

   dec insert : num#otree -> otree 
   dec flatten : otree -> list num 

   --- insert(n,empty) <= tip(n)
   --- insert(n,tip(m)) 
             <= n<m then node(tip(n),m,empty)
                  else node(empty,m,tip(n)) 
   --- insert(n,node(tl,m,t2))
             <= n<m then node(insert(n,tl),m,t2) 
                  else node(tl,m,insert(n,t2)) 
   --- flatten(empty) <= nil 
   --- flatten(tip(n)) <= [n] 
   --- flatten(node(tl,n,t2)) 
                    <= flatten(tl) <> (n::flatten(t2)) 

end 

module list_iterators 
   pubconst*, **

   typevar alpha, beta 

   dec * : (alpha->beta)#list alpha -> list beta
   dec ** : (alpha#beta->beta)#(list alpha#beta) 
                     -> beta 

   infix *,  ** : 6

   --- f * nil <= nil
	--- f * (a::al) <= (f a)::(f * al) 
   --- g ** (nil,b) <= b
--- g ** (a::al,b) <= g ** (al,g(a,b)) 

end 

module tree_sort 
   pubconst sort 
   uses ordered_trees, list_iterators
dec sort : list num -> list num
--- sort(l) <= flatten(insert ** (l,empty)) 
end

Список итераторов

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

Первая функция * идентична mapсar в LISP. Она создает список, содержащий результаты применения функции к каждому элементу данного списка. Это фактически не используется в примере.

Функция ** немного сложнее. Когда к ней добавляешь функцию g типа alpha#beta -> beta, список из alph, и 'начальный' beta объект, она применяет g к каждому элементу списка, начинаясь с данного beta объекта как со второго параметра и впоследствии перерабатывая результат предыдущего приложения. Это функция аналогична операции оператора 'сокращения' (англ. ‘reduction’ operator) APL; пример использования можно рассмотреть при вычислении объединения списка множества элементов:

union ** (setlist,emptyset)

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

Сортировка дерева

Функция сортировки списка чисел теперь определена используя примитивы, разработанные в предыдущих модулях. Операция ** из list_iterators используется, чтобы последовательно расставить элементы списка в первоначально пустой otree. После результат выравнен, для того чтобы произвести окончательный ответ.

Выводы

Так как язык hope был разработан принимая во внимание перечисленное, не удивительно, что он включает в себя их всех, несмотря на то, что некоторые продемонстрированы лучше, чем другие. Но более важным является вопрос того, предоставляет ли получившийся язык лучший интерфейс для компьютера, чем тот, который представлен существующими языками.

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

Важная цель создания языка состоит в том, чтобы легко понять справляется ли программа с заданной спецификацией. В этом отношении аппликативные языки, такие как hope, кажется, предлагают значительные преимущества; отсутствие операторов присваивания и последовательная замена итерации рекурсией облегчают программам анализ формы. Мощные системы проверки для аппликативных языков были записаны Бойером и Муром (Boyer and Moore) и Обеном (Aubin).

Другое преимущество аппликативного языка заключается в том, что программы легко поддаются методу модернизации программы, посредством чего простая, но неэффективная программа преобразована в достаточно эффективную шагами, которые проверяют её правильность. Очень простым примером преобразования программы было бы производство следующей линейно-разовой программы для генерации Чисел Фибоначчи, которая требует экспоненциального времени.

dec g :num -> num#nnm
--- g(O) <= 1,1
--- g(succ(n)) <= (a + b),a 	where a, b = = g (n)

dec fib' : hum -> num 
--- fib'(O) <= 1
--- fib'(1) <= 1
--- fib'(succ(succ(n))) 
        <=a+b 	where a, b = = g (n)

Кроме того, есть другое (ранее не упомянутое) преимущество аппликативных языков, которое может стать нашим спасением: аппликативные языки так плотно не связаны с понятием последовательной машины, как императивные языки. Значение функционального приложения e0 (e1...., en) не зависит от порядка оценки выражений e0, … , en (если параметры переданы 'значением'); это гарантируется отсутствием оператора присваивания. Если же доступна параллельная машина e0, … , en может быть оценено одновременно.

Язык hope имеет свои минусы; один из них проиллюстрирован на примере рассмотренной программы. Программа сортировки сортирует только список чисел, потому что otree - это '"упорядоченное дерево чисел". Мы хотим более общую программу сортировки, и это зависит от более общего определения упорядоченных деревьев; мы хотели бы определить 'упорядоченное - дерево alph. Объявление данных просто обобщить. Но для того чтобы объединить insert в тип:

alpha#otree(alpha)->otree(alpha)

должно быть более общее отношение порядка чем <, который задан только для чисел.

Одно решение этой проблемы состояло бы в том, чтобы потребовать пользователей otree, чтобы они придерживались определенного порядка отношений особенно при работе с otree. Это могло быть добавлено как дополнительный параметр к insert, или альтернативно это могло быть встроено в otrees (предоставленный как параметр к empty и распространенный к новым tips и nods с помощью insert). К сожалению, 'плохой' порядок отношений (например, тот, который не является переходным) нарушил бы целостность типа данных и вызвал бы непредсказуемый результаты.

Другая возможность состояла бы в том, чтобы определить общее отношение порядка как новый примитивный язык hope. Это было нашим решением при аналогичной проблеме с включением равенства =. Два значения данных равны, если у них есть одинаковые представления как условия конструкторов, за исключением того, что для недавно определенного типа данных пользователь может обеспечить нестандартное равенство, которое автоматически включено в стандартное системное равенство. Например, определим равенство для otrees так, чтобы tip (n) = node (empty, n, empty). Лучшим решением существующей трудности было бы разрешить чтобы порядок был связан с каждым типом, но как долго такие операции должны быть связаны с типом?

Лучшее решение состоит в том, чтобы, конечно, связать набор операций с каждым типом данных (таким образом, типы становятся алгебраическими вместо простых наборов). Вместо того, чтобы сводить к otree (alpha), мы могли сводить все к otree (alpha [<]), требуетя, чтобы отношение порядка существовало в типе параметра. Это метод, использованный в CLU и в языке спецификации CLEAR. Мы действительно хотим, чтобы у модулей языка hope были параметры, набор типов и операторов, ведь у кластеров CLU есть параметры.

Далее снова обратимся к рассмотренной программе и обратим внимание на то, что модуль tree_sort не зависит от того, что otrees это деревья, но только от определенных свойств insert и flatten. Мы можем заменить модуль ordered_lists на ordered_trees, где empty становится nil, а insert очевидной сохраняющей порядок вставкой в упорядоченном списке, и flatten это тождественное отображение. Tree_sort это параметрический модуль, который может быть 'применен' к любому модулю, удовлетворяющему определенным (нетривиальным) свойствам.

Параметр кластера CLU, являются явным списком типов и операторов:

T with < : T#T -> truval

В CLEAR такой объект (назван теорией и сопровождается аксиомами) можно быть назван 'Упорядоченное множество'; более того для создания таких теорий используется огромное количеством различных операций. Мы хотели бы расширить язык hope, что бы он включал в себя параметризованные модули, где параметры и интерфейсы между модулями nameable и manipulable как в CLEAR.

Ссылки

Список литературы

  • Aubin, R. Strategies for Mechanizing Structural Induction. Proc. 5th Int. Joint Conf. on Artificial Intelligence, Cambridge, Massachusetts, August, 1977, pp. 363-369.
  • John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978
  • Boyer, R.S. and Moore, J.S. A Computational Logic. Academic Press, 1980
  • Burge, W.H. Recursive Programming Techniques. Addison-Wesley, 1975.
  • Burstall, R.M. Design Considerations for a Functional Programming Language. Infotech State of the Art Conference: The Software Revolution, Copenhagen, October, 1977.
  • Rod M. Burstall, Electronic Category Theory, Proceedings of the 9th Symposium on Mathematical Foundations of Computer Science, p.22-39, September 01-05, 1980
  • R. M. Burstall , John Darlington, A Transformation System for Developing Recursive Programs, Journal of the ACM (JACM), v.24 n.1, p.44-67, Jan. 1977
  • Burstall, R.M. and Goguen, J.A. Putting Theories Together to Make Specifications. Proc. 5th Int. Joint Conf. on Artificial Intelligence, Cambridge, Massachusetts, August, 1977, pp. 1045-1058.
  • Burstall, R.M. and Sannella, D.T. HOPE User's Manual. In preparation.
  • O. J. Dahl , E. W. Dijkstra , C. A. R. Hoare, Structured programming, Academic Press Ltd., London, UK, 1972
  • Dahl, O-J., Myhrhaug, B. and Nygaard, K. The SIMULA 67 Common Base Language. Publication S22, Norwegian Computing Centre, Oslo, 1970.
  • Robert B. K. Dewar , Arthur Grand , Ssu-Cheng Liu , Jacob T. Schwartz , Edmond Schonberg, Programming by Refinement, as Exemplified by the SETL Representation Sublanguage, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.1, p.27-49, July 1979
  • Feather, M.S. A System for Developing Programs by Transformation. Ph.D. Th., University of Edinburgh, 1979.
  • Goguen, J.A. and Burstall, R.M. CAT, a System for the Structured Elaboration of Correct Programs from Structured Specifications. In preparation.
  • Goguen, J.A. and Tardo, J.J. An Introduction to OBJ: A Language for Writing and Testing Formal Algebraic Program Specifications. Specifications of Reliable Software Conf. Proc., Cambridge, Massachusetts, April, 1979.
  • Michael J. C. Gordon, The Denotational Description of Programming Languages: An Introduction, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
  • M. Gordon , R. Milner , L. Morris , M. Newey , C. Wadsworth, A Metalanguage for interactive proof in LCF, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.119-130, January 23-25, 1978, Tucson, Arizona
  • Peter Henderson , James H. Morris, Jr., A lazy evaluator, Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages, p.95-103, January 19-21, 1976, Atlanta, Georgia
  • Henderson, P. and Snowdon, R. An Experiment in Structured Programming. BIT 12, 1 (1972), 38-53
  • J. D. Ichbiah, Preliminary Ada reference manual, ACM SIGPLAN Notices, v.14 n.6a, p.1-145, June 1979
  • Kenneth E. Iverson, A programming language, John Wiley & Sons, Inc., New York, NY, 1962
  • R. D. Jenks, The SCRATCHPAD language, Proceedings of the ACM SIGPLAN symposium on Very high level languages, p.101-111, March 28-29, 1974, Santa Monica, California, USA
  • Brian W. Kernighan , P. L. Plauger, Software Tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1976
  • P. J. Landin, The next 700 programming languages, Communications of the ACM, v.9 n.3, p.157-166, March 1966
  • Barbara Liskov , Alan Snyder , Russell Atkinson , Craig Schaffert, Abstraction mechanisms in CLU, Communications of the ACM, v.20 n.8, p.564-576, Aug. 1977
  • George Milne , Robin Milner, Concurrent Processes and Their Syntax, Journal of the ACM (JACM), v.26 n.2, p.302-321, April 1979
  • Milner, R. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences 17, 3 (December 1978), 348-375.
  • Turner, D.A. SASL Language Manual. University of St. Andrews, 1979.
  • Wadsworth, C.P. Semantics and Pragmatics of the Lambda Calculus. Ph.D. Th., Programming Research Unit, Oxford University, 1971.
  • David H D Warren , Luis M. Pereira , Fernando Pereira, Prolog - the language and its implementation compared with Lisp, Proceedings of the 1977 symposium on Artificial intelligence and programming languages, p.109-115, August 15-17, 1977
  • Wulf, W.A., London, R.L. and Shaw, M. An Introduction to the Construction and Verification of Alphard Programs. IEEE Trans. on Software Eng. SE-2, 4 (December 1976), 253-265.