Nr 01 · Słownik · Teoria informatyki · Języki i teoria typów

Teoria typow

24 pojęć w 13 podgrupach, z prostymi definicjami i źródłami.

Abstrakcja danych · 1

  • 01typ egzystencjalnyTyp kwantyfikowany egzystencjalnie, ukrywający konkretną reprezentację wewnętrzną i służący jako podstawa abstrakcji danych.

Abstrakcje przeciazania · 1

  • 01klasa typówMechanizm grupujący typy spełniające wspólny zbiór operacji, umożliwiający przeciążanie zorganizowane i polimorfizm ograniczony.

Dyscypliny typowania · 2

  • 01typowanie dynamiczneWłasność języka, w której typy wartości są sprawdzane w trakcie wykonania, a nie statycznie podczas kompilacji.
  • 02typowanie statyczneWłasność języka, w której typy wyrażeń są ustalane i sprawdzane w czasie kompilacji, przed wykonaniem programu.

Hierarchia klasyfikacji · 1

  • 01rodzajTyp typów: klasyfikacja konstruktorów typów określająca ich aplikowalność, analogiczna do typów dla wartości.

Konstruktory typow · 4

  • 01typ algebraicznyADTTyp złożony konstruowany z innych typów za pomocą sumy (wariantów) i produktu (krotek), zwykle z dopasowaniem wzorca.
  • 02typ funkcyjnyTyp opisujący odwzorowanie z typu dziedziny w typ przeciwdziedziny, przypisywany funkcjom i wyrażeniom funkcyjnym.
  • 03typ iloczynuTyp złożony reprezentujący jednoczesne zestawienie wartości kilku typów składowych, jak krotka lub rekord.
  • 04typ sumytyp wariantowyTyp złożony reprezentujący wartość będącą jednym z kilku rozłącznych wariantów, z których każdy może nieść własne dane.

Podstawy systemow typow · 2

  • 01system typówFormalny system reguł przypisujących typy wyrażeniom programu w celu ograniczenia dopuszczalnych operacji i wykluczenia pewnych klas błędów.
  • 02typZbiór wartości wraz z dopuszczalnymi operacjami, przypisywany wyrażeniom jako klasyfikacja syntaktyczna ich znaczenia.

Podtypowanie · 2

  • 01podtypowanieRelacja między typami, w której wartość typu podrzędnego może być bezpiecznie użyta wszędzie tam, gdzie oczekiwany jest typ nadrzędny.
  • 02zasada podstawialnościLSPKryterium, w myśl którego obiekt typu podrzędnego musi zachowywać kontrakt typu nadrzędnego, by relacja podtypowania była poprawna.

Polimorfizm · 4

  • 01polimorfizmZdolność kodu lub funkcji do działania jednolicie na wartościach wielu różnych typów.
  • 02polimorfizm ad hocSposób, w którym funkcja zachowuje się różnie zależnie od typu argumentu, realizowany np. przez przeciążanie lub klasy typów.
  • 03polimorfizm parametrycznySposób, w którym funkcja działa jednolicie dla dowolnego typu parametryzującego, niezależnie od jego konkretnej postaci.
  • 04typ uniwersalnyTyp kwantyfikowany uniwersalnie po zmiennej typowej, opisujący wartości działające jednolicie dla każdego podstawienia tej zmiennej.

Rachunki typowane · 1

  • 01rachunek lambda z typamiSTLCFormalny rachunek funkcji z systemem typów ograniczającym poprawne wyrażenia, stanowiący rdzeń teorii typów języków programowania.

Typy a logika · 1

  • 01izomorfizm Curry'ego-Howardapropositions as typesOdpowiedniość między typami a zdaniami logicznymi oraz między programami a dowodami, łącząca teorię typów z logiką konstruktywną.

Typy zaawansowane · 1

  • 01typ zależnyTyp, którego definicja zależy od wartości, co pozwala wyrażać precyzyjne specyfikacje i dowody w systemie typów.

Weryfikacja typow · 1

  • 01wnioskowanie typówinferencja typówAutomatyczne wyprowadzanie typów wyrażeń bez jawnych adnotacji, na podstawie ich użycia i ograniczeń wynikających z reguł typowania.

Wlasnosci systemow typow · 3

  • 01bezpieczeństwo typówWłasność, w której poprawnie otypowany program nie może wywołać błędów polegających na zastosowaniu operacji do wartości niewłaściwego typu.
  • 02postępWłasność, w której poprawnie otypowane wyrażenie jest wartością albo może wykonać kolejny krok obliczenia, więc nie utyka w stanie błędu.
  • 03zachowanie typuredukcja podmiotuWłasność relacji ewaluacji: jeśli wyrażenie ma dany typ i wykonuje krok obliczenia, wynik zachowuje ten sam typ.

Pozostałe grupy — Języki i teoria typów

Grupa pojęć · Języki i teoria typów24 haseł