¿Cuál es la diferencia entre ADT, GADT y tipos inductivos?

¿Alguien podría explicar la diferencia entre:

Tipos de datos algebraicos (con los que estoy bastante familiarizado)
Tipos de datos algebraicos generalizados (¿qué los hace generalizados?)
Tipos inductivos (por ejemplo, Coq)

(Especialmente tipos inductivos.) Gracias.

lo.logic pl.programming-languages type-theory dependent-type ninjagecko
fuente

Respuestas:

Los tipos de datos algebraicos le permiten definir tipos de forma recursiva. Concretamente, supongamos que tenemos el tipo de datos

d a t a l i s t = N i l | C o n s o f N \times l i s t

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

Lo que esto significa es que es el conjunto más pequeño generado por los operadores y . Podemos formalizar esto definiendo el operador $\mathsf{list}$ $\mathsf{Nil}$ $\mathsf{Cons}$ $F(X)$

F (X) == {N i 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 \}$

y luego definiendo como $\mathsf{list}$

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

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

Un ADT generalizado es lo que obtenemos cuando definimos un operador de tipo recursivamente. Por ejemplo, podríamos definir el siguiente tipo de constructor:

b u s h a = L e a f o f a | N e s t o f b u s h (a \times a)

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

Este tipo significa que un elemento de es una tupla de s de longitud para alguna , ya que cada vez que entramos en el constructor el argumento de tipo se empareja consigo mismo . Entonces podemos definir el operador del que queremos tomar un punto fijo como: $\mathsf{bush\;}a$ $a$ $2^n$ $n$ $\mathsf{Nest}$

F (R) = λ X . {L e a 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) \}$

Un tipo inductivo en Coq es esencialmente un GADT, donde los índices del operador de tipo no están restringidos a otros tipos (como en, por ejemplo, Haskell), sino que también pueden indexarse por valores de la teoría de tipos. Esto le permite dar tipos para listas indexadas por longitud, etc.

Neel Krishnaswami
fuente

Gracias. ¿No significa eso, sin embargo, que "tipo inductivo" es completamente sinónimo de "tipo dependiente"?

ninjagecko

@Neel: Nunca he visto tipos como los bushllamados GADT. Los he visto llamados tipos anidados o no regulares.

jbapple

Los tipos anidados son un caso especial de GADT. La característica crítica de un GADT es simplemente que es una definición recursiva en un tipo superior. (Los cambios en la HR son básicamente el azúcar sintáctico para agregar una igualdad de tipo como componente del constructor).

Neel Krishnaswami

@ninjagecko: "Los tipos inductivos" son tipos con semántica como el punto menos fijo de un constructor. No todos los tipos pueden describirse de esta manera (las funciones no pueden, y tampoco pueden los tipos infinitos como las secuencias). Los tipos dependientes describen tipos que permiten que aparezcan términos del programa en ellos (es decir, los tipos pueden "depender de" los términos). Dado que Coq es una teoría de tipo dependiente, los tipos inductivos que le permite definir también son dependientes. Pero las teorías de tipos no dependientes también pueden admitir tipos inductivos, y esos tipos inductivos no serán dependientes.

Neel Krishnaswami

@NeelKrishnaswami: ¿Sería tan amable de aclarar su respuesta enumerando los "primeros pocos elementos más pequeños" de los tipos de bush a? En este ejemplo, ¿es Nest Leaf(a) Leaf(a) Leaf(a) Leaf(a)o Nest ((Nest Leaf(a) Leaf(a)) (Nest Leaf(a) Leaf(a)))como un ejemplo del conjunto?

ninjagecko

Considere tipos de datos algebraicos como:

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

Los tipos de retorno de cada constructor en un tipo de datos son todos iguales: Nily Consambos devuelven List a. Si permitimos que los constructores devuelvan diferentes tipos, tenemos un 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

Occupiedtiene el tipo a -> NullableList a b -> NullableList a NonEmpty, mientras que Constiene el tipo a -> List a -> List a. Es importante tener en cuenta que NonEmptyes un tipo, no un término. Otro ejemplo:

data Zero
data Succ n

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

Los tipos inductivos en lenguajes de programación que tienen tipos dependientes permiten que los tipos de retorno de los constructores dependan de los valores (no solo los tipos) de los argumentos.

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

Una nota al margen: GHC tiene un mecanismo para tratar a los constructores de valores como constructores de tipos . Esto no es lo mismo que los tipos inductivos dependientes que tiene Coq, pero disminuye un poco la carga sintáctica de los GADT y puede conducir a mejores mensajes de error.

jbapple
fuente

Gracias. "Tipos inductivos en lenguajes de programación que tienen tipos dependientes" ¿Cómo se vería un tipo inductivo en un lenguaje sin tipos dependientes, y puede tener tipos dependientes no inductivos (pero similares a GADT)?

ninjagecko