Konstruktor typów
W dziedzinie logiki matematycznej i informatyki , znanej jako teoria typów , konstruktor typów jest cechą typowanego języka formalnego , który buduje nowe typy ze starych. Uważa się, że typy podstawowe są budowane przy użyciu konstruktorów typu zerowego . Niektóre konstruktory typów przyjmują inny typ jako argument, np. konstruktory typów produktów , typów funkcji , typów mocy i typów list . Nowe typy można definiować przez rekurencyjne tworzenie konstruktorów typów.
Na przykład rachunek lambda o prostym typie można postrzegać jako język z jednym konstruktorem typu innego niż podstawowy — konstruktorem typu funkcji. Typy produktów można ogólnie uznać za „wbudowane” we wpisane rachunki lambda poprzez curry .
Abstrakcyjnie rzecz ujmując, konstruktor typu jest n - argumentowym operatorem typu przyjmującym jako argument zero lub więcej typów i zwracającym inny typ. Wykorzystując curry, n -arnego można (prze)zapisać jako sekwencję zastosowań operatorów typu jednoargumentowego. Dlatego możemy postrzegać operatory typów jako po prostu wpisany rachunek lambda, który ma tylko jeden podstawowy typ, zwykle oznaczany wymawiany jako „typ”, który jest typem wszystkich typów w języku bazowym, nazywamy teraz typami właściwymi w celu odróżnienia ich od typów operatorów typu w ich własnym rachunku różniczkowym, które nazywane są rodzajami .
Operatory typu mogą wiązać zmienne typu. Na przykład podanie struktury prostego rachunku λ na poziomie typu wymaga powiązania lub operatorów typu wyższego rzędu. Te operatory typu wiążącego odpowiadają drugiej osi sześcianu λ i teoriom typu, takim jak prosty rachunek λ z operatorami typu λ ω . Połączenie operatorów typu z polimorficznym rachunkiem λ ( System F ) daje System F ω .
Zobacz też
- Pierce, Benjamin (2002). Typy i języki programowania . MIT Press. ISBN 0-262-16209-1 . , rozdział 29, „Operatory typów i sortowanie”
- PT Johnstone , Szkice słonia , s. 940