Знаймо

Додати знання

приховати рекламу

Цей текст може містити помилки.

Системи типізації



План:


Введення

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

Зазвичай при викладі питань, пов'язаних з поданням про тип, розглядаються не теорії типів взагалі, а одна досить спеціальна система, формалізує приписування типу. В її рамках типи будуються виключно з типових змінних і стрілок, а терми будуються виключно з лямбда-абстракцій і / або комбінаторних термів і аплікацій [1].


1. Поліморфна типізація

Розглянуте приписування типів поліморфно в тому сенсі, що у довільно взятого терма може бути більше одного типу, по суті нескінченна безліч типів. Разом з тим така система не містить \ Forall -Типів, будучи, таким чином, більш слабкою, ніж сильні поліморфні теорії, які в даний час використовуються в логіці і програмуванні. Ця система лежить в основі всіх інших систем типів, а її властивості відіграють самостійну роль, так що вона цілком заслуговує самостійного вивчення.


2. Базова роль техніки приписування типів

Оволодіння технікою приписування типів є прекрасною базовою підготовкою для вивчення підходів, характерних для теорії типів в цілому. Її методи та алгоритми нетривіальні, але їх основні ідеї стають зрозумілими, як тільки базові поняття виявляться осмисленими і освоєними в достатній мірі. Багато з ідей, які при формулюванні для сильних теорій типів виглядають досить громіздкими і складними, а також ряд прийомів аналізу різних структур, застосовуваних в цих теоріях, в системі приписування типів приймають вельми ясну і наочну форму.


3. Різновиди теорій типів

Теорії типів сходять до Б. Расселу (B. Russel). На початку 1900-х рр.. теорії типів будувалися для досить спеціальних цілей дозволу парадоксів, які в той час порушували побудова основ математики. З плином часу теорії типів знайшли більш широке застосування, ставши частиною обов'язкових логічних засобів, особливо в теорії доказів. Використання теорій типів в комбінаторної логікою сходить до роботи Х. Каррі 1934-го р. (H. Curry), а в \ Lambda-Вирахуванні - до роботи А. Черча 1940-го р. (A. Church). Однак аж до 1970-х рр.. теорії типів залишалися відносно вузько використовуваними тільки фахівцями


4. Мови програмування, що реалізують теорії типів

До того часу виникла потреба в мовах програмування з великими виразними можливостями, і теорії типів стали привертати увагу фахівців в області комп'ютерних наук. У 1970-х і 1980-х рр.. було розроблено декілька нових мов, заснованих на теорії типів. Ці мови добре себе зарекомендували при побудові різних додатків і стали відомими як в середовищі фахівців, так і поза цим середовищем. Основним серед цих мов став ML, розроблений в Единбурзькому університеті групою дослідників під керівництвом Робіна Мілнера. Крім нього з'явилися язики HOL (Кембриджський університет), Miranda (Research Software Ltd.) І Nuprl (Корнельський університет).


5. Розвиток систем типізації

У всіх цих мовах міститься компонента приписування типів, а ще не так давно приписування типів служило введенням до вивчення більш сильних систем типізації, як, наприклад, у роботі Х. Каррі і Р. Фейса 1958-го р. (H. Curry and R. Feys). Проте з часом система приписування типів перестала здаватися тривіальної, а стала розглядатися як цілком самостійна система, яка до того ж виявилася більш складною, ніж це очікувалося. Еволюції поглядів на систему приписування типів присвячена не одна робота. У цьому зв'язку можна вказати, наприклад роботу Д. Скотта (D. Scott). Як виявилося, на багато питань все ще немає завершених відповідей, а спроби їх пошуку приводять до цікавих прийомів і методів, які мають практичні застосування, наприклад, при побудові алгоритмів перевірки типів.

Насправді до теперішнього часу про приписуванні типів відомо набагато більше, ніж можна вмістити в одній статті. Ті розділи, які тут знайшли відображення, дозволяють тільки зрозуміти суть справи. Для подальшого читання можна порекомендувати, наприклад, роботу Р. Хиндлі (R. Hindley).


Примітки

  1. Hindley JR Basic simple type theory. - Cambridge University Press, 1995.

Література

  • Вольфенгаген В. Е. Методи і засоби обчислень з об'єктами. Апплікатівние обчислювальні системи. - М.: JurInfoR Ltd., АТ "Центр ЮрИнфоР", 2004. - Xvi +789 с ISBN 5-89158-100-0.
  • Hindley JR Basic simple type theory. - Cambridge University Press, 1995.

Цей текст може містити помилки.

Схожі роботи | скачати

Схожі роботи:
Бездіяльність системи
Відновлення системи
Ефективність системи
Мікроелектромеханічні системи
Колоїдні системи
Системи органів
Оборонні системи
Соціотехніческіе системи
Стійкість Сонячної системи
© Усі права захищені
написати до нас
Рейтинг@Mail.ru