Qual é a diferença entre ADTs, GADTs e tipos indutivos?

Alguém pode explicar a diferença entre:

Tipos de dados algébricos (com os quais estou bastante familiarizado)
Tipos de dados algébricos generalizados (o que os torna generalizados?)
Tipos indutivos (por exemplo, Coq)

(Tipos especialmente indutivos.) Obrigado.

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

Respostas:

Os tipos de dados algébricos permitem definir tipos recursivamente. Concretamente, suponha que tenhamos o tipo de dados

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}$

O que isto significa é que é o mais pequeno conjunto gerado pela e operadores. Podemos formalizar isso definindo o 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 \}$

e, em seguida, definir como $\mathsf{list}$

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

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

Um ADT generalizado é o que obtemos quando definimos um operador de tipo recursivamente. Por exemplo, podemos definir o seguinte construtor de tipos:

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

$\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) \}$

Um tipo indutivo em Coq é essencialmente um GADT, onde os índices do operador de tipo não são restritos a outros tipos (como, por exemplo, Haskell), mas também podem ser indexados por valores da teoria de tipos. Isso permite que você forneça tipos para listas indexadas por comprimento e assim por diante.

Neel Krishnaswami
fonte

Obrigado. No entanto, isso não significa apenas que "tipo indutivo" é completamente sinônimo de "tipo dependente"?

Ninjagecko 08/03/12

@ Neel: Eu nunca vi tipos como os bushchamados GADTs. Eu os vi chamados tipos aninhados ou não regulares.

jbapple

Tipos aninhados são um caso especial de GADTs. O recurso crítico de um GADT é simplesmente o fato de ser uma definição recursiva de tipo superior. (As alterações nas RHS é basicamente açúcar sintáctica para a adição de uma igualdade tipo como um componente do construtor.)

Neel Krishnaswami

@ninjagecko: "Tipos indutivos" são tipos que recebem semântica como o ponto menos fixo de um construtor. Nem todos os tipos podem ser descritos dessa maneira (funções não podem e nem infinitos, como fluxos). Tipos dependentes descrevem tipos que permitem que os termos do programa ocorram neles (ou seja, os tipos podem "depender de" termos). Como Coq é uma teoria de tipos dependentes, os tipos indutivos que ele permite definir também são dependentes. Mas as teorias de tipos não dependentes também podem suportar tipos indutivos, e esses tipos indutivos não serão dependentes.

Neel Krishnaswami

@NeelKrishnaswami: Você gostaria de esclarecer sua resposta enumerando os "primeiros poucos menores" elementos dos tipos de bush a? Neste exemplo, é Nest Leaf(a) Leaf(a) Leaf(a) Leaf(a)ou Nest ((Nest Leaf(a) Leaf(a)) (Nest Leaf(a) Leaf(a)))como um exemplo do conjunto?

Ninjagecko 11/07/12

Considere tipos de dados algébricos, como:

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

Os tipos de retorno de cada construtor em um tipo de dados são todos iguais: Nile Consambos retornam List a. Se permitirmos que os construtores retornem tipos diferentes, teremos um 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

Occupiedtem o tipo a -> NullableList a b -> NullableList a NonEmpty, enquanto Constem o tipo a -> List a -> List a. É importante notar que NonEmptyé um tipo, não um termo. Outro exemplo:

data Zero
data Succ n

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

Tipos indutivos em linguagens de programação que possuem tipos dependentes permitem que os tipos de retorno dos construtores dependam dos valores (não apenas dos tipos) dos 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).

Uma observação lateral: o GHC possui um mecanismo para tratar construtores de valor como construtores de tipo . Isso não é o mesmo que os tipos indutivos dependentes da Coq, mas diminui um pouco a carga sintática dos GADTs e pode levar a melhores mensagens de erro.

jbapple
fonte

Obrigado. "Tipos indutivos em linguagens de programação que possuem tipos dependentes" Como seria então um tipo indutivo em uma linguagem sem tipos dependentes e você pode ter tipos dependentes não indutivos (mas do tipo GADT)?

Ninjagecko 8/03/12