Tipo recursivo

Em ciência da computação, um tipo recursivo é um tipo de dado para valores que podem conter outros valores do mesmo tipo.

Um exemplo é uma lista em Haskell:

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

Isso indica que uma lista de a ou é uma lista vazia ou um elemento a (a cabeça da lista) seguido de uma lista de a (a cauda da lista).

Teoria

Em teoria dos tipos, um tipo recursivo possui a forma geral $\mu \alpha .T$ em que a variável tipo $\alpha$ pode aparecer no tipo $T$ e corresponder a todo o tipo. Por exemplo, o número natural (ver axiomas de Peano) pode ser definido pelo tipo Haskell:

 data Nat = Zero | Succ Nat

Em teoria dos tipos, diz-se:$nat=\mu \alpha .1+\alpha$ em que representa-se os construtores Zero e Succ. O primeiro não leva argumentos (então, representado pelo tipo unidade), e o segundo leva como argumento outro número natural (então, outro elemento $\mu \alpha .1+\alpha$).

Ver também

• Recursividade