Zweifel am Verhalten des Einheitentyps in einem Typsystem

Question

Ich habe Zweifel an dem Einheitentyp im Kontext der Typentheorie und seiner Verwendung in verschiedenen Fallszenarien.

Zu Beginn ein Gerätetyp kann als nullärer Produkttyp, nämlich Einheit, mit einem einzigen Wertbegriff angesehen werden, der das leere Tupel ist, ().Außerdem gibt es eine einzigartig karte von jedem Typ zum Gerät.

Nun kommt es vor, dass die Verwendung des Einheitentyps über eine solche triviale Definition hinausgeht und tatsächlich bei der Definition von algebraischen Datentypen verwendet wird, bei denen es sich um Summen von Produkttypen handelt.Insbesondere ist es möglich, das Konzept eines darzustellen Aufzählungstyp unter Verwendung einer Summe von Einheitentypen, z.in StandardML könnten wir haben:

datatype suit = HEARTS | CLUBS | DIAMONDS | SPADES

wobei HERZ, KREUZ, KARO und PIK nulläre Produkttypen sind und daher alle isomorph zur Einheit sind.

Mein Zweifel ist der folgende:wenn es nur ein Element von Unit gibt, wie kann das Typsystem zwischen den vier verschiedenen Instanzen unterscheiden, die im obigen Summentyp verwendet werden (fünf Instanzen, wenn wir auch das leere Tupel berücksichtigen)...)?Ich verstehe, dass sie bis zum Isomorphismus als alle gleich angesehen werden können, aber sie unterscheiden sich in der Ausdehnung und tatsächlich, selbst wenn man nur das berücksichtigt suit wir sollen sie nach Mustern abgleichen...

Answer 1

Die kurze Antwort lautet, dass isomorphe Typen trotz identischem Verhalten nicht gleich sind und das Typsystem daher zwischen ihnen unterscheiden kann.In einem Nominaltypsystem wie dem von Ihnen beschriebenen werden Typen im Wesentlichen durch ihre Namen identifiziert, auch wenn sie strukturell gleichwertig sind.Dies ist bei den von Ihnen beschriebenen fünf Einheitentypen der Fall:sie sind strukturell gleichwertig, aber nominell ungleich, und so werden sie als verschieden behandelt.

Beachten Sie, dass der Aspekt des Mustervergleichs orthogonal ist:sie können sich die fünf Einheitentypen als isoliert existierend vorstellen.In den meisten Typentheorien können Sie die Summe von zwei beliebigen Typen nehmen, sogar von zwei, die (nominell) gleich sind, z. Unit + Unit.Sie müssen weiterhin eine Musterübereinstimmung durchführen und haben zwei Fälle:Links Unit und das Richtige Unit.Der nominale Aspekt ist unwichtig, obwohl viele Programmiersprachen die Namen verwenden, um zwischen den verschiedenen Fällen wie diesem zu unterscheiden, anstelle der Indizes der Summanden (insbesondere in Sprachen, in denen Sie nur Summen verschiedener nominaler Typen verwenden dürfen, wie z Standard ML).