Los tipos de datos algebraicos le permiten definir tipos de forma recursiva. Concretamente, supongamos que tenemos el tipo de datos
datalist=Nil|ConsofN×list
Lo que esto significa es que es el conjunto más pequeño generado por los operadores y . Podemos formalizar esto definiendo el operadorN i l C o n s F ( X )listNilConsF(X)
F(X)=={Nil}∪{Cons(n,x)|n∈N∧x∈X}
y luego definiendo comolist
list=⋃i∈NFi(∅)
Un ADT generalizado es lo que obtenemos cuando definimos un operador de tipo recursivamente. Por ejemplo, podríamos definir el siguiente tipo de constructor:
busha=Leafofa|Nestofbush(a×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:a 2 n n N e s tbushaa2nnNest
F(R)=λX.{Leaf(x)|x∈X}∪{Nest(v)|v∈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.
Gracias. ¿No significa eso, sin embargo, que "tipo inductivo" es completamente sinónimo de "tipo dependiente"?
ninjagecko
44
@Neel: Nunca he visto tipos como los bushllamados GADT. Los he visto llamados tipos anidados o no regulares.
jbapple
3
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
44
@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
2
@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
19
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).
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)?
bush
llamados GADT. Los he visto llamados tipos anidados o no regulares.bush a
? En este ejemplo, ¿esNest Leaf(a) Leaf(a) Leaf(a) Leaf(a)
oNest ((Nest Leaf(a) Leaf(a)) (Nest Leaf(a) Leaf(a)))
como un ejemplo del conjunto?Considere tipos de datos algebraicos como:
Los tipos de retorno de cada constructor en un tipo de datos son todos iguales:
Nil
yCons
ambos devuelvenList a
. Si permitimos que los constructores devuelvan diferentes tipos, tenemos un GADT :Occupied
tiene el tipoa -> NullableList a b -> NullableList a NonEmpty
, mientras queCons
tiene el tipoa -> List a -> List a
. Es importante tener en cuenta queNonEmpty
es un tipo, no un término. Otro ejemplo: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.
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.
fuente