Teoria typow

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

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

Własność języka, w której typy wartości są sprawdzane w trakcie wykonania, a nie statycznie podczas kompilacji.

Własność języka, w której typy wyrażeń są ustalane i sprawdzane w czasie kompilacji, przed wykonaniem programu.

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

Typ złożony konstruowany z innych typów za pomocą sumy (wariantów) i produktu (krotek), zwykle z dopasowaniem wzorca.

Typ opisujący odwzorowanie z typu dziedziny w typ przeciwdziedziny, przypisywany funkcjom i wyrażeniom funkcyjnym.

Typ złożony reprezentujący jednoczesne zestawienie wartości kilku typów składowych, jak krotka lub rekord.

Typ 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.

Formalny system reguł przypisujących typy wyrażeniom programu w celu ograniczenia dopuszczalnych operacji i wykluczenia pewnych klas błędów.

Zbiór wartości wraz z dopuszczalnymi operacjami, przypisywany wyrażeniom jako klasyfikacja syntaktyczna ich znaczenia.

Relacja 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.

Kryterium, w myśl którego obiekt typu podrzędnego musi zachowywać kontrakt typu nadrzędnego, by relacja podtypowania była poprawna.

Zdolność kodu lub funkcji do działania jednolicie na wartościach wielu różnych typów.

Sposób, w którym funkcja zachowuje się różnie zależnie od typu argumentu, realizowany np. przez przeciążanie lub klasy typów.

Sposób, w którym funkcja działa jednolicie dla dowolnego typu parametryzującego, niezależnie od jego konkretnej postaci.

Typ kwantyfikowany uniwersalnie po zmiennej typowej, opisujący wartości działające jednolicie dla każdego podstawienia tej zmiennej.

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

Odpowiedniość między typami a zdaniami logicznymi oraz między programami a dowodami, łącząca teorię typów z logiką konstruktywną.

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

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

Wł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.

Wł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.

Własność relacji ewaluacji: jeśli wyrażenie ma dany typ i wykonuje krok obliczenia, wynik zachowuje ten sam typ.