In der Typentheorie, einem Gebiet der mathematischen Logik und Informatik , ist ein Typkonstruktor ein Merkmal einer typisierten formalen Sprache , das neue Typen aus bestehenden erzeugt. Basistypen werden mithilfe von Nulltypkonstruktoren konstruiert . Einige Typkonstruktoren benötigen einen anderen Typ als Argument, beispielsweise die Konstruktoren für Produkttypen , Funktionstypen , Potenztypen und Listentypen . Neue Typen lassen sich durch rekursive Komposition von Typkonstruktoren definieren.

Beispielsweise kann der einfach typisierte Lambda-Kalkül als eine Sprache mit einem einzigen nicht-basischen Typkonstruktor – dem Funktionstypkonstruktor – betrachtet werden. Produkttypen können im Allgemeinen durch Currying in typisierten Lambda-Kalkülen als „eingebaut“ angesehen werden .

Abstrakt betrachtet ist ein Typkonstruktor ein n -ärer Typoperator, der null oder mehrere Typen als Argumente entgegennimmt und einen anderen Typ zurückgibt. Mithilfe von Currying lassen sich n -äre Typoperatoren als Folge von Anwendungen unärer Typoperatoren (um)schreiben. Daher können wir die Typoperatoren als einen einfach getypten Lambda-Kalkül betrachten, der nur einen Basistyp besitzt, üblicherweise mit `n` bezeichnet und als „Typ“ ausgesprochen. Dieser Basistyp ist der Typ aller Typen der zugrundeliegenden Sprache, die nun als echte Typen bezeichnet werden , um sie von den Typen der Typoperatoren in ihrem eigenen Kalkül, den sogenannten Arten, zu unterscheiden .

Typoperatoren können Typvariablen binden. Beispielsweise erfordert die Angabe der Struktur des einfach getypten λ-Kalküls auf Typenebene bindende oder höherwertige Typoperatoren. Diese bindenden Typoperatoren entsprechen der zweiten Achse des λ-Würfels und Typentheorien wie dem einfach getypten λ-Kalkül mit Typoperatoren, λ ω . Die Kombination von Typoperatoren mit dem polymorphen λ-Kalkül ( System F ) ergibt System F ω .

Einige funktionale Programmiersprachen verwenden explizit Typkonstruktoren. Ein bekanntes Beispiel ist Haskell , in dem alle dataTypdeklarationen als Deklarationen von Typkonstruktoren gelten und Basistypen (oder Null-Typkonstruktoren) als Typkonstanten bezeichnet werden. [ 1 ] [ 2 ] Typkonstruktoren können auch als parametrische polymorphe Datentypen betrachtet werden .

Siehe auch

Referenzen

  1. ^ Marlow, Simon (April 2010), „4.1.2 Syntax of Types“ , Haskell 2010 Language Report , abgerufen am 15. August 2023
  2. ^ „Konstruktor“ . HaskellWiki . Abgerufen am 15. August 2023 .
  • Pierce, Benjamin (2002). Typen und Programmiersprachen . MIT Press. ISBN 0-262-16209-1Die, Kapitel 29, „Typoperatoren und Kinding“
  • P. T. Johnstone , Skizzen eines Elefanten , S. 940