Tipos como cidadão de primeira classe

Vindo de um background em C ++, não entendo por que precisamos de tipos / expressões de tipo como cidadão de primeira classe? O único idioma que conheço que suporta esse recurso é o Aldor.

Alguém tem alguma literatura sobre tipos como cidadão de primeira classe ou conhece alguns motivos pelos quais é útil?

Os tipos de primeira classe ativam algo chamado digitação dependente . Isso permite que o programador use valores de tipos no nível de tipo. Por exemplo, o tipo de todos os pares de números inteiros é um tipo regular, enquanto o par de todos os números inteiros com o número esquerdo menor que o número direito é um tipo dependente. O exemplo introdutório padrão disso são as listas codificadas em tamanho (normalmente chamadas Vectorem Haskell / Idris). O pseudocódigo a seguir é uma mistura de Idris e Haskell.

-- a natural number
data Nat = Zero | Successor Nat

data Vector length typ where
  Empty : Vector Zero typ
  (::)   : typ -> Vector length typ -> Vector (Successor length) typ

Este pedaço de código nos diz duas coisas:

• A lista vazia tem comprimento zero.
• consinserir um elemento em uma lista cria uma lista de comprimento n + 1

Isso parece muito semelhante a outro conceito com 0 e n + 1não é? Eu voltarei a isso.

O que ganhamos com isso? Agora podemos determinar propriedades adicionais das funções que usamos. Por exemplo: Uma propriedade importante de appendé que o comprimento da lista resultante seja a soma dos comprimentos das duas listas de argumentos:

plus : Nat -> Nat -> Nat
plus          Zero n = n
plus (Successor m) n = Successor (plus m n)

append : Vector n a -> Vector m a -> Vector (plus n m) a
append Empty  ys = ys
append (x::xs) ys = x :: append xs ys

Mas, apesar de tudo, essa técnica não parece útil na programação cotidiana. Como isso se relaciona com soquetes, POST/ GETsolicitações e assim por diante?

Bem, não (pelo menos não sem um esforço considerável). Mas pode nos ajudar de outras maneiras:

Tipos dependentes nos permitem formular invariantes em regras de código como o modo como uma função deve se comportar. Usando isso, obtemos segurança adicional sobre o comportamento do código, semelhante às pré e pós-condições de Eiffel. Isso é extremamente útil para a prova automatizada de teoremas, que é um dos possíveis usos para Idris.

Voltando ao exemplo acima, a definição de listas codificadas em comprimento se assemelha ao conceito matemático de indução . Em Idris, você pode realmente formular o conceito de indução em uma lista da seguinte maneira:

              -- If you can supply the following:
list_induction : (Property : Vector len typ -> Type) -> -- a property to show
                  (Property Empty) -> -- the base case
                  ((w : a) -> (v : Vector n a) ->
                      Property v -> Property (w :: v)) -> -- the inductive step
                  (u : Vector m b) -> -- an arbitrary vector
                  Property u -- the property holds for all vectors

Essa técnica é limitada a provas construtivas, mas ainda assim é muito poderosa. Você pode tentar escrever appendindutivamente como um exercício.

Obviamente, tipos dependentes são apenas um dos tipos de primeira classe, mas é sem dúvida um dos mais comuns. Usos adicionais incluem, por exemplo, retornar um tipo específico de uma função com base em seus argumentos.

type_func : Vector n a -> Type
type_func Empty = Nat
type_func v     = Vector (Successor Zero) Nat

f : (v : Vector n a) -> type_func v
f Empty = 0
f vs    = length vs :: Empty

Este é um exemplo sem sentido, mas demonstra algo que você não pode emular sem os tipos de primeira classe.