О понимании типов, абстракций данных и полиморфизма (стр. 1 )

О понимании типов, абстракций данных и полиморфизма.
Автор: Luca Cardelli.
Резюме
Наша цель это рассмотреть понятие типов в языках программирования, представить модель типизированного, полиморфного языка программирования, который отражает недавние исследования в теории типов и проверить значимость последних исследований в конструировании практически применимого языка программирования.
Объектно-ориентированные языки предлагают и среду и средства для исследования взаимодействия между представлениями типов, абстракций и полиморфизма, так как они расширяют понятие типа до абстракции данных и так как наследование типов это важная форма полиморфизма. Мы разработаем систему типов, основанную на модели лямбда исчисления, котороя позволяет нам проще исследовать эти взаимодействия, свободных от сложностей продукционных языков программирования.
Рассматривается эволюция языков от безтиповых множеств до мономорфных и далее до полиморфных систем типов. Проверяются механизмы для полиморфизма такие как перегрузка, приведение типов, выделение подтипов ,параметризация. Разрабатывается объединенная среда для полиморфных систем типов в терминах типизированного лямбда исчисления, дополненного механизмом связывания типов через квантификацию.
Типовое лямбда-исчисление расширяется всеобщей квантификацией ( это кванторы всеобщности для любого x типа A в функции F(x) ) для моделирования шаблонных(generic) функций с параметрами-типами ( шаблонная функция определяет абстрактную операцию, указывая имя операции и список параметров, но не реализацию. Она шаблонная в том смысле, что она может принимать любые объекты в качестве аргументов. Но сама по себе шаблонная функция не может ничего делать. Если мы просто определим шаблонную функцию, то без разницы с какими параметрами мы её вызовем она будет выдавать ошибку. Чтобы шаблонная функция обрабатывала определенные аргументы мы должны определить одну или более реализаций шаблонной функции, называемых методами. Каждый метод представляет реализацию шаблонной функции для определенных классов аргументов);расширяется кванторами существования и пакетированием(сокрытие информации) для моделирования абстракных типов данных;расширяется кванторами ограничения для моделирования выделения подтипов и наследования типов. Итак мы получаем простое и точное описание мощной системы типов, котороая включает в себя абстрактные типы данных, параметрический полиморфизм и множественное наследование в единой непротиворечивой среде. Обсуждаются механизмы проверки типов для расширенного лямбда исчисления. Расширенное лямбда исчисление используется как язык программирования для различных пояснительных примеров. Мы будем называть этот язык Fun вместо лямбда (Fun ключевое слово для абстракции функций) так как это удобнее. Fun матиматически прост и может служить как основа для построения и реализвции реального языка программирования с системой типов, которая более мощная и выразительная чем существующие системы в других языках программирования. В частности этот язык может служить основой для построения строго типизированного объектно-ориентированного языка.