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 ${\displaystyle \mu \alpha .T}$ em que a variável tipo ${\displaystyle \alpha }$ pode aparecer no tipo ${\displaystyle 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:${\displaystyle 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 ${\displaystyle \mu \alpha .1+\alpha }$).

Ver também

• Recursividade