Jaka jest różnica między ADT, GADT i typami indukcyjnymi?

Może ktoś będzie w stanie wyjaśnić różnicę między:

Algebraiczne typy danych (które dość dobrze znam)
Uogólnione algebraiczne typy danych (co czyni je uogólnionymi?)
Rodzaje indukcyjne (np. Coq)

(Szczególnie typy indukcyjne.) Dziękuję.

lo.logic pl.programming-languages type-theory dependent-type ninjagecko
źródło

Odpowiedzi:

Algebraiczne typy danych umożliwiają rekurencyjne definiowanie typów. Konkretnie, załóżmy, że mamy typ danych

re za t za l ja s t = N. ja l | do o n s o fa N. \times l ja s t

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

Oznacza to, że jest najmniejszym zestawem generowanym przez operatorów i . Możemy to sformalizować, definiując operator $\mathsf{list}$ $\mathsf{Nil}$ $\mathsf{Cons}$ $F(X)$

fa (X) == {N. ja l} \cup {do 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 \}$

a następnie zdefiniowanie jako $\mathsf{list}$

l ja s t = ⋃_{ja \in N.} {fa}^{ja} (\emptyset)

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

Uogólnione ADT jest to, co otrzymujemy, kiedy zdefiniować typ operatora rekurencyjnie. Na przykład możemy zdefiniować następujący konstruktor typu:

b u s h za = L. mi za fa o fa za | N. mi s t o fa b u s h (za \times za)

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

Ten typ oznacza, że element jest krotką s o długości jakiegoś , ponieważ za każdym razem gdy w konstruktor typ argumentu jest połączony ze sobą . Możemy więc zdefiniować operatora, który chcemy przyjąć jako punkt stały: $\mathsf{bush\;}a$ $a$ $2^n$ $n$ $\mathsf{Nest}$

fa (R) = λ X . {L. mi za fa (x) | x \in X} \cup {N. mi 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) \}$

Typ indukcyjny w Coq jest zasadniczo GADT, gdzie indeksy operatora typu nie są ograniczone do innych typów (jak na przykład Haskell), ale mogą być również indeksowane według wartości teorii typów. Dzięki temu możesz podać typy list indeksowanych według długości i tak dalej.

Neel Krishnaswami
źródło

Dziękuję Ci. Czy nie oznacza to jednak, że „typ indukcyjny” jest całkowicie synonimem „typu zależnego”?

ninjagecko

@Neel: Nigdy nie widziałem typów takich jak bushGADT. Widziałem je nazywane typami zagnieżdżonymi lub nieregularnymi.

jbapple,

Typy zagnieżdżone są szczególnym przypadkiem GADT. Krytyczną cechą GADT jest po prostu to, że jest to definicja rekurencyjna na wyższym poziomie. (Zmiany w rhs to w zasadzie cukier syntaktyczny służący do dodania równości typu jako elementu konstruktora.)

Neel Krishnaswami

@ninjagecko: „Typy indukcyjne” to typy, które mają semantykę jako najmniej ustalony punkt konstruktora. Nie wszystkie typy można opisać w ten sposób (funkcje nie mogą, podobnie jak typy nieskończone, takie jak strumienie). Typy zależne opisują typy, które pozwalają na występowanie w nich warunków programu (to znaczy typy mogą „zależeć od” warunków). Ponieważ Coq jest teorią typów zależnych, typy indukcyjne, które pozwala zdefiniować, są również zależne. Ale teorie typów niezależnych mogą również obsługiwać typy indukcyjne, a te typy indukcyjne nie będą zależne.

Neel Krishnaswami,

@NeelKrishnaswami: Czy byłbyś tak uprzejmy, aby wyjaśnić swoją odpowiedź, wymieniając „kilka pierwszych najmniejszych” elementów typów bush a? W tym przykładzie jest to Nest Leaf(a) Leaf(a) Leaf(a) Leaf(a), czy Nest ((Nest Leaf(a) Leaf(a)) (Nest Leaf(a) Leaf(a)))jako jeden z przykładów zestawu?

ninjagecko

Rozważ algebraiczne typy danych, takie jak:

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

Rodzaje powrotne każdego konstruktora w typ danych są takie same: Nili Consobaj powrót List a. Jeśli pozwolimy konstruktorom zwracać różne typy, mamy 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

Occupiedma typ a -> NullableList a b -> NullableList a NonEmpty, a Consma typ a -> List a -> List a. Należy zauważyć, że NonEmptyjest to typ, a nie termin. Inny przykład:

data Zero
data Succ n

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

Typy indukcyjne w językach programowania, które mają typy zależne, pozwalają typom zwracanym przez konstruktory zależeć od wartości (nie tylko typów) argumentów.

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).

Uwaga dodatkowa: GHC ma mechanizm traktowania konstruktorów wartości jako konstruktorów typów . Nie jest to to samo co zależne typy indukcyjne, które posiada Coq, ale nieco zmniejsza obciążenie składniowe GADT i może prowadzić do lepszych komunikatów o błędach.

jbapple
źródło

Dziękuję Ci. „Typy indukcyjne w językach programowania, które mają typy zależne” Jak zatem wyglądałby typ indukcyjny w języku bez typów zależnych i czy można mieć typy nieindukcyjne (ale podobne do GADT)?

ninjagecko