Түр полиморфизмінің бір түрі: Төмендету (Subtyping)

Кіріспе

Тип полиморфизмінің формасы

Программалау тілі теориясында, субтипизация (сондай-ақ субтип полиморфизмі немесе инклюзия полиморфизмі деп аталады) тип полиморфизмінің бір түрі болып табылады. Субтип – басқа дерек типімен (супертиппен) қолданылу мүмкіндігі арқылы байланысты дерек типі, яғни супертиптің элементтерімен жұмыс істеуге арналған бағдарлама элементтері (әдетте, кіші программалар немесе функциялар) сонымен қатар субтиптің элементтерімен де жұмыс істей алады. Егер S, T-нің кіші типі болса, субтипизация қатынасы (1=S <: T, 1=S ⊑ T, немесе 1=S ≤: T) S типіндегі кез келген өрнекті T типіндегі өрнек күтілетін кез келген контексте қауіпсіз түрде қолдануға болады дегенді білдіреді. Мұнда субтипизацияның нақты семантикасы «қауіпсіз қолдану» және «кез келген контекст» берілген типтік формализм немесе бағдарламалау тілімен қалай анықталатынына байланысты. Бағдарламалау тілінің типтік жүйесі негізінен өзінің субтипизация қатынасын анықтайды, бұл тілде конверсия механизмдері болмаса (немесе өте аз болса) тривиальды болуы мүмкін. Субтипизация қатынасының арқасында, өрнек бірнеше типке тиесілі болуы мүмкін. Сондықтан субтипизация типтік полиморфизмнің бір түрі болып табылады. Объектіге бағытталған бағдарламалауда «полиморфизм» термині көбінесе осы субтип полиморфизміне ғана қатысты қолданылады, ал параметрлік полиморфизмнің техникалары жалпы бағдарламалау деп есептеледі. Функционалдық бағдарламалау тілдері көбінесе жазбалардың субтипизациясына мүмкіндік береді. Осылайша, жазба типтерімен кеңейтілген қарапайым типті лямбда-есептеуі, субтипизацияның пайдалы түсінігін анықтау және зерттеуге болатын ең қарапайым теориялық орта болып табылады. Нәтижесінде алынған есептеу өрнектердің бірнеше типіне мүмкіндік беретіндіктен, ол енді «қарапайым» типтік теория емес. Функционалдық бағдарламалау тілдері, анықтамасы бойынша, функциялық литералдарды қолдайды, оларды жазбаларда сақтауға болады, сондықтан субтипизациясы бар жазба типтері объектіге бағытталған бағдарламалаудың кейбір мүмкіндіктерін қамтамасыз етеді. Әдетте функционалдық бағдарламалау тілдері параметрлік полиморфизмнің кейбір, көбінесе шектеулі формаларын ұсынады. Теориялық тұрғыда екі мүмкіндіктің өзара әрекеттесуін зерттеу қажет; ортақ теориялық орта F<: жүйесі болып табылады. Объектіге бағытталған бағдарламалаудың теориялық қасиеттерін қамтуға тырысатын әртүрлі есептеулер F<: жүйесінен туындауы мүмкін. Субтипизация тұжырымы лингвистикалық гипонимия және голонимия тұжырымдарымен байланысты. Бұл математикалық логикадағы шектелген квантификация тұжырымымен де байланысты (реттелген логиканы қараңыз). Субтипизацияны объектіге бағытталған тілдерден (сынып немесе объект) мұрагерлік тұжырымымен шатастырмау керек; субтипизация типтер арасындағы қатынас (объектіге бағытталған терминологияда интерфейстер), ал мұрагерлік – жаңа объектілерді қолданыстағылардан жасауға мүмкіндік беретін тілдік мүмкіндіктен туындайтын іске асырулар арасындағы қатынас. Көптеген объектіге бағытталған тілдерде субтипизация интерфейс мұрагерлігі деп аталады, ал мұрагерлік – іске асыру мұрагерлігі деп аталады.

In programming language theory, subtyping (also called subtype polymorphism or inclusion polymorphism) is a form of type polymorphism. A subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, meaning that program elements (typically subroutines or functions), written to operate on elements of the supertype, can also operate on elements of the subtype. If S is a subtype of T, the subtyping relation (written as 1=S <: T, 1=S ⊑ T, or 1=S ≤: T ) means that any term of type S can safely be used in any context where a term of type T is expected. The precise semantics of subtyping here crucially depends on the particulars of how "safely be used" and "any context" are defined by a given type formalism or programming language. The type system of a programming language essentially defines its own subtyping relation, which may well be trivial, should the language support no (or very little) conversion mechanisms. Due to the subtyping relation, a term may belong to more than one type. Subtyping is therefore a form of type polymorphism. In object oriented programming the term 'polymorphism' is commonly used to refer solely to this subtype polymorphism, while the techniques of parametric polymorphism would be considered generic programming. Functional programming languages often allow the subtyping of records. Consequently, simply typed lambda calculus extended with record types is perhaps the simplest theoretical setting in which a useful notion of subtyping may be defined and studied. Because the resulting calculus allows terms to have more than one type, it is no longer a "simple" type theory. Since functional programming languages, by definition, support function literals, which can also be stored in records, records types with subtyping provide some of the features of object oriented programming. Typically, functional programming languages also provide some, usually restricted, form of parametric polymorphism. In a theoretical setting, it is desirable to study the interaction of the two features; a common theoretical setting is system F<:. Various calculi that attempt to capture the theoretical properties of object oriented programming may be derived from system F<:. The concept of subtyping is related to the linguistic notions of hyponymy and holonymy. It is also related to the concept of bounded quantification in mathematical logic (see Order sorted logic). Subtyping should not be confused with the notion of (class or object) inheritance from object oriented languages; subtyping is a relation between types (interfaces in object oriented parlance) whereas inheritance is a relation between implementations stemming from a language feature that allows new objects to be created from existing ones. In a number of object oriented languages, subtyping is called interface inheritance, with inheritance referred to as implementation inheritance.

Шығу тегі

Бағдарламалау тілдеріндегі субтипілеу түсінігі 1960 жылдарға дейін жетеді; ол Simula туындыларында енгізілді. Субтипілеудің алғашқы формалды сипаттамаларын 1980 жылы Джон К. Рейнольдс жасады, ол категория теориясын пайдаланып, жасырын түрлендірулерді формалдады, сондай-ақ 1985 жылы Лука Карделли де осы мәселеге үлес қосты. Субтипілеу концепциясы объектіге бағытталған бағдарламалау кеңінен қолданыс тапқан сайын, көріне бастады (кейбір аймақтарда полиморфизммен мағынасы жақын деп есептеледі). Осы контексте, қауіпсіз алмастыру принципі көбінесе Барбара Лисковтың есімімен аталады, ол 1987 жылы объектіге бағытталған бағдарламалау бойынша конференциядағы негізгі баяндамасында оны танымал етті. Лисков пен Жаннетт Уинг анықтаған, өзгертілетін нысандарды ескеретін субтипілеудің идеалды түсінігі, мінез-құлықты субтипілеу деп аталады, және ол типтік тексеру құралында іске асырылатын нәрседен әлдеқайда күшті. (Толық мәліметтер төменде келтірілген.)

Ішкі типтеу жүйелері

Типтік теоретиктер номиналды кіші типтеуді және құрылымдық кіші типтеуді ажыратады. Номиналды кіші типтеуде тек белгілі бір тәсілмен жарияланған типтер ғана бір-бірінің кіші типі бола алады, ал құрылымдық кіші типтеуде екі типтің құрылымы біреуінің екіншісінің кіші типі болатынын анықтайды. Жоғарыда сипатталған кластық объектіге бағытталған кіші типтеу номиналды болып табылады; объектіге бағытталған тіл үшін құрылымдық кіші типтеу ережесі мынадай болуы мүмкін: егер A типіндегі объектілер B типіндегі объектілерге жіберілген барлық хабарламаларды қабылдай алса (яғни, егер олар бірдей әдістерді анықтаса), онда A, B-нің кіші типі болады, олардың бірінің екіншісінен мұрагерлік алған-алмауына қарамастан. Бұл «duck typing» деп аталады және динамикалық типтегі объектіге бағытталған тілдерде кең таралған. Объекті типтерінен басқа типтер үшін де дұрыс құрылымдық кіші типтеу ережелері белгілі. Кіші типтеуді қолдайтын бағдарламалау тілдерінің іске асырылуы екі негізгі санатқа бөлінеді: қосатын іске асыру, онда A типіндегі кез келген мәннің өрнегі, егер A <: B болса, B типіндегі сол мәнді де білдіреді, және мәжбүрлі іске асыру, онда A типіндегі мән B типіне автоматты түрде түрлендіріледі. Объектіге бағытталған тілдегі субклассификация арқылы туындаған кіші типтеу әдетте қосатын болады; бүтін сандар мен қозғалатын нүктелі сандарды байланыстыратын кіші типтеу қатынастары, олар әртүрлі өрнектеледі, әдетте мәжбүрлі болады. Кіші типтеу қатынасын анықтайтын барлық типтік жүйелерде ол рефлексивті (яғни, кез келген A типі үшін A <: A) және транзитивті (яғни, егер A <: B және B <: C болса, онда A <: C) болады. Бұл оны типтерге қатысты преордер етеді.

Кеңіш пен тереңдіктің субтипі

Жазбалардың түрлері ені мен тереңдігіне қатысты кіші типтеу ұғымдарын тудырады. Бұл бастапқы жазба түріндегідей операцияларды орындайтын жаңа жазба түрін алудың екі әртүрлі жолын көрсетеді. Еске сала кетейік, жазба – (аталған) өрістердің жиынтығы. Кіші тип – бастапқы типте рұқсат етілген барлық операцияларды орындайтын тип болғандықтан, жазбаның кіші типі бастапқы типтегідей өрістердегі операцияларды қолдауы керек. Мұндай қолдауға қол жеткізудің бір жолы – ендік кіші типтеу деп аталады, ол жазбаға қосымша өрістерді қосады. Формальды түрде айтқанда, ендік жоғары типте кездесетін әрбір (аталған) өріс ендік кіші типте де кездеседі. Осылайша, жоғары типте орындалатын кез келген операция кіші типте де қолдауға ие болады. Екінші әдіс – тереңдік кіші типтеу, ол әртүрлі өрістерді олардың кіші типтерімен алмастырады. Яғни, кіші типтің өрістері жоғары типтің өрістерінің кіші типтері болып табылады. Жоғары типтегі өріс үшін қолдауға ие болған кез келген операция оның кіші типі үшін де қолдауға ие болғандықтан, жазбаның жоғары типіне орындалатын кез келген операция жазбаның кіші типімен де орындалады. Тереңдік кіші типтеу тек өзгермейтін жазбалар үшін ғана мағыналы: мысалы, сіз нақты нүктенің 'x' өрісіне 1.5 санын тағайындай аласыз (екі нақты өрісі бар жазба), бірақ бүтін сан нүктесінің 'x' өрісіне сол сияқты тағайындауға болмайды (бірақ ол нақты нүкте типінің терең кіші типі болып табылады), себебі 1.5 – бүтін сан емес (Variance қараңыз). Жазбалардың кіші типтерін F<: жүйесінде анықтауға болады, ол параметрлік полиморфизмді жазба типтерінің кіші типтеуімен біріктіреді және екі мүмкіндікті де қолдайтын көптеген функционалдық бағдарламалау тілдерінің теориялық негізі болып табылады. Кейбір жүйелер таңбаланған ажыратылған біріктірілген типтердің (мысалы, алгебралық дерек типтерінің) кіші типтеуін де қолдайды. Ендік кіші типтеу ережесі керісінше: ендік кіші типте кездесетін әрбір таңба ендік жоғары типте де кездесуі керек.

Функция түрлері

Егер 1=T1 → T2 функцияның түрі болса, онда оның субтипі 1=S1 → S2 функциясының кез келген түрі болып табылады, егер 1=T1 <: S1 және 1=S2 <: T2 шарттары орындалса. Мұны келесі типтеу ережесі арқылы қорытындылауға болады: 1=S1 → S2 параметрінің түрі контрвариантты деп аталады, өйткені оның субтиптеу қатынасы кері, ал қайтарылатын түрі ковариантты. Бұл кері айналу формальды түрде мына себептен болады: нақтыланған тип қабылдайтын типтерге қатысты "көбірек мүмкіндік береді", ал қайтаратын типке қатысты "көбірек шектеулі". Бұл Scala тілінде дәл осылай жұмыс істейді: n-арлық функция ішкі түрде trait-ты мұралаған класс болып табылады (Java сияқты тілдерде оны жалпы интерфейс ретінде қарастыруға болады), онда параметрлердің типтері және - оның қайтарылатын түрі; типтің алдындағы "−" таңбасы тип контрвариантты екенін, ал "+" таңбасы ковариантты екенін білдіреді. Көптеген объектіге бағытталған тілдер сияқты, жанама әсерлерге рұқсат беретін тілдерде, бір функцияны екіншісінің контекстінде қауіпсіз пайдалануға кепілдік беру үшін субтиптеу ғана жеткіліксіз. Лисковтың осы саладағы жұмысы мінез-құлықты субтиптеуге бағытталған, ол типтік жүйе қауіпсіздігінен басқа, субтиптердің супертиптер кепілдік берген барлық инварианттарды сақтайтынын талап етеді. Бұл субтиптеудің анықтамасы көбінесе шешілмейді, сондықтан оны типті тексерушімен тексеру мүмкін емес. Өзгертілетін сілтемелердің субтиптеуі параметрлер мен қайтарылатын мәндерді өңдеуге ұқсас. Жазуға ғана рұқсат етілген сілтемелер (немесе тұндырғыштар) параметрлер мәндері сияқты контрвариантты; оқуға ғана рұқсат етілген сілтемелер (немесе көздер) қайтарылатын мәндер сияқты ковариантты. Сонымен қатар, бастапқы және түпкілікті мәндер ретінде әрекет ететін өзгертілетін сілтемелер инвариантты болады.