Was ist der Unterschied zwischen ADTs, GADTs und induktiven Typen?

Könnte jemand den Unterschied erklären zwischen:

Algebraische Datentypen (mit denen ich ziemlich vertraut bin)
Generalisierte algebraische Datentypen (was macht sie generalisiert?)
Induktive Typen (zB Coq)

(Besonders induktive Typen.) Danke.

lo.logic pl.programming-languages type-theory dependent-type Ninjagecko
quelle

Antworten:

Mit algebraischen Datentypen können Sie Typen rekursiv definieren. Nehmen wir konkret an, wir haben den Datentyp

d ein t ein l ich s t = N ich l | C O n s O f N \times l ich s t

$\mathsf{data\;list = Nil \;\;|\;\; Cons\;of\;\mathbb{N} \times list}$

Was dies bedeutet , ist , dass die kleinste Menge der erzeugten und Operatoren. Wir können dies formalisieren, indem wir den Operator $\mathsf{list}$ $\mathsf{Nil}$ $\mathsf{Cons}$ $F(X)$

F (X) == {N ich l} \cup {C O n s (n, x) | n \in N \land x \in X}

$F(X) == \{ \mathsf{Nil} \} \cup \{ \mathsf{Cons}(n, x) \;|\; n \in \mathbb{N} \land x \in X \}$

und dann definieren als $\mathsf{list}$

l ich s t = ⋃_{ich \in N} F^{ich} (\emptyset)

$\mathsf{list} = \bigcup_{i \in \mathbb{N}} F^i(\emptyset)$

Eine verallgemeinerte ADT erhalten wir, wenn wir einen Typoperator rekursiv definieren. Beispielsweise könnten wir den folgenden Typkonstruktor definieren:

b u s h ein = L e ein f O f ein | N e s t O f b u s h (ein \times ein)

$\mathsf{bush}\;a = \mathsf{Leaf\;of\;}a \;\;|\;\; \mathsf{Nest\;of\;bush}(a \times a)$

Dieser Typ bedeutet, dass ein Element von istfür mancheein Tupel von s der Länge $\mathsf{bush\;}a$ $a$ $2^n$ , da jedes Malwir in die gehen Konstruktor der Typ Argument mit sich selbst gepaart. So können wir den Operator definieren, den wir als festen Punkt verwenden möchten: $n$ $\mathsf{Nest}$

F (R) = λ X . {L e ein f (x) | x \in X} \cup {N e s t (v) | v \in R (X)}

$F(R) = \lambda X.\; \{ \mathsf{Leaf}(x) \;|\; x \in X\} \cup \{ \mathsf{Nest}(v) \;|\; v \in R(X) \}$

Ein induktiver Typ in Coq ist im Wesentlichen ein GADT, bei dem die Indizes des Typoperators nicht auf andere Typen beschränkt sind (wie beispielsweise in Haskell), sondern auch durch Werte der Typentheorie indiziert werden können . Auf diese Weise können Sie Typen für längenindexierte Listen usw. angeben.

Neel Krishnaswami
quelle

Vielen Dank. Wäre das nicht gleichbedeutend damit, dass "induktiver Typ" völlig synonym mit "abhängiger Typ" ist?

Ninjagecko

@Neel: Ich habe noch nie Typen wie bushGADTs gesehen. Ich habe sie als verschachtelte oder nicht reguläre Typen bezeichnet gesehen.

Jbapple

Geschachtelte Typen sind ein Sonderfall von GADTs. Das entscheidende Merkmal einer GADT ist einfach, dass es sich um eine rekursive Definition höherer Art handelt. (Änderungen an der rhs ist im Grunde syntaktischer Zucker für das Hinzufügen einer Typgleichheit als Komponente des Konstruktors.)

Neel Krishnaswami

@ninjagecko: "Induktive Typen" sind Typen mit Semantik als kleinstem Fixpunkt eines Konstruktors. Nicht alle Typen können auf diese Weise beschrieben werden (Funktionen können dies nicht, und es können auch keine unendlichen Typen wie z. B. Streams verwendet werden). Abhängige Typen beschreiben Typen, die das Auftreten von Programmbegriffen in ihnen ermöglichen (dh Typen können von Begriffen "abhängen"). Da es sich bei Coq um eine Theorie abhängiger Typen handelt, sind auch die induktiven Typen abhängig, die Sie definieren können. Unabhängige Typentheorien können jedoch auch induktive Typen unterstützen, und diese induktiven Typen sind nicht abhängig.

Neel Krishnaswami

@NeelKrishnaswami: Wären Sie so freundlich, Ihre Antwort zu klären, indem Sie die "ersten paar kleinsten" Elemente der Typen aufzählen bush a? In diesem Beispiel ist es Nest Leaf(a) Leaf(a) Leaf(a) Leaf(a)oder Nest ((Nest Leaf(a) Leaf(a)) (Nest Leaf(a) Leaf(a)))als ein Beispiel der Menge?

Ninjagecko

Betrachten Sie algebraische Datentypen wie:

data List a = Nil | Cons a (List a)

Die Rückgabetypen jedes Konstruktors in einem Datentyp sind alle gleich: Nilund Consbeide geben zurück List a. Wenn wir den Konstruktoren erlauben, verschiedene Typen zurückzugeben, haben wir eine GADT :

data Empty -- this is an empty data declaration; Empty has no constructors
data NonEmpty

data NullableList a t where
    Vacant :: NullableList a Empty
    Occupied :: a -> NullableList a b -> NullableList a NonEmpty

Occupiedhat den Typ a -> NullableList a b -> NullableList a NonEmpty, während Consder Typ hat a -> List a -> List a. Es ist wichtig zu beachten, dass dies NonEmptyein Typ ist, kein Begriff. Ein anderes Beispiel:

data Zero
data Succ n

data SizedList a t where
    Alone :: SizedList a Zero
    WithFriends :: a -> SizedList a n -> SizedList a (Succ n)

Induktive Typen in Programmiersprachen mit abhängigen Typen ermöglichen es den Rückgabetypen der Konstruktoren, von den Werten (nicht nur den Typen) der Argumente abzuhängen.

Inductive Parity := Even | Odd.

Definition flipParity (x:Parity) : Parity :=
  match x with
    | Even => Odd
    | Odd => Even
  end.

Fixpoint getParity (x:nat) : Parity :=
  match x with
    | 0 => Even
    | S n => flipParity (getParity n)
  end.

(*
A ParityNatList (Some P) is a list in which each member
is a natural number with parity P.
*)

Inductive ParityNatList : option Parity -> Type :=
  Nil : forall P, ParityNatList P
| Cons : forall (x:nat) (P:option Parity), 
  ParityNatList P -> ParityNatList 
  (match P, getParity x with
     | Some Even, Even => Some Even
     | Some Odd, Odd => Some Odd
     | _, _ => None
   end).

Eine Randnotiz: GHC hat einen Mechanismus zur Behandlung von Wertekonstruktoren als Typkonstruktoren . Dies ist nicht dasselbe wie die abhängigen induktiven Typen, die Coq hat, aber es verringert die syntaktische Belastung von GADTs etwas und kann zu besseren Fehlermeldungen führen.

Apfel
quelle

Vielen Dank. "Induktive Typen in Programmiersprachen mit abhängigen Typen" Wie würde ein induktiver Typ in einer Sprache ohne abhängige Typen aussehen, und können Sie nicht-induktive (aber GADT-ähnliche) abhängige Typen haben?

Ninjagecko