Rodzaj produktu
W językach programowania i teorii typów iloczyn typów to inny, złożony typ w strukturze . „Argumenty” produktu są typami , a struktura typu produktu jest określona przez ustaloną kolejność operandów w produkcie. Instancja typu produktu zachowuje ustaloną kolejność, ale poza tym może zawierać wszystkie możliwe instancje swoich pierwotnych typów danych . Wyrażeniem instancji typu produktu będzie krotka i jest nazywany wyrażeniem „typu krotki”. Produkt typów jest bezpośrednim produktem dwóch lub więcej typów.
Jeśli istnieją tylko dwa typy komponentów, można to nazwać „typem pary”. Na przykład, jeśli dwa typy składowe A i B są zbiorem wszystkich możliwych wartości tego typu, typ produktu zapisany A × B zawiera elementy będące parami (a, b), gdzie „a” i „b” są instancjami Odpowiednio A i B. Typ pary jest szczególnym przypadkiem zależnego typu pary , gdzie typ B może zależeć od instancji wybranej z A.
W wielu językach typy produktów przyjmują formę rekordu , w przypadku którego dostęp do komponentów krotki można uzyskać za pomocą etykiety . W językach, które mają algebraiczne typy danych , podobnie jak w większości funkcjonalnych języków programowania, algebraiczne typy danych z jednym konstruktorem są izomorficzne z typem produktu.
W korespondencji Curry’ego – Howarda typy produktów są powiązane w logice z spójnikiem logicznym (AND).
Pojęcie to rozciąga się bezpośrednio na iloczyn dowolnej skończonej liczby typów (n-arny typ iloczynu) i w tym przypadku charakteryzuje wyrażenia zachowujące się jak krotki wyrażeń odpowiednich typów. Zdegenerowaną formą typu produktu jest typ jednostki : jest to produkt bez typów .
W językach programowania typu call-by-value typ produktu można interpretować jako zbiór par, których pierwszym składnikiem jest wartość pierwszego typu, a drugim składnikiem jest wartość drugiego typu. Krótko mówiąc, jest to produkt kartezjański i odpowiada produktowi w kategorii typów.
Większość funkcjonalnych języków programowania ma prymitywne pojęcie typu produktu. Na przykład iloczyn typu 1 , ..., typu n jest zapisywany jako typ 1 * ... * typ n w ML i ( typ 1 , ... , typ n ) w Haskell . W obu tych językach zapisywane są krotki ( v 1 , ... , v n ) , a składniki krotki są wyodrębniane przez dopasowanie wzorca . Ponadto wiele funkcjonalnych języków programowania zapewnia bardziej ogólne algebraiczne typy danych , które rozszerzają zarówno typy iloczynu, jak i sumy . Typy produktów to podwójne sumy.
Zobacz też
- rodzaj produktu w n Lab
- Teoria typów homotopii: Uniwalentne podstawy matematyki , Program podstaw uniwalentnych, Instytut Studiów Zaawansowanych . Patrz sekcja 1.5 .